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

The gauge of a closed convex absorbing set containing 0 is a gauge.

theorem isClosed_epigraph_gaugeFunctionEReal_of_closed_convex_zeroMem_absorbing {n : ℕ} {C : Set (Fin n → ℝ)} (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : IsClosed (epigraph Set.univ fun (x : Fin n → ℝ) => ↑(gaugeFunction C x))

The gauge function of a closed convex absorbing set has closed epigraph.

theorem polarGauge_supportFunctionEReal_eq_gaugeFunctionEReal {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) (hγ : IsGauge fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) (hγclosed : IsClosed (epigraph Set.univ fun (x : Fin n → ℝ) => ↑(gaugeFunction C x))) : polarGauge (supportFunctionEReal C) = fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)

The polar gauge of the support function agrees with the gauge of the set.

theorem gaugeFunction_and_supportFunctionEReal_closedGauges_polar {n : ℕ} {C : Set (Fin n → ℝ)} (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : have γ := fun (x : Fin n → ℝ) => ↑(gaugeFunction C x); have δ := supportFunctionEReal C; (IsGauge γ ∧ IsClosed (epigraph Set.univ γ)) ∧ (IsGauge δ ∧ IsClosed (epigraph Set.univ δ)) ∧ polarGauge γ = δ ∧ polarGauge δ = γ

Corollary 15.1.2: If C ⊆ ℝ^n is a closed convex set containing 0, then the gauge γ(· | C) and the support function δ^*(· | C) are closed gauges polar to each other.

In this development, γ(· | C) is fun x => (gaugeFunction C x : EReal), the support function is supportFunctionEReal C, "closed" is expressed as IsClosed (epigraph univ ·), and polarity of gauges is given by polarGauge. We additionally assume C is absorbing.

theorem absorbing_of_zero_mem_interior {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hC0 : 0 ∈ interior C) (x : Fin n → ℝ) : ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C

If 0 lies in the interior of a convex set, then the set is absorbing.

theorem normGauge_continuous {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : Continuous k

A norm gauge is continuous on ℝ^n.

theorem normGauge_sublevel_one_closed {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : IsClosed {x : Fin n → ℝ | k x ≤ 1}

The unit sublevel set of a norm gauge is closed.

theorem normGauge_sublevel_one_zero_mem_interior {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : 0 ∈ interior {x : Fin n → ℝ | k x ≤ 1}

The unit sublevel set of a norm gauge contains the origin in its interior.

theorem normGauge_sublevel_one_recessionCone_eq_singleton_zero {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : {x : Fin n → ℝ | k x ≤ 1}.recessionCone = {0}

The recession cone of the unit sublevel set of a norm gauge is {0}.

theorem normGauge_sublevel_one_bounded {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : Bornology.IsBounded {x : Fin n → ℝ | k x ≤ 1}

The unit sublevel set of a norm gauge is bounded.

theorem normGauge_sublevelOne_symmClosedBoundedConvex {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : have C := {x : Fin n → ℝ | k x ≤ 1}; IsClosed C ∧ Convex ℝ C ∧ Bornology.IsBounded C ∧ 0 ∈ interior C ∧ ∀ x ∈ C, -x ∈ C

The unit sublevel set of a norm gauge is symmetric, closed, bounded, convex, and contains 0 in its interior.

theorem gaugeFunctionEReal_isNormGauge_of_symmClosedBoundedConvex_zeroInterior {n : ℕ} {C : Set (Fin n → ℝ)} (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (hC_bdd : Bornology.IsBounded C) (hC0 : 0 ∈ interior C) (hC_symm : ∀ x ∈ C, -x ∈ C) : IsNormGauge fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)

The gauge of a symmetric closed bounded convex set with 0 in its interior is a norm gauge.

theorem supportFunctionEReal_isNormGauge_of_symmClosedBoundedConvex_zeroInterior {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hC_conv : Convex ℝ C) (hC_bdd : Bornology.IsBounded C) (hC0 : 0 ∈ interior C) (hC_symm : ∀ x ∈ C, -x ∈ C) : IsNormGauge (supportFunctionEReal C)

The support function of a symmetric closed bounded convex set with 0 in its interior is a norm gauge.

theorem polarGauge_eq_supportFunctionEReal_unitSublevel {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : have C := {x : Fin n → ℝ | k x ≤ 1}; polarGauge k = supportFunctionEReal C

The polar gauge of a norm gauge is the support function of its unit sublevel set.

noncomputable def normGaugeEquiv_symmClosedBoundedConvex {n : ℕ} : { k : (Fin n → ℝ) → EReal // IsNormGauge k } ≃ { C : Set (Fin n → ℝ) // IsClosed C ∧ Convex ℝ C ∧ Bornology.IsBounded C ∧ 0 ∈ interior C ∧ ∀ x ∈ C, -x ∈ C }

Theorem 15.2: The relations k(x) = γ(x | C) and C = {x ∈ ℝ^n | k x ≤ 1} define a one-to-one correspondence between norms k on ℝ^n and symmetric closed bounded convex sets C ⊆ ℝ^n such that 0 ∈ interior C.

In this development, ℝ^n is Fin n → ℝ; the unit ball of k is {x | k x ≤ 1}; and γ(x | C) is represented by fun x => (gaugeFunction C x : EReal).

Equations

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

theorem polarGauge_isNormGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) : IsNormGauge (polarGauge k)

Theorem 15.2 (polar): Under the norm/set correspondence of Theorem 15.2, the polar of a norm is a norm. In this development, the polar of k is polarGauge k.

noncomputable def linftyNormEReal {n : ℕ} (x : Fin n → ℝ) : EReal

Text 15.0.13: Define k : ℝⁿ → [0, +∞) by k(x) = max {|ξ₁|, …, |ξₙ|} for x = (ξ₁, …, ξₙ).

Then k is a norm, and its polar gauge k^∘ is the ℓ₁-norm: k^∘(x⋆) = |ξ₁⋆| + ⋯ + |ξₙ⋆| for x⋆ = (ξ₁⋆, …, ξₙ⋆). Consequently, k and k^∘ form a polar pair of norms.

In this development, ℝⁿ is Fin n → ℝ, and we model real-valued norms as EReal-valued functions via coercion ℝ → EReal.

Equations

• linftyNormEReal x = ↑‖x‖

noncomputable def l1NormEReal {n : ℕ} (x : Fin n → ℝ) : EReal

Equations

• l1NormEReal x = ↑(∑ i : Fin n, |x i|)

theorem real_sign_mul_self_eq_abs (r : ℝ) : r.sign * r = |r|

The sign function satisfies sign r * r = |r|.

theorem abs_sign_le_one (r : ℝ) : |r.sign| ≤ 1

The absolute value of Real.sign is bounded by 1.

theorem supportFunctionEReal_linftyUnitBall_eq_l1NormEReal {n : ℕ} : have C := {x : Fin n → ℝ | ‖x‖ ≤ 1}; supportFunctionEReal C = l1NormEReal

The support function of the ℓ∞ unit ball is the ℓ1 norm.

theorem supportFunctionEReal_l1UnitBall_eq_linftyNormEReal {n : ℕ} : have C := {x : Fin n → ℝ | ∑ i : Fin n, |x i| ≤ 1}; supportFunctionEReal C = linftyNormEReal

The support function of the ℓ1 unit ball is the ℓ∞ norm.

theorem linftyNormEReal_isNormGauge {n : ℕ} : IsNormGauge linftyNormEReal

theorem polarGauge_linftyNormEReal {n : ℕ} : polarGauge linftyNormEReal = l1NormEReal

theorem polarGauge_l1NormEReal {n : ℕ} : polarGauge l1NormEReal = linftyNormEReal