theorem dotProduct_le_add_fenchelConjugate {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) (x y : Fin n → ℝ) : ↑(x ⬝ᵥ y) ≤ f x + fenchelConjugate n f y

Fenchel–Young inequality from the conjugate definition, using f 0 = 0.

theorem properConvexFunctionOn_of_nonneg_closedConvex_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : ProperConvexFunctionOn Set.univ f

Nonnegativity and f 0 = 0 give properness on univ for a closed convex function.

theorem fenchelConjugate_biconjugate_eq_of_nonneg_closedConvex_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : fenchelConjugate n (fenchelConjugate n f) = f

Biconjugation reduces to the original function under closedness and nonnegativity.

theorem fenchelConjugate_nonneg_of_nonneg_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf0 : f 0 = 0) (y : Fin n → ℝ) : 0 ≤ fenchelConjugate n f y

Nonnegativity and f 0 = 0 make the Fenchel conjugate nonnegative.

theorem dilation_le_one_pos_imp_polar_feasible {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) {x : Fin n → ℝ} {t : ℝ} (ht : 0 < t) (hle : ↑t * f (t⁻¹ • x) ≤ 1) (y : Fin n → ℝ) : ↑(y ⬝ᵥ x) ≤ 1 + ↑t * fenchelConjugate n f y

Dilation feasibility yields the polar inequality for a positive scale.

theorem polar_feasible_imp_dilation_le_one_pos {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {x : Fin n → ℝ} {t : ℝ} (ht : 0 < t) (hfeas : ∀ (y : Fin n → ℝ), ↑(y ⬝ᵥ x) ≤ 1 + ↑t * fenchelConjugate n f y) : ↑t * f (t⁻¹ • x) ≤ 1

Polar feasibility implies the dilation inequality for a positive scale.

theorem exists_dotProduct_gt_one_of_ne_zero {n : ℕ} {x : Fin n → ℝ} (hx : x ≠ 0) : ∃ (y : Fin n → ℝ), 1 < y ⬝ᵥ x

Nonzero vectors admit a dual witness with dot product exceeding 1.

theorem sInf_pos_real_eq_zero : have S := {μ : EReal | ∃ (t : ℝ), 0 < t ∧ μ = ↑t}; sInf S = 0

The infimum of positive real coefficients in EReal is zero.

theorem polarFenchelConjugate_eq_sInf_dilation_le_one {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : have g := polarConvex (fenchelConjugate n f); have fDil := fun (t : ℝ) (x : Fin n → ℝ) => ↑t * f (t⁻¹ • x); ∀ (x : Fin n → ℝ), g x = sInf {μ : EReal | ∃ (t : ℝ), 0 < t ∧ μ = ↑t ∧ fDil t x ≤ 1}

Text 15.0.31: Let f : ℝⁿ → [0, +∞] be a nonnegative closed convex function with f 0 = 0, and define g := f^{*∘}. For λ > 0, define the dilation f_λ x := λ * f (λ⁻¹ • x). Then for every x ∈ ℝⁿ one has the representation

g x = inf { λ > 0 | f_λ x ≤ 1 }.

In this development, we model [0, +∞] by EReal together with nonnegativity assumptions, define g as polarConvex (fenchelConjugate n f), and represent the infimum as sInf in EReal.

noncomputable def obverseConvex {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 15.0.32: Let f : ℝⁿ → [0, +∞] be a nonnegative closed convex function with f(0) = 0. For λ > 0, define the scaled (perspective) function f_λ x := λ * f (x / λ). The obverse of f is the function g : ℝⁿ → [0, +∞] given by g x := inf {λ > 0 | f_λ x ≤ 1}.

If f = δ(· | C) for a closed convex set C containing 0, then g = γ(· | C) is the gauge of C. If f = γ(· | C) is the gauge of such a set C, then g = δ(· | C). Thus the gauge and indicator functions of C are obverses of each other.

In this development, ℝⁿ is Fin n → ℝ, [0, +∞] is modeled by EReal with nonnegativity assumptions, δ(· | C) is erealIndicator C, and γ(· | C) is represented by fun x => (gaugeFunction C x : EReal).

Equations

• obverseConvex f x = sInf {μ : EReal | ∃ (t : ℝ), 0 < t ∧ μ = ↑t ∧ ↑t * f (t⁻¹ • x) ≤ 1}

theorem obverseConvex_erealIndicator_apply_simp {n : ℕ} {C : Set (Fin n → ℝ)} {t : ℝ} (ht : 0 < t) (x : Fin n → ℝ) : ↑t * erealIndicator C (t⁻¹ • x) ≤ 1 ↔ x ∈ t • C

The obverse constraint for an indicator reduces to scaled membership.

theorem obverseConvex_erealIndicator_eq_gaugeFunction {n : ℕ} (C : Set (Fin n → ℝ)) (h0C : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : obverseConvex (erealIndicator C) = fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)

Text 15.0.32 (indicator case): if f = δ(· | C) for a closed convex absorbing set C containing 0, then its obverse is γ(· | C).

theorem obverseConvex_gaugeFunction_eq_erealIndicator {n : ℕ} (C : Set (Fin n → ℝ)) (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (h0C : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : (obverseConvex fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) = erealIndicator C

Text 15.0.32 (gauge case): if f = γ(· | C) for a closed convex absorbing set C containing 0, then its obverse is δ(· | C).

theorem obverseConvex_set_eq_image_pos {n : ℕ} (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : {μ : EReal | ∃ (t : ℝ), 0 < t ∧ μ = ↑t ∧ ↑t * f (t⁻¹ • x) ≤ 1} = (fun (t : ℝ) => ↑t) '' {t : ℝ | 0 < t ∧ ↑t * f (t⁻¹ • x) ≤ 1}

The obverse sInf set is the image of its positive real parameters.

theorem obverseConvex_le_coe_pos_of_perspective_le_one {n : ℕ} (f : (Fin n → ℝ) → EReal) {t : ℝ} (ht : 0 < t) (x : Fin n → ℝ) (hle : ↑t * f (t⁻¹ • x) ≤ 1) : obverseConvex f x ≤ ↑t

Feasibility at a positive scalar gives an upper bound for the obverse.

theorem obverseConvex_nonneg {n : ℕ} (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : 0 ≤ obverseConvex f x

The obverse is always nonnegative.

theorem exists_lt_of_sInf_lt {S : Set ℝ} (hne : S.Nonempty) {a : ℝ} (h : sInf S < a) : ∃ s ∈ S, s < a

An element below a strict upper bound for sInf exists in a nonempty real set.

theorem mul_le_one_iff_le_inv_pos {t : ℝ} {a : EReal} (ht : 0 < t) (ha : 0 ≤ a) : ↑t * a ≤ 1 ↔ a ≤ (↑t)⁻¹

For positive t, scaling inequality is equivalent to a reciprocal bound.

theorem perspective_isUpperSet {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_conv : ConvexFunctionOn Set.univ f) (hf0 : f 0 = 0) {x : Fin n → ℝ} {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (hle : ↑s * f (s⁻¹ • x) ≤ 1) : ↑t * f (t⁻¹ • x) ≤ 1

Feasibility at a smaller scale implies feasibility at a larger scale.

theorem obverseConvex_le_coe_pos_iff_perspective_le_one {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {x : Fin n → ℝ} {lam : ℝ} (hlam : 0 < lam) : obverseConvex f x ≤ ↑lam ↔ ↑lam * f (lam⁻¹ • x) ≤ 1

Obverse at a positive scalar equals the perspective sublevel inequality.