theorem polarGauge_innerMulGauge_le_j_on_J {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (j_nonneg : ∀ (y : ↑J), 0 ≤ j y) (j_ne_top : ∀ (y : ↑J), j y ≠ ⊤) (y : ↑J) : polarGauge (innerMulGauge j) ↑y ≤ j y ∧ polarGauge (innerMulGauge j) ↑y ≠ ⊤

The polar gauge of innerMulGauge is bounded by j on J.

theorem exists_closedGauge_of_inner_le_mul {n : ℕ} {H J : Set (Fin n → ℝ)} (h : ↑H → EReal) (j : ↑J → EReal) (h_nonneg : ∀ (x : ↑H), 0 ≤ h x) (h_ne_top : ∀ (x : ↑H), h x ≠ ⊤) (j_nonneg : ∀ (y : ↑J), 0 ≤ j y) (j_ne_top : ∀ (y : ↑J), j y ≠ ⊤) (hineq : ∀ (x : ↑H) (y : ↑J), ↑(↑x ⬝ᵥ ↑y) ≤ h x * j y) : have k := innerMulGauge j; (IsGauge k ∧ IsClosed (epigraph Set.univ k)) ∧ (∀ (x : Fin n → ℝ), k x ≠ ⊤ → ∀ (y : ↑J), ↑(x ⬝ᵥ ↑y) ≤ k x * j y) ∧ (∀ (x : ↑H), k ↑x ≠ ⊤) ∧ (∀ (x : ↑H), k ↑x ≤ h x) ∧ (∀ (y : ↑J), polarGauge k ↑y ≠ ⊤) ∧ (∀ (y : ↑J), polarGauge k ↑y ≤ j y) ∧ ∀ (x y : Fin n → ℝ), k x ≠ ⊤ → polarGauge k y ≠ ⊤ → ↑(x ⬝ᵥ y) ≤ k x * polarGauge k y

Text 15.0.10: Given subsets H, J ⊆ ℝⁿ and functions h : H → [0, +∞], j : J → [0, +∞] such that ⟪x, y⟫ ≤ h x * j y for all x ∈ H, y ∈ J, define k(x) := inf { μ ≥ 0 | ⟪x, y⟫ ≤ μ * j y for all y ∈ J }.

Then k is a closed gauge and satisfies ⟪x, y⟫ ≤ k x * j y for all x ∈ dom k, y ∈ J, with dom k ⊇ H and k x ≤ h x for all x ∈ H. Moreover, its polar gauge k^∘ satisfies dom k^∘ ⊇ J and k^∘ y ≤ j y for all y ∈ J, hence ⟪x, y⟫ ≤ k x * k^∘ y for all x ∈ dom k, y ∈ dom k^∘.

In this development, ℝⁿ is Fin n → ℝ, [0, +∞] is modeled by EReal with nonnegativity, and effective-domain assumptions are modeled by k x ≠ ⊤.

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

Text 15.0.11: Let k(x) = ‖x‖₂ be the Euclidean norm on ℝⁿ. Then k is both the gauge function and the support function of the Euclidean unit ball B = {x | ‖x‖₂ ≤ 1}. In particular, the polar gauge satisfies k^∘ = k. Consequently, the inequality associated with the polar pair (k, k^∘) is the Schwarz inequality

⟪x, y⟫ ≤ ‖x‖₂ ‖y‖₂ for all x, y ∈ ℝⁿ.

In this development, we work with Fin n → ℝ for ℝⁿ, define ‖x‖₂ as Real.sqrt (dotProduct x x), take the unit ball to be {x | Real.sqrt (dotProduct x x) ≤ 1}, and use gaugeFunction and supportFunctionEReal for the gauge and support functions.

Equations

• euclideanNormEReal x = ↑√(x ⬝ᵥ x)

def piEuclideanUnitBall (n : ℕ) : Set (Fin n → ℝ)

Equations

• piEuclideanUnitBall n = {x : Fin n → ℝ | √(x ⬝ᵥ x) ≤ 1}

theorem exists_unitBall_smul_eq {n : ℕ} (x : Fin n → ℝ) : ∃ y ∈ piEuclideanUnitBall n, x = √(x ⬝ᵥ x) • y

Every vector can be written as its Euclidean norm times a unit-ball vector.

theorem piEuclideanUnitBall_absorbing {n : ℕ} (x : Fin n → ℝ) : ∃ (r : ℝ), 0 ≤ r ∧ ∃ y ∈ piEuclideanUnitBall n, x = r • y

The Euclidean unit ball is absorbing.

theorem euclideanNormEReal_eq_gaugeFunction_euclideanUnitBall {n : ℕ} : euclideanNormEReal = fun (x : Fin n → ℝ) => ↑(gaugeFunction (piEuclideanUnitBall n) x)

theorem euclideanNormEReal_eq_supportFunctionEReal_euclideanUnitBall {n : ℕ} : euclideanNormEReal = supportFunctionEReal (piEuclideanUnitBall n)

theorem dotProduct_le_mul_sqrt_dotProduct_self {n : ℕ} (x y : Fin n → ℝ) : x ⬝ᵥ y ≤ √(x ⬝ᵥ x) * √(y ⬝ᵥ y)

def IsNormGauge {n : ℕ} (k : (Fin n → ℝ) → EReal) : Prop

Text 15.0.12: A gauge k : ℝⁿ → [0, +∞) is called a norm if it is finite everywhere, symmetric (k (-x) = k x for all x), and satisfies k x > 0 for all x ≠ 0.

Equivalently, k is real-valued and satisfies: (a) k x > 0 for all x ≠ 0; (b) k (x₁ + x₂) ≤ k x₁ + k x₂ for all x₁, x₂; (c) k (λ • x) = λ * k x for all x and all λ > 0; (d) k (-x) = k x for all x.

In particular, (c) and (d) imply k (λ • x) = |λ| * k x for all x and all λ ∈ ℝ.

In this development, ℝⁿ is Fin n → ℝ, codomain is EReal, and "finite everywhere" is ∀ x, k x ≠ ⊤.

Equations

• IsNormGauge k = (IsGauge k ∧ (∀ (x : Fin n → ℝ), k x ≠ ⊤) ∧ (∀ (x : Fin n → ℝ), k (-x) = k x) ∧ ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x)

theorem IsNormGauge.smul_eq_abs {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsNormGauge k) (x : Fin n → ℝ) (r : ℝ) : k (r • x) = ↑|r| * k x

def epigraph_isConvexCone_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : ConvexCone ℝ ((Fin n → ℝ) × ℝ)

The epigraph of a gauge is a convex cone in ℝⁿ × ℝ.

Equations

• epigraph_isConvexCone_of_isGauge hk = { carrier := epigraph Set.univ k, smul_mem' := ⋯, add_mem' := ⋯ }

theorem kCl_eq_epigraphClosureInf {n : ℕ} (k : (Fin n → ℝ) → EReal) : (fun (x : Fin n → ℝ) => sInf {μ : EReal | ∃ (r : ℝ), μ = ↑r ∧ (x, r) ∈ closure (epigraph Set.univ k)}) = epigraphClosureInf k

The closure-slice infimum used in Theorem 15.1 matches epigraphClosureInf.

theorem supportFunctionEReal_le_polarGauge_of_gaugeFunction {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : supportFunctionEReal C xStar ≤ polarGauge (fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) xStar

The support function is bounded above by the polar gauge of a gauge-function.

theorem supportFunctionEReal_nonneg_of_absorbing {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCabs : ∀ (x : Fin n → ℝ), ∃ (r : ℝ), 0 ≤ r ∧ ∃ y ∈ C, x = r • y) (xStar : Fin n → ℝ) : 0 ≤ supportFunctionEReal C xStar

The support function of an absorbing set is nonnegative.

theorem polarGauge_of_gaugeFunction_le_supportFunctionEReal {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCabs : ∀ (x : Fin n → ℝ), ∃ (r : ℝ), 0 ≤ r ∧ ∃ y ∈ C, x = r • y) (xStar : Fin n → ℝ) : polarGauge (fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) xStar ≤ supportFunctionEReal C xStar

The polar gauge of a gauge-function is bounded above by the support function under absorbing.

theorem polarGauge_euclideanNormEReal {n : ℕ} : polarGauge euclideanNormEReal = euclideanNormEReal

theorem signflip_euclidean_involutive {n : ℕ} : let E₂ := EuclideanSpace ℝ (Fin n); let H₂ := E₂ × ℝ; have σ₂ := fun (p : H₂) => (-p.1, p.2); ∀ (p : H₂), σ₂ (σ₂ p) = p

The sign-flip on the first coordinate of EuclideanSpace × ℝ is an involution.

theorem inner_signflip_H2 {n : ℕ} : let E₂ := EuclideanSpace ℝ (Fin n); let H₂ := WithLp 2 (E₂ × ℝ); have σ₂ := fun (p : H₂) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2); ∀ (p q : H₂), inner ℝ (σ₂ p) q = inner ℝ p (σ₂ q)

The inner product commutes with the sign-flip on the first coordinate in H₂.

theorem innerDual_preimage_signflip {n : ℕ} (A : Set (WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ))) : ↑(ProperCone.innerDual ((fun (p : WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ)) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2)) ⁻¹' A)) = (fun (p : WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ)) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2)) ⁻¹' ↑(ProperCone.innerDual A)

The inner dual cone commutes with sign-flip on the first coordinate in WithLp 2 (E × ℝ).

noncomputable def eH_transport_to_H2 (n : ℕ) : WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ) ≃L[ℝ] (Fin n → ℝ) × ℝ

Continuous linear equivalence between the inner-product model H₂ and ((Fin n → ℝ) × ℝ).

Equations

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

theorem mem_epigraph_snd_nonneg_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) {x : Fin n → ℝ} {r : ℝ} (hx : (x, r) ∈ epigraph Set.univ k) : 0 ≤ r

Epigraph points of a gauge have nonnegative second coordinate.

theorem signflip_H2_involutive {n : ℕ} : let E₂ := EuclideanSpace ℝ (Fin n); let H₂ := WithLp 2 (E₂ × ℝ); have σ₂ := fun (p : H₂) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2); ∀ (p : H₂), σ₂ (σ₂ p) = p

The sign-flip on the first coordinate of H₂ is an involution.

theorem isClosed_innerDual_H2 {n : ℕ} (S : Set (WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ))) : IsClosed ↑(ProperCone.innerDual S)

The inner dual cone in H₂ is closed.

theorem eH_transport_to_H2_symm_apply {n : ℕ} (x : Fin n → ℝ) (r : ℝ) : have eH := eH_transport_to_H2 n; eH.symm (x, r) = WithLp.toLp 2 (WithLp.toLp 2 x, r)

Explicit formula for the inverse of eH_transport_to_H2.

theorem inner_eH_symm_signflip {n : ℕ} (x xStar : Fin n → ℝ) (r μ : ℝ) : inner ℝ ((eH_transport_to_H2 n).symm (x, r)) ((fun (p : WithLp 2 (EuclideanSpace ℝ (Fin n) × ℝ)) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2)) ((eH_transport_to_H2 n).symm (xStar, μ))) = -(x ⬝ᵥ xStar) + r * μ

Inner product formula for the transported sign-flip in H₂.