Monotone conjugacy on the half-line, and the convex functions built from a gauge

Two correspondences that fit together. The first is conjugacy for nondecreasing convex functions of one nonnegative variable: on that class the ordinary conjugate, cut back to the half-line, is again such a function, and the operation is an involution. The second composes such a function with a closed gauge on a vector space; the result is a convex function all of whose sublevel sets are dilates of one another, and conjugacy on those functions is the first correspondence applied level by level, with the gauge replaced by its polar. Specialising the half-line factor to ζ ↦ ζ^p / p gives the functions positively homogeneous of degree p, whose conjugates are positively homogeneous of the Hölder conjugate degree q; that the two powers are exchanged is Young's inequality, read as a conjugacy.

Main definitions

• MonotoneHalfLineFn g — g : ℝ → EReal is +∞ on the negative axis, nondecreasing on the half-line, convex, closed, and finite at the origin.
• IsGaugeLike f — f 0 = inf f, and the sublevel sets above that infimum are all positive multiples of one another.
• monotoneConj g — the monotone conjugate g⁺(s) = sup {t s - g t ∣ t ≥ 0}, itself taken to be +∞ for s < 0.
• monotoneComp g k — the composite g ∘ k of such a g with a [0, +∞]-valued k, under the convention g (+∞) = +∞.
• levelSup g α — the crossing level sup {ζ ≥ 0 ∣ g ζ ≤ α}, the dilation factor of the sublevel set {g ∘ k ≤ α}.
• powHalfLine p, PosHomogeneousDeg p f, degGauge p f — the function ζ ↦ ζ^p / p of the half-line; the condition f (λ x) = λ^p f x for λ > 0; and the gauge (p f)^{1/p} attached to such an f.

Main results

• monotoneHalfLineFn_monotoneConj, monotoneConj_monotoneConj — the class is stable under monotoneConj, and g⁺⁺ = g (Theorem 12.4 in [^1]).
• closedProperConvexFn_monotoneComp, setOf_monotoneComp_le_eq_smul — for a non-constant g, g ∘ k is closed proper convex, and its sublevel sets are all dilates of {k ≤ 1}.
• conj_monotoneComp — (g ∘ k)* = g⁺ ∘ k° for a closed gauge k.
• monotoneConj_powHalfLine — (ζ ↦ ζ^p / p)⁺ = (σ ↦ σ^q / q).
• posHomogeneousDeg_iff_exists_isGauge — a closed proper convex function is positively homogeneous of degree p exactly when it is (1/p) k^p for a closed gauge k.
• conj_monotoneComp_powHalfLine, polarGauge_degGauge, pairing_le_rpow_mul_rpow, polarSet_setOf_le_inv — the conjugate of (1/p) k^p is (1/q) (k°)^q, the gauges (p f)^{1/p} and (q f*)^{1/q} are polar, and the level sets {f ≤ 1/p} and {f* ≤ 1/q} are polar sets.
• closedProperConvexFn_and_isGaugeLike_iff — a function is closed proper convex and gauge-like exactly when it is g ∘ k for a closed gauge k and a non-constant MonotoneHalfLineFn g (Theorem 15.3 in [^1]). IsGaugeLike.exists_eq_monotoneComp is the reconstruction half.

Implementation notes

A MonotoneHalfLineFn may be constant, and then g ∘ k need not be closed: its sublevel sets are dom k, which for a closed gauge can fail to be closed. That is what the "non-constant" hypothesis buys, and it enters only through MonotoneHalfLineFn.exists_monotoneConj_ne_top; the conjugacy formula itself does not need it.

References

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

Restriction to a closed set

theorem Tdaf.ConvexAnalysis.ClosedFn.restrict {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] {f : E → EReal} {s : Set E} (hf : ClosedFn f) (hne : ∀ (x : E), f x ≠ ⊥) (hs : IsClosed s) : ClosedFn (ConvexAnalysis.restrict s f)

Cutting a closed function down to a closed set leaves it closed.

The self-pairing of the line, flipped

mulPairing is its own flip, but only propositionally, so the results stated against B.flip need the flipped copy to be visible to instance search as well.

instance Tdaf.ConvexAnalysis.instIsContinuousPairingRealFlipMulPairing : IsContinuousPairing mulPairing.flip

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingRealFlipMulPairing : IsCompatiblePairing mulPairing.flip

Nondecreasing convex functions on the half-line

structure Tdaf.ConvexAnalysis.MonotoneHalfLineFn (g : ℝ → EReal) : Prop

A nondecreasing closed convex function on the half-line: +∞ on the negative axis, nondecreasing on [0, ∞), convex, closed, and finite at the origin.

Convexity and closedness are asked of g as a function on all of ℝ; because g is +∞ to the left of the origin, that is the same as asking them on the half-line. This is exactly the class on which monotone conjugacy is an involution.

• top_of_neg ⦃t : ℝ⦄ : t < 0 → g t = ⊤

  g is +∞ to the left of the origin.

• monotoneOn : MonotoneOn g (Set.Ici 0)

  g is nondecreasing on the half-line.

• convex : ConvexFn g

  g is convex.

• closed : ClosedFn g

  g is closed.

• zero_ne_top : g 0 ≠ ⊤

  g is finite at the origin.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.ne_bot {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (t : ℝ) : g t ≠ ⊥

A function of this class never takes the value -∞: it is +∞ somewhere, so the exceptional branch of clFn is excluded.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.iInf_eq_zero {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) : ⨅ (t : ℝ), g t = g 0

The infimum of g is attained at the origin.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.zero_le {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (t : ℝ) : g 0 ≤ g t

g 0 is the least value of g.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.proper {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) : Proper g

A function of this class is proper.

The monotone conjugate

noncomputable def Tdaf.ConvexAnalysis.monotoneConj (g : ℝ → EReal) : ℝ → EReal

The monotone conjugate g⁺(s) = sup {t s - g t ∣ t ≥ 0} of a function on the half-line. Like g itself it is taken to be +∞ to the left of the origin, which is what makes the operation an involution rather than a bijection onto a smaller class.

Equations

• Tdaf.ConvexAnalysis.monotoneConj g = Tdaf.ConvexAnalysis.restrict (Set.Ici 0) fun (s : ℝ) => ⨆ (t : ℝ), ⨆ (_ : 0 ≤ t), ↑(t * s) - g t

theorem Tdaf.ConvexAnalysis.monotoneConj_of_nonneg {s : ℝ} (g : ℝ → EReal) (hs : 0 ≤ s) : monotoneConj g s = ⨆ (t : ℝ), ⨆ (_ : 0 ≤ t), ↑(t * s) - g t

theorem Tdaf.ConvexAnalysis.monotoneConj_of_neg {s : ℝ} (g : ℝ → EReal) (hs : s < 0) : monotoneConj g s = ⊤

theorem Tdaf.ConvexAnalysis.conj_mulPairing_apply {g : ℝ → EReal} (hg : ∀ ⦃t : ℝ⦄, t < 0 → g t = ⊤) (s : ℝ) : conj mulPairing g s = ⨆ (t : ℝ), ⨆ (_ : 0 ≤ t), ↑(t * s) - g t

On a function that is +∞ to the left of the origin, the supremum over the half-line and the supremum over the whole line agree, so the monotone conjugate is the ordinary conjugate for mulPairing, cut back to the half-line.

theorem Tdaf.ConvexAnalysis.monotoneConj_eq_restrict_conj {g : ℝ → EReal} (hg : ∀ ⦃t : ℝ⦄, t < 0 → g t = ⊤) : monotoneConj g = restrict (Set.Ici 0) (conj mulPairing g)

The monotone conjugate as a restricted ordinary conjugate.

theorem Tdaf.ConvexAnalysis.monotoneConj_of_nonneg' {g : ℝ → EReal} {s : ℝ} (hg : ∀ ⦃t : ℝ⦄, t < 0 → g t = ⊤) (hs : 0 ≤ s) : monotoneConj g s = conj mulPairing g s

On the half-line the monotone conjugate and the ordinary conjugate agree.

theorem Tdaf.ConvexAnalysis.conj_le_monotoneConj {g : ℝ → EReal} (hg : ∀ ⦃t : ℝ⦄, t < 0 → g t = ⊤) (s : ℝ) : conj mulPairing g s ≤ monotoneConj g s

The monotone conjugate dominates the ordinary one, being +∞ where they differ.

theorem Tdaf.ConvexAnalysis.monotone_conj_mulPairing {g : ℝ → EReal} (hg : ∀ ⦃t : ℝ⦄, t < 0 → g t = ⊤) : Monotone (conj mulPairing g)

The ordinary conjugate of a function that is +∞ to the left of the origin is nondecreasing: only nonnegative arguments contribute to the supremum.

theorem Tdaf.ConvexAnalysis.conj_mulPairing_of_nonpos {g : ℝ → EReal} {s : ℝ} (hg : MonotoneHalfLineFn g) (hs : s ≤ 0) : conj mulPairing g s = -g 0

The conjugate is constant to the left of the origin, with the value -g 0.

theorem Tdaf.ConvexAnalysis.monotoneConj_zero {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) : monotoneConj g 0 = -g 0

The monotone conjugate at the origin is -g 0.

theorem Tdaf.ConvexAnalysis.monotoneHalfLineFn_monotoneConj {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) : MonotoneHalfLineFn (monotoneConj g)

The class is stable under monotone conjugacy.

theorem Tdaf.ConvexAnalysis.iSup_sub_monotoneConj {g : ℝ → EReal} {t : ℝ} (hg : MonotoneHalfLineFn g) (ht : 0 ≤ t) : ⨆ (s : ℝ), ↑(s * t) - monotoneConj g s = ⨆ (s : ℝ), ↑(s * t) - conj mulPairing g s

The negative half of the line contributes nothing to the biconjugate supremum at a nonnegative argument: there g⁺ is constant, and the constant is already the value of the term at the origin. This is the only place where the truncation in monotoneConj has to be undone.

theorem Tdaf.ConvexAnalysis.monotoneConj_monotoneConj {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) : monotoneConj (monotoneConj g) = g

Monotone conjugacy is an involution on the nondecreasing closed convex functions of one nonnegative variable that are finite at the origin.

The proof is the Fenchel–Moreau theorem for mulPairing together with iSup_sub_monotoneConj, which says that truncating the conjugate to the half-line does not change the second conjugate at a nonnegative argument.

Composing a gauge with a function on the half-line

noncomputable def Tdaf.ConvexAnalysis.monotoneComp {E : Type u_1} (g : ℝ → EReal) (k : E → EReal) : E → EReal

The composite g ∘ k of a function on the half-line with a [0, +∞]-valued function k, with the convention g (+∞) = +∞.

Presenting the composite as an infimum over the real levels above k x avoids extending g to EReal by hand — and hence a Decidable split — while making both defining equations one-line consequences: monotoneComp g k x = g c when k x = c and g is nondecreasing on the half-line (monotoneComp_of_eq_coe), and monotoneComp g k x = ⊤ when k x = ⊤ (monotoneComp_of_eq_top).

Equations

• Tdaf.ConvexAnalysis.monotoneComp g k x = ⨅ (t : ℝ), ⨅ (_ : k x ≤ ↑t), g t

theorem Tdaf.ConvexAnalysis.monotoneComp_apply {E : Type u_1} (g : ℝ → EReal) (k : E → EReal) (x : E) : monotoneComp g k x = ⨅ (t : ℝ), ⨅ (_ : k x ≤ ↑t), g t

The defining formula for the composite.

theorem Tdaf.ConvexAnalysis.monotoneComp_le {E : Type u_1} {g : ℝ → EReal} {k : E → EReal} {x : E} {c : ℝ} (h : k x ≤ ↑c) : monotoneComp g k x ≤ g c

Every real level above k x bounds the composite from above.

theorem Tdaf.ConvexAnalysis.monotoneComp_of_eq_top {E : Type u_1} {k : E → EReal} {x : E} (g : ℝ → EReal) (h : k x = ⊤) : monotoneComp g k x = ⊤

The composite is +∞ wherever k is: no real level lies above +∞.

theorem Tdaf.ConvexAnalysis.monotoneComp_of_eq_coe {E : Type u_1} {g : ℝ → EReal} {k : E → EReal} {x : E} {c : ℝ} (hg : MonotoneOn g (Set.Ici 0)) (hc : 0 ≤ c) (h : k x = ↑c) : monotoneComp g k x = g c

The composite at a finite value of k: the infimum is attained at the level t = k x, because g is nondecreasing on the half-line. No semicontinuity is involved.

theorem Tdaf.ConvexAnalysis.eq_top_or_exists_coe_of_nonneg {z : EReal} (hz : 0 ≤ z) : z = ⊤ ∨ ∃ (c : ℝ), 0 ≤ c ∧ z = ↑c

A nonnegative extended real is either +∞ or a nonnegative real.

Convexity and properness of the composite

theorem Tdaf.ConvexAnalysis.convexFn_monotoneComp {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : ℝ → EReal} {k : E → EReal} (hg : ConvexFn g) (hk : ConvexFn k) : ConvexFn (monotoneComp g k)

Composing preserves convexity. No monotonicity of g is needed: the infimum over the real levels above k x already builds it in, and the strict form of convexity (convexFn_iff_forall_lt) supplies a level for each side to be combined.

theorem Tdaf.ConvexAnalysis.proper_monotoneComp {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : ℝ → EReal} {k : E → EReal} (hg : MonotoneHalfLineFn g) (hk : IsGauge k) : Proper (monotoneComp g k)

The composite is proper: it takes the value g 0 at the origin, which is finite, and it is bounded below by g 0 everywhere.

Growth of a non-constant function of the half-line

A convex nondecreasing function of the half-line that is not constant grows at least linearly, so its monotone conjugate is finite at small positive arguments. That is the exact content of the "non-constant" hypothesis: it is what makes g ∘ k closed.

theorem Tdaf.ConvexAnalysis.coe_add_mul_le_of_convex {g : ℝ → EReal} {c₀ r t₂ : ℝ} (hg : ConvexFn g) (hnb : ∀ (z : ℝ), g z ≠ ⊥) (h0 : g 0 ≤ ↑c₀) (ht₂ : 0 < t₂) (hr : ↑r ≤ g t₂) {t : ℝ} (ht : t₂ ≤ t) : ↑(c₀ + (r - c₀) / t₂ * t) ≤ g t

A convex function of the half-line lies above the secant through the origin, extended. If g 0 ≤ c₀ and r ≤ g t₂ with t₂ > 0, then g t ≥ c₀ + ((r - c₀) / t₂) t for t ≥ t₂.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.exists_affine_minorant {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) : ∃ (m : ℝ) (c₀ : ℝ) (t₂ : ℝ), 0 < m ∧ 0 < t₂ ∧ g 0 = ↑c₀ ∧ ∀ (t : ℝ), t₂ ≤ t → ↑(c₀ + m * t) ≤ g t

A non-constant convex nondecreasing function of the half-line has an affine minorant of positive slope, beyond the point where it first rises. This is the quantitative form of "g (ζ) → +∞".

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.exists_monotoneConj_ne_top {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) : ∃ (ζ : ℝ), 0 < ζ ∧ monotoneConj g ζ ≠ ⊤

The monotone conjugate of a non-constant function of the half-line is finite somewhere on the positive axis — it is finite at every ζ below the slope of the affine minorant.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.exists_lt_monotoneConj {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) : ∃ (s : ℝ), 0 < s ∧ monotoneConj g 0 < monotoneConj g s

The monotone conjugate of a function finite at a positive level is non-constant. The term of the defining supremum at that level is an affine function of s with positive slope, so g⁺ grows without bound. Together with MonotoneHalfLineFn.exists_monotoneConj_ne_top this is Rockafellar's "g⁺ satisfies the same conditions as g", and it shows that conjugacy exchanges the two side conditions.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.bddAbove_setOf_le {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) (α : ℝ) : BddAbove {t : ℝ | 0 ≤ t ∧ g t ≤ ↑α}

The set of levels at which a non-constant function of the half-line is below a given real bound is bounded above: past the affine minorant, c₀ + m t ≤ α caps t.

theorem Tdaf.ConvexAnalysis.MonotoneHalfLineFn.exists_pos_le {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) {α : ℝ} (hα : g 0 < ↑α) : ∃ (t : ℝ), 0 < t ∧ g t ≤ ↑α

A convex function of the half-line finite at some positive level is continuous from the right at the origin, in the form needed here: every real level strictly above g 0 is already attained at some positive argument. Without finiteness at a positive level g may jump to +∞ at once.

noncomputable def Tdaf.ConvexAnalysis.levelSup (g : ℝ → EReal) (α : ℝ) : ℝ

The crossing level sup {ζ ≥ 0 ∣ g ζ ≤ α} of a function of the half-line. It is the dilation factor of the sublevel set {g ∘ k ≤ α}.

Equations

• Tdaf.ConvexAnalysis.levelSup g α = sSup {t : ℝ | 0 ≤ t ∧ g t ≤ ↑α}

theorem Tdaf.ConvexAnalysis.levelSup_mem {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) {α : ℝ} (hα : g 0 ≤ ↑α) : 0 ≤ levelSup g α ∧ g (levelSup g α) ≤ ↑α

The crossing level is attained: the set of levels below α is closed and bounded.

theorem Tdaf.ConvexAnalysis.le_levelSup {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) {α t : ℝ} (ht : 0 ≤ t) (htα : g t ≤ ↑α) : t ≤ levelSup g α

Any level below α is below the crossing level.

theorem Tdaf.ConvexAnalysis.levelSup_pos {g : ℝ → EReal} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) {α : ℝ} (hα : g 0 < ↑α) : 0 < levelSup g α

The crossing level is positive as soon as α is strictly above g 0 and g is finite somewhere on the positive axis.

The sublevel sets of g ∘ k are dilates of one another

This is the geometric content of Rockafellar's "gauge-like": every sublevel set {g ∘ k ≤ α} with α above the minimum is the dilate λ • {k ≤ 1}, with λ the crossing level of g at α.

theorem Tdaf.ConvexAnalysis.monotoneComp_le_coe_iff {E : Type u_1} {g : ℝ → EReal} {k : E → EReal} {α : ℝ} (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) (hknn : ∀ (z : E), 0 ≤ k z) (hα : g 0 ≤ ↑α) (x : E) : monotoneComp g k x ≤ ↑α ↔ k x ≤ ↑(levelSup g α)

The sublevel sets of g ∘ k are the sublevel sets of k, at the crossing level.

theorem Tdaf.ConvexAnalysis.setOf_monotoneComp_le_eq_smul {E : Type u_1} {g : ℝ → EReal} {k : E → EReal} {α : ℝ} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) (hα : g 0 < ↑α) : {x : E | monotoneComp g k x ≤ ↑α} = levelSup g α • {x : E | k x ≤ 1}

The sublevel sets of g ∘ k are dilates of {k ≤ 1} — Rockafellar's "gauge-like", for the composite of a closed gauge with a non-constant nondecreasing closed convex function of the half-line finite at some positive level.

The conjugate of a gauge composed with a function on the half-line

The composite g ∘ k of a closed gauge with a nondecreasing closed convex function on the half-line is conjugate to the composite of the polar gauge with the monotone conjugate. The proof regroups the supremum defining the conjugate by the level ζ = k x: on the dilate ζ • {k ≤ 1} the composite is at most g ζ, and the supremum of the pairing over that dilate is ζ k°(y). Closedness of k enters only through conj_monotoneComp_le.

theorem Tdaf.ConvexAnalysis.pairing_nonpos_of_gauge_eq_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {k : E → EReal} {x : E} {y : F} {c : ℝ} (hk : IsGauge k) (hx : k x = 0) (hc : polarGauge B k y = ↑c) : (B x) y ≤ 0

Where a gauge vanishes the pairing is nonpositive, provided the polar gauge is finite there.

The set {k = 0} is the recession cone of {k ≤ 1} and not in general {0}, so the bound has to be obtained by scaling: k (l⁻¹ • x) = 0 ≤ 1 for every l > 0, whence ⟨x, y⟩ ≤ l k°(y), and letting l shrink gives ⟨x, y⟩ ≤ 0. Finiteness of k°(y) is essential — in EReal, 0 * (+∞) = 0.

theorem Tdaf.ConvexAnalysis.coe_mul_polarGauge_sub_le_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : ℝ → EReal} {k : E → EReal} {y : F} (hk : IsGauge k) {ζ r : ℝ} (hζ : 0 < ζ) (hr : g ζ = ↑r) : ↑ζ * polarGauge B k y - g ζ ≤ conj B (monotoneComp g k) y

The core lower bound. On the dilate ζ • {k ≤ 1} the composite g ∘ k is at most g ζ, and the supremum of the pairing over that dilate is ζ k°(y); so ζ k°(y) - g ζ is a lower bound for the conjugate of g ∘ k, at every level ζ > 0 where g is finite.

Nothing is assumed about g beyond finiteness at the single level ζ, and nothing about k beyond its being a gauge. This one lemma supplies both the ≥ half of the conjugacy formula and, at a point where the polar gauge is +∞, the degeneracy that forces the conjugate to be +∞ there.

theorem Tdaf.ConvexAnalysis.sub_apply_zero_le_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : ℝ → EReal} {k : E → EReal} {y : F} (hk : IsGauge k) (hg : MonotoneOn g (Set.Ici 0)) : 0 - g 0 ≤ conj B (monotoneComp g k) y

The origin realises the level ζ = 0 of the computation, since a gauge vanishes there.

theorem Tdaf.ConvexAnalysis.monotoneConj_le_conj_monotoneComp {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : ℝ → EReal} {k : E → EReal} {y : F} {c : ℝ} (hk : IsGauge k) (hg : MonotoneHalfLineFn g) (hc : polarGauge B k y = ↑c) : monotoneConj g c ≤ conj B (monotoneComp g k) y

The ≥ half of the conjugacy formula, at a point where the polar gauge is finite.

theorem Tdaf.ConvexAnalysis.pairing_le_mul_of_gauge {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {k : E → EReal} {x : E} {y : F} {c : ℝ} (hk : IsGauge k) (hkc : ClosedFn k) {d : ℝ} (hx : k x = ↑c) (hy : polarGauge B k y = ↑d) : (B x) y ≤ c * d

The Cauchy–Schwarz inequality for a gauge and its polar: ⟨x, y⟩ ≤ k(x) k°(y) wherever both sides are finite.

For k(x) > 0 this is the level-set description of a closed gauge, x ∈ k(x) • {k ≤ 1}, together with the identification of k° as the support function of {k ≤ 1}. For k(x) = 0 the product would be 0 · k°(y), and the bound is pairing_nonpos_of_gauge_eq_zero.

theorem Tdaf.ConvexAnalysis.conj_monotoneComp_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : ℝ → EReal} {k : E → EReal} {y : F} {c : ℝ} (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hc : polarGauge B k y = ↑c) : conj B (monotoneComp g k) y ≤ monotoneConj g c

The ≤ half of the conjugacy formula, at a point where the polar gauge is finite.

The supremum over x is regrouped by the level ζ = k x, and on each level the pairing is bounded by pairing_le_mul_of_gauge.

theorem Tdaf.ConvexAnalysis.conj_monotoneComp {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : ℝ → EReal} {k : E → EReal} (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) : conj B (monotoneComp g k) = monotoneComp (monotoneConj g) (polarGauge B k)

The conjugacy formula: for a closed gauge k and a nondecreasing closed convex g on the half-line that is finite at some positive level, the conjugate of g ∘ k is g⁺ ∘ k°.

The finiteness hypothesis is used only where k°(y) = +∞, to force the conjugate to be +∞ there; both halves of the finite case hold without it. It cannot be dropped: for g the indicator of {0} the left-hand side is δ*(· ∣ {k ≤ 0}), which vanishes on the polar of the recession cone of {k ≤ 1}, while the right-hand side is +∞ off the barrier cone of {k ≤ 1}, and those two cones differ.

Neither compatibility nor continuity of the pairing is needed, and g need not be non-constant; the topology on E enters only through the closedness of k.

g ∘ k is a closed proper convex function

Closedness is obtained the way the book obtains it: by applying the conjugacy formula twice. (g ∘ k)** = g⁺⁺ ∘ k°° = g ∘ k, and a convex function equal to its own biconjugate is closed. The second application needs g⁺ to be finite somewhere on the positive axis, which is exactly what g non-constant provides.

theorem Tdaf.ConvexAnalysis.closedFn_monotoneComp {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {g : ℝ → EReal} {k : E → EReal} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] [IsContinuousPairing B.flip] (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) : ClosedFn (monotoneComp g k)

g ∘ k is closed, for a closed gauge k and a non-constant nondecreasing closed convex g on the half-line finite at some positive level.

Non-constancy is essential and is exactly what the proof consumes, through MonotoneHalfLineFn.exists_monotoneConj_ne_top: for constant g the composite is g 0 on dom k and +∞ off it, and dom k need not be closed.

theorem Tdaf.ConvexAnalysis.closedProperConvexFn_monotoneComp {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {g : ℝ → EReal} {k : E → EReal} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] [IsContinuousPairing B.flip] (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) : ClosedProperConvexFn (monotoneComp g k)

g ∘ k is a closed proper convex function.

The powers of the half-line

ζ ↦ ζ^p / p for 1 < p < ∞. Under monotone conjugacy these functions are permuted by p ↦ q, the Hölder conjugate exponent; that is Young's inequality, read as a conjugacy.

noncomputable def Tdaf.ConvexAnalysis.powHalfLine (p : ℝ) : ℝ → EReal

The function ζ ↦ ζ^p / p of the half-line, extended by +∞ to the negative axis.

Equations

• Tdaf.ConvexAnalysis.powHalfLine p = Tdaf.ConvexAnalysis.restrict (Set.Ici 0) fun (ζ : ℝ) => ↑(ζ ^ p / p)

@[simp]

theorem Tdaf.ConvexAnalysis.powHalfLine_of_nonneg {ζ : ℝ} (p : ℝ) (hζ : 0 ≤ ζ) : powHalfLine p ζ = ↑(ζ ^ p / p)

theorem Tdaf.ConvexAnalysis.powHalfLine_of_neg {ζ : ℝ} (p : ℝ) (hζ : ζ < 0) : powHalfLine p ζ = ⊤

theorem Tdaf.ConvexAnalysis.powHalfLine_ne_top {ζ : ℝ} (p : ℝ) (hζ : 0 ≤ ζ) : powHalfLine p ζ ≠ ⊤

theorem Tdaf.ConvexAnalysis.powHalfLine_zero {p : ℝ} (hp : 0 < p) : powHalfLine p 0 = 0

theorem Tdaf.ConvexAnalysis.monotoneOn_powHalfLine {p : ℝ} (hp : 0 < p) : MonotoneOn (powHalfLine p) (Set.Ici 0)

ζ ↦ ζ^p / p is nondecreasing on the half-line.

theorem Tdaf.ConvexAnalysis.rpow_inv_rpow {p : ℝ} (hp : 0 < p) {z : ℝ} (hz : 0 ≤ z) : (z ^ p⁻¹) ^ p = z

Raising z^{1/p} back to the pth power returns z.

theorem Tdaf.ConvexAnalysis.rpow_rpow_inv {p : ℝ} (hp : 0 < p) {z : ℝ} (hz : 0 ≤ z) : (z ^ p) ^ p⁻¹ = z

Taking the 1/pth power of z^p returns z.

theorem Tdaf.ConvexAnalysis.rpow_inv_le_one_iff {p : ℝ} (hp : 0 < p) {z : ℝ} (hz : 0 ≤ z) : z ^ p⁻¹ ≤ 1 ↔ z ≤ 1

The 1/pth power does not move the unit level.

theorem Tdaf.ConvexAnalysis.monotoneHalfLineFn_powHalfLine {p : ℝ} (hp : 1 ≤ p) : MonotoneHalfLineFn (powHalfLine p)

ζ ↦ ζ^p / p is a nondecreasing closed convex function of the half-line, finite at the origin — the class on which monotone conjugacy is an involution.

theorem Tdaf.ConvexAnalysis.monotoneConj_powHalfLine {p q : ℝ} (hpq : p.HolderConjugate q) : monotoneConj (powHalfLine p) = powHalfLine q

Young's inequality, as a conjugacy: the monotone conjugate of ζ ↦ ζ^p / p is σ ↦ σ^q / q, for Hölder conjugate exponents p and q.

The supremum sup {ζ σ - ζ^p / p ∣ ζ ≥ 0} is bounded above by σ^q / q by Young's inequality and attained at ζ = σ^{q-1}, where ζ σ = ζ^p = σ^q.

Positive homogeneity of degree p

f (λ x) = λ^p f x for λ > 0. For 1 < p < ∞ these are exactly the functions (1/p) k^p of a closed gauge k, and the gauge is recovered as (p f)^{1/p}.

def Tdaf.ConvexAnalysis.PosHomogeneousDeg {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : ℝ) (f : E → EReal) : Prop

A function is positively homogeneous of degree p when f (λ • x) = λ^p f x for every λ > 0. Degree 1 is PosHomogeneous; as there, only positive scalars are constrained, so the value at the origin is not determined.

Equations

• Tdaf.ConvexAnalysis.PosHomogeneousDeg p f = ∀ (a : ℝ), 0 < a → ∀ (x : E), f (a • x) = ↑(a ^ p) * f x

theorem Tdaf.ConvexAnalysis.PosHomogeneousDeg.map_zero_trichotomy {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hf : PosHomogeneousDeg p f) : f 0 = 0 ∨ f 0 = ⊤ ∨ f 0 = ⊥

Positive homogeneity of positive degree leaves only three possible values at the origin.

theorem Tdaf.ConvexAnalysis.PosHomogeneousDeg.nonneg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {p : ℝ} (hp : 1 < p) (hconv : ConvexFn f) (hne : ∀ (z : E), f z ≠ ⊥) (hf : PosHomogeneousDeg p f) (h0 : f 0 = 0) (x : E) : 0 ≤ f x

A convex function positively homogeneous of degree p > 1 that vanishes at the origin is nonnegative. Convexity gives λ^p f x ≤ λ f x for 0 < λ < 1, and λ^p < λ there.

theorem Tdaf.ConvexAnalysis.posHomogeneousDeg_monotoneComp_powHalfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] {k : E → EReal} {p : ℝ} (hp : 0 < p) (hk : IsGauge k) : PosHomogeneousDeg p (monotoneComp (powHalfLine p) k)

The composite (1/p) k^p of a gauge is positively homogeneous of degree p.

noncomputable def Tdaf.ConvexAnalysis.degGauge {E : Type u_1} (p : ℝ) (f : E → EReal) : E → EReal

The gauge attached to a function positively homogeneous of degree p: (p f)^{1/p}, with (+∞)^{1/p} = +∞.

Written through monotoneComp so that the two defining equations come for free: it is (p a)^{1/p} where f takes the finite value a ≥ 0, and +∞ where f is.

Equations

• Tdaf.ConvexAnalysis.degGauge p f = Tdaf.ConvexAnalysis.monotoneComp (fun (a : ℝ) => ↑((p * a) ^ p⁻¹)) f

theorem Tdaf.ConvexAnalysis.monotoneOn_degGaugeFn {p : ℝ} (hp : 0 < p) : MonotoneOn (fun (a : ℝ) => ↑((p * a) ^ p⁻¹)) (Set.Ici 0)

theorem Tdaf.ConvexAnalysis.degGauge_of_eq_coe {E : Type u_1} {f : E → EReal} {x : E} {p : ℝ} (hp : 0 < p) {a : ℝ} (ha : 0 ≤ a) (h : f x = ↑a) : degGauge p f x = ↑((p * a) ^ p⁻¹)

theorem Tdaf.ConvexAnalysis.degGauge_of_eq_top {E : Type u_1} {f : E → EReal} {x : E} (p : ℝ) (h : f x = ⊤) : degGauge p f x = ⊤

theorem Tdaf.ConvexAnalysis.degGauge_nonneg {E : Type u_1} {f : E → EReal} {p : ℝ} (hp : 0 < p) (hnn : ∀ (z : E), 0 ≤ f z) (x : E) : 0 ≤ degGauge p f x

theorem Tdaf.ConvexAnalysis.degGauge_map_zero {E : Type u_1} [AddCommGroup E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (h0 : f 0 = 0) : degGauge p f 0 = 0

theorem Tdaf.ConvexAnalysis.posHomogeneous_degGauge {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hnn : ∀ (z : E), 0 ≤ f z) (hf : PosHomogeneousDeg p f) : PosHomogeneous (degGauge p f)

theorem Tdaf.ConvexAnalysis.setOf_degGauge_le_one {E : Type u_1} {f : E → EReal} {p : ℝ} (hp : 0 < p) (hnn : ∀ (z : E), 0 ≤ f z) : {x : E | degGauge p f x ≤ 1} = {x : E | f x ≤ ↑p⁻¹}

The unit level set of (p f)^{1/p} is the level set {f ≤ 1/p}.

theorem Tdaf.ConvexAnalysis.degGauge_eq_gaugeFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hnn : ∀ (z : E), 0 ≤ f z) (hf : PosHomogeneousDeg p f) (h0 : f 0 = 0) : degGauge p f = gaugeFn {x : E | f x ≤ ↑p⁻¹}

(p f)^{1/p} is the Minkowski functional of {f ≤ 1/p}.

theorem Tdaf.ConvexAnalysis.isGauge_degGauge {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hconv : ConvexFn f) (hnn : ∀ (z : E), 0 ≤ f z) (hf : PosHomogeneousDeg p f) (h0 : f 0 = 0) : IsGauge (degGauge p f)

(p f)^{1/p} is a gauge. Convexity is not proved from the formula but read off from the level set: (p f)^{1/p} is the Minkowski functional of the convex set {f ≤ 1/p}.

theorem Tdaf.ConvexAnalysis.monotoneComp_powHalfLine_degGauge {E : Type u_1} {f : E → EReal} {p : ℝ} (hp : 0 < p) (hnn : ∀ (z : E), 0 ≤ f z) : monotoneComp (powHalfLine p) (degGauge p f) = f

(1/p) [(p f)^{1/p}]^p = f: the gauge attached to a nonnegative function recovers it.

theorem Tdaf.ConvexAnalysis.degGauge_monotoneComp_powHalfLine {E : Type u_1} [AddCommGroup E] [Module ℝ E] {k : E → EReal} {p : ℝ} (hp : 0 < p) (hk : IsGauge k) : degGauge p (monotoneComp (powHalfLine p) k) = k

(p · (1/p) k^p)^{1/p} = k: the gauge is recovered from the composite, so the representation is unique.

Homogeneity of degree p for closed functions

Closedness is what pins the value at the origin, and with it the sign.

theorem Tdaf.ConvexAnalysis.PosHomogeneousDeg.map_zero_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) : f 0 = 0

A closed proper function positively homogeneous of degree p > 0 vanishes at the origin. Along a ray into the origin the values are λ^p f x₀ → 0, so the epigraph, being closed, contains (0, 0); of the three values homogeneity allows at the origin, only 0 is ≤ 0.

theorem Tdaf.ConvexAnalysis.closedFn_degGauge {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} {p : ℝ} (hp : 0 < p) (hconv : ConvexFn f) (hcl : ClosedFn f) (hnn : ∀ (z : E), 0 ≤ f z) (hf : PosHomogeneousDeg p f) (h0 : f 0 = 0) : ClosedFn (degGauge p f)

(p f)^{1/p} is a closed gauge, being the Minkowski functional of the closed convex set {f ≤ 1/p}.

theorem Tdaf.ConvexAnalysis.monotoneComp_powHalfLine_degGauge_eq_self {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} {p : ℝ} (hp : 1 < p) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) : monotoneComp (powHalfLine p) (degGauge p f) = f

The representation f = (1/p) [(p f)^{1/p}]^p of a closed proper convex function positively homogeneous of degree p.

theorem Tdaf.ConvexAnalysis.posHomogeneousDeg_iff_exists_isGauge {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} {p : ℝ} (hp : 1 < p) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) : PosHomogeneousDeg p f ↔ ∃ (k : E → EReal), IsGauge k ∧ ClosedFn k ∧ f = monotoneComp (powHalfLine p) k

A closed proper convex function is positively homogeneous of degree p ∈ (1, ∞) exactly when it is (1/p) k^p for a closed gauge k. The gauge is unique — it is (p f)^{1/p}, by degGauge_monotoneComp_powHalfLine.

Conjugacy for the homogeneous functions of degree p

Corollaries 15.3.1 and 15.3.2: [(1/p) k^p]* = (1/q) (k°)^q, the gauge (p f)^{1/p} is polar to (q f*)^{1/q}, and the two unit level sets {f ≤ 1/p} and {f* ≤ 1/q} are polar sets.

theorem Tdaf.ConvexAnalysis.conj_monotoneComp_powHalfLine {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {k : E → EReal} {p q : ℝ} (hpq : p.HolderConjugate q) (hk : IsGauge k) (hkc : ClosedFn k) : conj B (monotoneComp (powHalfLine p) k) = monotoneComp (powHalfLine q) (polarGauge B k)

[(1/p) k^p]* = (1/q) (k°)^q.

theorem Tdaf.ConvexAnalysis.setOf_polarGauge_le_one {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {k : E → EReal} (hk : IsGauge k) : {y : F | polarGauge B k y ≤ 1} = polarSet B {x : E | k x ≤ 1}

The unit level set of a polar gauge is the polar set of the unit level set.

theorem Tdaf.ConvexAnalysis.conj_eq_monotoneComp_powHalfLine {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {p q : ℝ} (hpq : p.HolderConjugate q) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) : conj B f = monotoneComp (powHalfLine q) (polarGauge B (degGauge p f))

The conjugate of a closed proper convex function positively homogeneous of degree p is (1/q) (k°)^q for the gauge k = (p f)^{1/p} — in particular it is positively homogeneous of degree q.

theorem Tdaf.ConvexAnalysis.polarGauge_degGauge {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {p q : ℝ} (hpq : p.HolderConjugate q) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) : polarGauge B (degGauge p f) = degGauge q (conj B f)

(p f)^{1/p} is a closed gauge whose polar is (q f*)^{1/q}.

theorem Tdaf.ConvexAnalysis.pairing_le_rpow_mul_rpow {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {y : F} {p q : ℝ} (hpq : p.HolderConjugate q) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) {a b : ℝ} (hx : f x = ↑a) (hy : conj B f y = ↑b) : (B x) y ≤ (p * a) ^ p⁻¹ * (q * b) ^ q⁻¹

The Hölder-type inequality ⟨x, y⟩ ≤ [p f(x)]^{1/p} [q f*(y)]^{1/q} on dom f × dom f*.

theorem Tdaf.ConvexAnalysis.polarSet_setOf_le_inv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {p q : ℝ} (hpq : p.HolderConjugate q) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) (hf : PosHomogeneousDeg p f) : polarSet B {x : E | f x ≤ ↑p⁻¹} = {y : F | conj B f y ≤ ↑q⁻¹}

The closed convex sets {f ≤ 1/p} and {f* ≤ 1/q} are polar to each other.

Gauge-like functions, and the converse half

f is gauge-like when f 0 = inf f and the sublevel sets {f ≤ α} above that infimum are all positive multiples of one set. setOf_monotoneComp_le_eq_smul says that g ∘ k is gauge-like; here is the converse, that a gauge-like closed proper convex function is such a composite.

The gauge is the gauge of one sublevel set, k = γ(· | {f ≤ f 0 + 1}), and then every sublevel set of f is a sublevel set of k (IsGaugeLike.exists_isGauge_setOf_le_eq); so f x depends on x only through k x. The half-line factor is read off along a ray, g ζ = f (ζ • x₁) with k x₁ = 1, which makes g convex and closed for free. Such a ray exists unless k takes only the values 0 and +∞ — unless the sublevel sets are a single cone — in which case f is f 0 on that cone and +∞ off it, and the half-line factor is the step function f 0 + δ(· | [0, 1]).

structure Tdaf.ConvexAnalysis.IsGaugeLike {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : Prop

A gauge-like function, Rockafellar's term: the infimum of f is attained at the origin, and the sublevel sets strictly above that infimum are all positive multiples of a single set.

• map_zero_eq_iInf : f 0 = ⨅ (x : E), f x

  The infimum of f is attained at the origin.

• exists_setOf_le_eq_smul : ∃ (C : Set E), ∀ (α : ℝ), f 0 < ↑α → ∃ (l : ℝ), 0 < l ∧ {x : E | f x ≤ ↑α} = l • C

  The sublevel sets above the infimum are proportional to one another.

theorem Tdaf.ConvexAnalysis.IsGaugeLike.map_zero_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hgl : IsGaugeLike f) (x : E) : f 0 ≤ f x

The origin minimises a gauge-like function.

theorem Tdaf.ConvexAnalysis.IsGaugeLike.exists_setOf_le_eq_smul_setOf_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hgl : IsGaugeLike f) {α β : ℝ} (hα : f 0 < ↑α) (hβ : f 0 < ↑β) : ∃ (c : ℝ), 0 < c ∧ {x : E | f x ≤ ↑α} = c • {x : E | f x ≤ ↑β}

Any two sublevel sets above the infimum are positive multiples of each other — the form the reconstruction uses, with no reference to the auxiliary set.

theorem Tdaf.ConvexAnalysis.IsGaugeLike.exists_map_zero_eq_coe {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hgl : IsGaugeLike f) (hpr : Proper f) : ∃ (a : ℝ), f 0 = ↑a

f 0 is a real number, for a proper gauge-like f: it is finite below by properness, and above because it is bounded by any value in the effective domain.

theorem Tdaf.ConvexAnalysis.le_of_forall_setOf_le_eq {E : Type u_1} {f k : E → EReal} {a₀ : ℝ} (hbot : ∀ (x : E), f x ≠ ⊥) (hmin : ∀ (x : E), ↑a₀ ≤ f x) (hlev : ∀ (α : ℝ), a₀ < α → ∃ (c : ℝ), 0 < c ∧ {x : E | f x ≤ ↑α} = {x : E | k x ≤ ↑c}) (u v : E) (huv : k u ≤ k v) : f u ≤ f v

f is a nondecreasing function of k. If every sublevel set of f above its infimum a₀ is a sublevel set of k, then k u ≤ k v forces f u ≤ f v.

theorem Tdaf.ConvexAnalysis.eq_top_of_forall_setOf_le_eq {E : Type u_1} {f k : E → EReal} {a₀ : ℝ} (hbot : ∀ (x : E), f x ≠ ⊥) (hmin : ∀ (x : E), ↑a₀ ≤ f x) (hlev : ∀ (α : ℝ), a₀ < α → ∃ (c : ℝ), 0 < c ∧ {x : E | f x ≤ ↑α} = {x : E | k x ≤ ↑c}) (u : E) (hu : k u = ⊤) : f u = ⊤

f is +∞ wherever k is. Same hypotheses as le_of_forall_setOf_le_eq: a finite value of f at u would put u in a sublevel set of k.

theorem Tdaf.ConvexAnalysis.IsGauge.exists_eq_one_or_forall_eq_zero_or_eq_top {E : Type u_1} [AddCommGroup E] [Module ℝ E] {k : E → EReal} (hk : IsGauge k) : (∃ (x₁ : E), k x₁ = 1) ∨ ∀ (x : E), k x = 0 ∨ k x = ⊤

A gauge either takes the value 1 somewhere — supplying Rockafellar's ray — or takes only the values 0 and +∞, in which case its sublevel sets are a single cone.

theorem Tdaf.ConvexAnalysis.IsGaugeLike.exists_isGauge_setOf_le_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} (hgl : IsGaugeLike f) (hconv : ConvexFn f) (hcl : ClosedFn f) {a₀ : ℝ} (h0 : f 0 = ↑a₀) : ∃ (k : E → EReal), IsGauge k ∧ ClosedFn k ∧ ∀ (α : ℝ), a₀ < α → ∃ (c : ℝ), 0 < c ∧ {x : E | f x ≤ ↑α} = {x : E | k x ≤ ↑c}

The gauge attached to a gauge-like function: the gauge of one sublevel set, of which every sublevel set of f above the infimum is again a sublevel set.

theorem Tdaf.ConvexAnalysis.IsGaugeLike.exists_eq_monotoneComp {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → EReal} (hgl : IsGaugeLike f) (hconv : ConvexFn f) (hcl : ClosedFn f) (hpr : Proper f) : ∃ (g : ℝ → EReal) (k : E → EReal), MonotoneHalfLineFn g ∧ (∃ (t : ℝ), 0 < t ∧ g 0 < g t) ∧ (∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) ∧ IsGauge k ∧ ClosedFn k ∧ f = monotoneComp g k

The converse half: a gauge-like closed proper convex function is g ∘ k for a closed gauge k and a non-constant nondecreasing closed convex function g of the half-line that is finite at some positive level.

theorem Tdaf.ConvexAnalysis.isGaugeLike_monotoneComp {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {g : ℝ → EReal} {k : E → EReal} (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) : IsGaugeLike (monotoneComp g k)

The forward half, in the packaging the converse produces: g ∘ k is gauge-like. This is setOf_monotoneComp_le_eq_smul with the auxiliary set named.

The characterisation of gauge-like functions

The two halves, assembled. The pairing enters only through the forward implication, where closedness of g ∘ k comes from Fenchel–Moreau.

theorem Tdaf.ConvexAnalysis.isGaugeLike_conj_monotoneComp {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B.flip] {g : ℝ → EReal} {k : E → EReal} (hk : IsGauge k) (hkc : ClosedFn k) (hg : MonotoneHalfLineFn g) (hfin : ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) (hne : ∃ (t : ℝ), 0 < t ∧ g 0 < g t) : IsGaugeLike (conj B (monotoneComp g k))

The conjugate of a gauge-like closed proper convex function is gauge-like too. conj_monotoneComp says which composite it is; what has to be checked is that g⁺ satisfies the same two side conditions as g, and conjugacy exchanges them — g finite at a positive level makes g⁺ non-constant, and g non-constant makes g⁺ finite at a positive level.

theorem Tdaf.ConvexAnalysis.closedProperConvexFn_and_isGaugeLike_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {f : E → EReal} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] [IsContinuousPairing B.flip] : ClosedProperConvexFn f ∧ IsGaugeLike f ↔ ∃ (g : ℝ → EReal) (k : E → EReal), (MonotoneHalfLineFn g ∧ (∃ (t : ℝ), 0 < t ∧ g 0 < g t) ∧ ∃ (ζ : ℝ), 0 < ζ ∧ g ζ ≠ ⊤) ∧ (IsGauge k ∧ ClosedFn k) ∧ f = monotoneComp g k

A function is a gauge-like closed proper convex function exactly when it is g ∘ k for a closed gauge k and a non-constant nondecreasing closed convex function g of the half-line which is finite at some positive level.

The conjugacy formula that accompanies the theorem is conj_monotoneComp, (g ∘ k)* = g⁺ ∘ k°; it needs neither the pairing hypotheses of the forward implication nor non-constancy.