The conjugate read off the polar of the homogenised epigraph

A convex function f on E is encoded, one dimension up, by the convex cone in ℝ × E × ℝ generated by the vectors (1, x, μ) with μ ≥ f x — the cone homCone f of Convex/Homogenize.lean. This module computes its polar for the pairing ⟨(λ, x, μ), (λ*, y, μ*)⟩ = λ λ* + ⟨x, y⟩ + μ μ*, and finds the conjugate of f inside it: under the reflection (λ*, y, μ*) ↦ (-μ*, y, -λ*) the polar of homCone f is exactly the closure of homCone f*.

So conjugacy of functions and polarity of cones are the same correspondence, read in two coordinate systems one dimension apart. Duality/Polar.lean develops polarity from conjugacy; this module is the derivation in the other direction.

Main definitions

• homConePairing B — the pairing of ℝ × E × ℝ with ℝ × F × ℝ induced by B.
• homCoord F — the homogenising coordinate (λ*, y, μ*) ↦ λ*. Its cross-section λ* = 1 is where the conjugate lives, and its positivity is what the density argument cuts on.
• negSwapEnds F — the reflection (λ*, y, μ*) ↦ (-μ*, y, -λ*), a linear involution.

Main results

• conj_le_coe_iff_forall_mem_epi — f*(y) ≤ c read on the epigraph: ⟨x, y⟩ - μ ≤ c for every (x, μ) ∈ epi f. This is what turns a polarity condition into a statement about f*.
• polarCone_homCone — the polar of homCone f unfolded. The cone hull is invisible to polarity, so the polar is cut out by the generating vectors (1, x, μ) alone.
• mem_homCone_conj_iff_of_pos — the cross-section: for λ* > 0, the reflected vector (-μ*, y, -λ*) lies in the polar of homCone f exactly when (λ*, y, μ*) lies in homCone f*.
• closure_homCone_conj — cl (homCone f*) = (negSwapEnds F) ⁻¹' (homCone f)° (Theorem 14.4 in [^1]).

Divergences from the reference

The hypotheses are the two properness conditions rather than "closed proper convex": dom f nonempty, to see that the polar lies in the half-space λ* ≥ 0, and dom f* nonempty, to see that it is not contained in the boundary hyperplane λ* = 0, plus convexity of f. Closedness of f is what makes the second automatic, and belongs at the call site.

No bipolar theorem is used, and no closure of K. The classical argument reads "cl K contains (0, 0, 1) but not (0, 0, -1)"; both facts are already visible in K, from the ray (1, x₀, r + t) and from a single affine minorant of f. So the whole module needs no local convexity, no compatibility of the pairing and no finite dimension.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14.

The pairing, the coordinate and the reflection

@[reducible, inline]

abbrev Tdaf.ConvexAnalysis.homConePairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (ℝ × E) × ℝ →ₗ[ℝ] (ℝ × F) × ℝ →ₗ[ℝ] ℝ

The pairing of ℝ × E × ℝ with ℝ × F × ℝ induced by B: ⟨(λ, x, μ), (λ*, y, μ*)⟩ = λ λ* + ⟨x, y⟩ + μ μ*. An abbrev, so that the prodPairing instances remain visible to instance search.

Equations

• Tdaf.ConvexAnalysis.homConePairing B = Tdaf.ConvexAnalysis.epiPairing (Tdaf.ConvexAnalysis.prodPairing Tdaf.ConvexAnalysis.mulPairing B)

@[simp]

theorem Tdaf.ConvexAnalysis.homConePairing_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (p : (ℝ × E) × ℝ) (q : (ℝ × F) × ℝ) : ((homConePairing B) p) q = p.1.1 * q.1.1 + (B p.1.2) q.1.2 + p.2 * q.2

theorem Tdaf.ConvexAnalysis.homConePairing_flip {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (homConePairing B).flip = homConePairing B.flip

def Tdaf.ConvexAnalysis.homCoord (F : Type u_3) [AddCommGroup F] [Module ℝ F] : (ℝ × F) × ℝ →ₗ[ℝ] ℝ

The homogenising coordinate (λ*, y, μ*) ↦ λ*, as a linear functional on ℝ × F × ℝ.

Equations

• Tdaf.ConvexAnalysis.homCoord F = LinearMap.fst ℝ ℝ F ∘ₗ LinearMap.fst ℝ (ℝ × F) ℝ

@[simp]

theorem Tdaf.ConvexAnalysis.homCoord_apply {F : Type u_2} [AddCommGroup F] [Module ℝ F] (q : (ℝ × F) × ℝ) : (homCoord F) q = q.1.1

def Tdaf.ConvexAnalysis.negSwapEnds (F : Type u_3) [AddCommGroup F] [Module ℝ F] : (ℝ × F) × ℝ →ₗ[ℝ] (ℝ × F) × ℝ

The reflection (λ*, y, μ*) ↦ (-μ*, y, -λ*) of ℝ × F × ℝ: it exchanges the homogenising coordinate with the epigraph coordinate and reverses the sign of both. This linear involution is the change of variables that turns the polar of a homogenised epigraph back into one.

Equations

• Tdaf.ConvexAnalysis.negSwapEnds F = { toFun := fun (q : (ℝ × F) × ℝ) => ((-q.2, q.1.2), -q.1.1), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.negSwapEnds_apply {F : Type u_2} [AddCommGroup F] [Module ℝ F] (q : (ℝ × F) × ℝ) : (negSwapEnds F) q = ((-q.2, q.1.2), -q.1.1)

@[simp]

theorem Tdaf.ConvexAnalysis.negSwapEnds_negSwapEnds {F : Type u_2} [AddCommGroup F] [Module ℝ F] (q : (ℝ × F) × ℝ) : (negSwapEnds F) ((negSwapEnds F) q) = q

theorem Tdaf.ConvexAnalysis.continuous_negSwapEnds (F : Type u_3) [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] : Continuous ⇑(negSwapEnds F)

The conjugate on the epigraph

theorem Tdaf.ConvexAnalysis.conj_le_coe_iff_forall_mem_epi {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {y : F} {c : ℝ} : conj B f y ≤ ↑c ↔ ∀ p ∈ epi f, (B p.1) y - p.2 ≤ c

f*(y) ≤ c read on the epigraph: ⟨x, y⟩ - μ ≤ c for every point (x, μ) of the epigraph. This is conj_le_coe_iff with the affine minorant traded for the epigraph it dominates, and it needs no properness.

The polar of the homogenised epigraph

theorem Tdaf.ConvexAnalysis.mem_polarCone_epi_levelOneLift {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {q : (ℝ × F) × ℝ} : q ∈ polarCone (homConePairing B) (epi (levelOneLift f)) ↔ ∀ (x : E) (μ : ℝ), f x ≤ ↑μ → q.1.1 + (B x) q.1.2 + μ * q.2 ≤ 0

Membership of the polar of the generating epigraph, unfolded: the generating vectors are the (1, x, μ) with μ ≥ f x, and each of them contributes one homogeneous inequality.

theorem Tdaf.ConvexAnalysis.polarCone_homCone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : ConvexFn f) : polarCone (homConePairing B) (homCone f) = polarCone (homConePairing B) (epi (levelOneLift f))

Polarity does not see the cone generated: the polar of homCone f is cut out by the generating vectors (1, x, μ) alone.

theorem Tdaf.ConvexAnalysis.mem_homCone_conj_iff_of_pos {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : ConvexFn f) {q : (ℝ × F) × ℝ} (ha : 0 < q.1.1) : q ∈ homCone (conj B f) ↔ (negSwapEnds F) q ∈ polarCone (homConePairing B) (homCone f)

The cross-section. For a strictly positive homogenising coordinate, the reflected vector (-μ*, y, -λ*) lies in the polar of homCone f exactly when (λ*, y, μ*) lies in homCone f*. This is the computation "(-μ*, x*, -1) ∈ K° iff μ* ≥ f*(x*)", at a general positive λ*.

theorem Tdaf.ConvexAnalysis.nonpos_of_forall_add_mul_nonpos {C d : ℝ} (h : ∀ (t : ℝ), 0 ≤ t → C + t * d ≤ 0) : d ≤ 0

If a real affine expression C + t d is non-positive for every t ≥ 0, its slope is non-positive. This is the "let μ → ∞ along the vertical ray" step, done with an explicit t.

theorem Tdaf.ConvexAnalysis.nonneg_homCoord_of_mem_polarCone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : ConvexFn f) (hdom : (dom f).Nonempty) {q : (ℝ × F) × ℝ} (hq : (negSwapEnds F) q ∈ polarCone (homConePairing B) (homCone f)) : 0 ≤ (homCoord F) q

The polar of the homogenised epigraph lies in the half-space λ* ≥ 0. The vertical ray (1, x₀, r + t), t ≥ 0, above a point of dom f is what forces it.

The theorem

theorem Tdaf.ConvexAnalysis.closure_homCone_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsContinuousPairing B.flip] (hf : ConvexFn f) (hdom : (dom f).Nonempty) (hdom' : (dom (conj B f)).Nonempty) : closure (homCone (conj B f)) = ⇑(negSwapEnds F) ⁻¹' polarCone (homConePairing B) (homCone f)

For a convex f with nonempty effective domain and nonempty conjugate domain, and K the convex cone generated by the vectors (1, x, μ) with μ ≥ f x,

cl (homCone f*) = {(λ*, y, μ*) | (-μ*, y, -λ*) ∈ (homCone f)°}.

The three steps are the cross-section λ* > 0, the fact that the polar lies in λ* ≥ 0, and Convex.closure_inter_setOf_pos.