noncomputable def polarConvexEquiv_nonneg_closedConvex_zero {n : ℕ} : { f : (Fin n → ℝ) → EReal // (∀ (x : Fin n → ℝ), 0 ≤ f x) ∧ ClosedConvexFunction f ∧ f 0 = 0 } ≃ { f : (Fin n → ℝ) → EReal // (∀ (x : Fin n → ℝ), 0 ≤ f x) ∧ ClosedConvexFunction f ∧ f 0 = 0 }

Corollary 15.4.1: The polarity mapping f ↦ fᵒ induces a symmetric one-to-one correspondence on the class of all nonnegative closed convex functions on ℝⁿ that vanish at the origin.

In this development, fᵒ is polarConvex f.

Equations

• One or more equations did not get rendered due to their size.

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

The obverse is the polar of the Fenchel conjugate under nonnegativity and closedness.

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

Nonnegativity and f 0 = 0 force the Fenchel conjugate to vanish at 0.

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

The polar of the obverse recovers the Fenchel conjugate.

theorem obverseConvex_zero_of_nonneg_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf0 : f 0 = 0) : obverseConvex f 0 = 0

The obverse vanishes at 0 under nonnegativity and f 0 = 0.

theorem obverseConvex_smul_le_coe_of_mul_le_one {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {t : ℝ} (ht : 0 < t) {y : Fin n → ℝ} : ↑t * f y ≤ 1 → obverseConvex f (t • y) ≤ ↑t

A feasible dilation inequality bounds the obverse at a scaled point.

theorem fenchelConjugate_obverseConvex_le_of_polar_feasible {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) {xStar : Fin n → ℝ} {μStar : EReal} (hμ : 0 ≤ μStar ∧ ∀ (y : Fin n → ℝ), ↑(y ⬝ᵥ xStar) ≤ 1 + μStar * f y) : fenchelConjugate n (obverseConvex f) xStar ≤ μStar

A polar-feasible μ⋆ bounds the Fenchel conjugate of the obverse.

theorem inner_le_one_add_mul_of_fenchelConjugate_obverse_of_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {xStar : Fin n → ℝ} {μ ε : ℝ} (hμ : fenchelConjugate n (obverseConvex f) xStar = ↑μ) (hε : 0 < ε) {y : Fin n → ℝ} {r : ℝ} (hfy : f y = ↑r) (hr : 0 < r) : ↑(y ⬝ᵥ xStar) ≤ 1 + ↑(μ + ε) * f y

Positive finite values of f yield a polar-feasible inner bound.

theorem inner_le_one_of_f_eq_zero_of_fenchelConjugate_obverse_finite {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {xStar : Fin n → ℝ} {μ : ℝ} (hμ : fenchelConjugate n (obverseConvex f) xStar = ↑μ) {y : Fin n → ℝ} (hfy : f y = 0) : ↑(y ⬝ᵥ xStar) ≤ 1

A zero value of f forces the inner product to be at most one.

theorem polar_feasible_of_fenchelConjugate_obverse_add_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {xStar : Fin n → ℝ} {μ ε : ℝ} (hμ : fenchelConjugate n (obverseConvex f) xStar = ↑μ) (hε : 0 < ε) : 0 ≤ ↑(μ + ε) ∧ ∀ (y : Fin n → ℝ), ↑(y ⬝ᵥ xStar) ≤ 1 + ↑(μ + ε) * f y

The Fenchel conjugate value yields a polar-feasible bound with μ + ε.

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

The polar is bounded above by the Fenchel conjugate of the obverse.

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

The Fenchel conjugate of the obverse is the polar (core symmetry).

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

The obverse of the Fenchel conjugate is the polar.

theorem obverseConvex_nonneg_closedConvex_zero_and_polar_eq_conjugate {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (hg : g = obverseConvex f) : (∀ (x : Fin n → ℝ), 0 ≤ g x) ∧ ClosedConvexFunction g ∧ g 0 = 0 ∧ obverseConvex g = f ∧ polarConvex f = fenchelConjugate n g ∧ fenchelConjugate n f = polarConvex g ∧ obverseConvex (polarConvex f) = fenchelConjugate n f ∧ obverseConvex (fenchelConjugate n f) = polarConvex f

Theorem 15.5: Let f be a nonnegative closed convex function with f(0)=0, and let g be the obverse of f.

Then g is also a nonnegative closed convex function with g(0)=0, and f is the obverse of g. Moreover,

f^∘ = g^* and f^* = g^∘,

and f^∘ and f^* are obverses of each other. In this development, the obverse is obverseConvex, the polar is polarConvex, and the Fenchel conjugate is fenchelConjugate n ·.

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

Corollary 15.5.1: If f is a nonnegative closed convex function on ℝⁿ with f(0)=0, then f^{∘*} = f^{*∘}; i.e. the Fenchel conjugate of the polar equals the polar of the Fenchel conjugate.

In this development, fᵒ is polarConvex f and f* is fenchelConjugate n f.

theorem obverseConvex_le_coe_pos_iff_f_le_inv {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {x : Fin n → ℝ} {α : ℝ} (hα : 0 < α) : obverseConvex f x ≤ ↑α ↔ f (α⁻¹ • x) ≤ ↑α⁻¹

Obverse sublevel inequality is equivalent to a reciprocal bound on f.

theorem sublevelSet_obverseConvex_eq_smul_sublevelSet {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (hg : g = obverseConvex f) {α : ℝ} (hα : 0 < α) : {x : Fin n → ℝ | g x ≤ ↑α} = α • {x : Fin n → ℝ | f x ≤ ↑α⁻¹}

Text 15.0.36: Let f be as in Theorem 15.5 and let g be its obverse. For α > 0, {x | g x ≤ α} = α • {x | f x ≤ α⁻¹}. In particular, the sublevel sets of g are homothetic to those of f with reciprocal levels.

theorem sublevelSet_polarConvex_le_inv_eq_inv_smul_sublevelSet_fenchelConjugate {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {α : ℝ} (hα : 0 < α) : {xStar : Fin n → ℝ | polarConvex f xStar ≤ ↑α⁻¹} = α⁻¹ • {xStar : Fin n → ℝ | fenchelConjugate n f xStar ≤ ↑α}

Text 15.0.36: Since polarConvex f is the obverse of fenchelConjugate n f (Theorem 15.5), for every α > 0, {x⋆ | polarConvex f x⋆ ≤ α⁻¹} = α⁻¹ • {x⋆ | fenchelConjugate n f x⋆ ≤ α}. The set on the left is the “middle” set appearing in Theorem 14.7.

theorem dilation_le_iff_scaled_le_one {lam mu : ℝ} (hmu : 0 < mu) (A : EReal) : ↑lam * A ≤ ↑mu ↔ ↑(lam / mu) * A ≤ 1

Normalize a dilation inequality in EReal to a ≤ 1 form.

theorem obverse_dilation_le_iff_obverse_le_div {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {lam mu : ℝ} (hmu : 0 < mu) : ↑mu * obverseConvex f (mu⁻¹ • x) ≤ ↑lam ↔ obverseConvex f (mu⁻¹ • x) ≤ ↑(lam / mu)

Divide a dilated obverse inequality by a positive scalar.

theorem inv_div_inv_smul_smul_eq_inv_smul {n : ℕ} {x : Fin n → ℝ} {lam mu : ℝ} (hmu : 0 < mu) : (lam / mu)⁻¹ • mu⁻¹ • x = lam⁻¹ • x

Combine reciprocal scalings in a nested smul.

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

Text 15.0.37: For the obverse g of f, one has (f_λ)(x) ≤ μ if and only if (g_μ)(x) ≤ λ, assuming λ > 0 and μ > 0.

Here f_λ x := λ * f (λ⁻¹ • x) and g_μ x := μ * g (μ⁻¹ • x).

theorem sublevelSet_obverseConvex_eq_sublevelSet_perspective {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (hg : g = obverseConvex f) {α : ℝ} (hα : 0 < α) : {x : Fin n → ℝ | g x ≤ ↑α} = {x : Fin n → ℝ | ↑α * f (α⁻¹ • x) ≤ 1}

Sublevel sets of the obverse match those of the perspective.

theorem sublevelSet_perspective_eq_smul_sublevelSet {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (hg : g = obverseConvex f) {α : ℝ} (hα : 0 < α) : {x : Fin n → ℝ | ↑α * f (α⁻¹ • x) ≤ 1} = α • {x : Fin n → ℝ | f x ≤ ↑α⁻¹}

Perspective sublevel sets are homothetic to those of f.

theorem sublevelSet_obverseConvex_eq_sublevelSet_dilation_eq_smul_sublevelSet {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (hg : g = obverseConvex f) {α : ℝ} (hα : 0 < α) : have fα := fun (x : Fin n → ℝ) => ↑α * f (α⁻¹ • x); {x : Fin n → ℝ | g x ≤ ↑α} = {x : Fin n → ℝ | fα x ≤ 1} ∧ {x : Fin n → ℝ | fα x ≤ 1} = α • {x : Fin n → ℝ | f x ≤ ↑α⁻¹}

Text 15.0.38: Let f : ℝⁿ → [0, +∞] be a nonnegative closed convex function with f 0 = 0, and let g be the obverse of f. For λ > 0 define (f_λ)(x) := λ * f (λ⁻¹ • x). Then for every α > 0, {x | g x ≤ α} = {x | (f_α) x ≤ 1} = α • {x | f x ≤ α⁻¹}.

theorem polarConvex_eq_obverseConvex_fenchelConjugate_and_sublevelSet {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) {α : ℝ} (hα : 0 < α) : polarConvex f = obverseConvex (fenchelConjugate n f) ∧ {xStar : Fin n → ℝ | polarConvex f xStar ≤ ↑α⁻¹} = α⁻¹ • {xStar : Fin n → ℝ | fenchelConjugate n f xStar ≤ ↑α}

Text 15.0.39: Let f : ℝⁿ → [0, +∞] be a nonnegative closed convex function with f 0 = 0. Then the polar f^∘ is the obverse of the Fenchel conjugate f*. Consequently, for every α > 0, {x⋆ | f^∘ x⋆ ≤ α⁻¹} = α⁻¹ • {x⋆ | f* x⋆ ≤ α}.

In this development, f^∘ is polarConvex f and f* is fenchelConjugate n f.