theorem lpNormEReal_isClosedGauge_and_polar {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : have k := lpNormEReal p; have kPolar := lpNormEReal q; IsClosedGauge k ∧ polarGauge k = kPolar ∧ polarGauge kPolar = k ∧ IsNormGauge k ∧ IsNormGauge kPolar

theorem matrix_quadraticHalf_eq_quadraticHalfLinear {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) : (fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x)) = quadraticHalfLinear n (Matrix.toLin' Q)

Rewrite the quadratic form using quadraticHalfLinear and Matrix.toLin'.

theorem matrix_quadratic_posHomogeneous {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) : PositivelyHomogeneousOfDegree 2 fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x)

The quadratic form is positively homogeneous of degree 2.

theorem matrix_quadratic_closedConvex_and_proper {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQpos : Q.PosDef) : (ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x)) ∧ ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x)

The quadratic form from a positive definite matrix is closed, convex, and proper.

theorem fenchelConjugate_matrix_quadraticHalf_of_posDef {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) : (fenchelConjugate n fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x)) = fun (xStar : Fin n → ℝ) => ↑(1 / 2) * ↑(xStar ⬝ᵥ Q⁻¹.mulVec xStar)

The Fenchel conjugate of the quadratic form under positive definiteness.

theorem matrix_quadratic_closedProperConvex_and_fenchelConjugate {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) : have f := fun (x : Fin n → ℝ) => ↑(1 / 2) * ↑(x ⬝ᵥ Q.mulVec x); ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ fenchelConjugate n f = fun (xStar : Fin n → ℝ) => ↑(1 / 2) * ↑(xStar ⬝ᵥ Q⁻¹.mulVec xStar)

Text 15.0.25: Let Q be a symmetric positive definite n × n matrix and define f(x) = (1/2) * ⟪x, Q x⟫. Then f is a closed proper convex function on ℝⁿ and its Fenchel conjugate satisfies f^*(x⋆) = (1/2) * ⟪x⋆, Q⁻¹ x⋆⟫.

Since f is positively homogeneous of degree 2, Corollary 15.3.2 implies that k(x) = ⟪x, Q x⟫^{1/2} is a closed gauge (in fact, a norm) whose polar is k^∘(x⋆) = ⟪x⋆, Q⁻¹ x⋆⟫^{1/2}.

theorem matrix_quadraticGauge_isClosedGauge_isNormGauge_and_polar {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have kStar := fun (xStar : Fin n → ℝ) => ↑√(xStar ⬝ᵥ Q⁻¹.mulVec xStar); IsClosedGauge k ∧ IsNormGauge k ∧ polarGauge k = kStar

Text 15.0.25 (gauge/polar): with Q symmetric positive definite, the map k(x) = ⟪x, Q x⟫^{1/2} is a closed norm gauge and kᵒ(x⋆) = ⟪x⋆, Q⁻¹ x⋆⟫^{1/2}.

theorem matrix_quadraticSublevel_eq_unitSublevel_sqrt {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) : {x : Fin n → ℝ | x ⬝ᵥ Q.mulVec x ≤ 1} = {x : Fin n → ℝ | ↑√(x ⬝ᵥ Q.mulVec x) ≤ 1}

The quadratic sublevel set agrees with the unit sublevel of its square-root gauge.

theorem matrix_quadraticInvSublevel_eq_unitSublevel_sqrt {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) : {xStar : Fin n → ℝ | ↑√(xStar ⬝ᵥ Q⁻¹.mulVec xStar) ≤ 1} = {xStar : Fin n → ℝ | xStar ⬝ᵥ Q⁻¹.mulVec xStar ≤ 1}

The inverse quadratic sublevel set agrees with the unit sublevel of its square-root gauge.

theorem matrix_quadraticSublevel_polar {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) : have C := {x : Fin n → ℝ | x ⬝ᵥ Q.mulVec x ≤ 1}; {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1} = {xStar : Fin n → ℝ | xStar ⬝ᵥ Q⁻¹.mulVec xStar ≤ 1}

Text 15.0.26: Let Q be a symmetric positive definite n × n matrix. Define the convex set C = {x | ⟪x, Q x⟫ ≤ 1}. Then its polar (with respect to the pairing ⟪x, x⋆⟫) is C^∘ = {x⋆ | ⟪x⋆, Q⁻¹ x⋆⟫ ≤ 1}.

theorem ring_inverse_apply_of_isUnit {ι : Type u_1} (v : ι → ℝ) (hv : IsUnit v) (i : ι) : Ring.inverse v i = (v i)⁻¹

Ring.inverse on a unit-valued function agrees with pointwise inversion.

theorem polar_ellipticDisk_quadraticForm_diagonal_fun_fin2 (v x : Fin 2 → ℝ) : x ⬝ᵥ (Matrix.diagonal v).mulVec x = v 0 * x 0 ^ 2 + v 1 * x 1 ^ 2

Quadratic form of a diagonal matrix on Fin 2.

theorem polar_ellipticDisk_posDef_diagonal {α₁ α₂ : ℝ} (hα₁ : α₁ ≠ 0) (hα₂ : α₂ ≠ 0) : (Matrix.diagonal ![(α₁ ^ 2)⁻¹, (α₂ ^ 2)⁻¹]).PosDef

The diagonal matrix for the elliptic disk is positive definite.

theorem polar_ellipticDisk_quadraticForm_inv_diagonal_fin2 {α₁ α₂ : ℝ} (hα₁ : α₁ ≠ 0) (hα₂ : α₂ ≠ 0) (x : Fin 2 → ℝ) : have Q := Matrix.diagonal ![(α₁ ^ 2)⁻¹, (α₂ ^ 2)⁻¹]; x ⬝ᵥ Q⁻¹.mulVec x = α₁ ^ 2 * x 0 ^ 2 + α₂ ^ 2 * x 1 ^ 2

Quadratic form for the inverse diagonal matrix in the elliptic disk.

theorem polar_ellipticDisk {α₁ α₂ : ℝ} (hα₁ : α₁ ≠ 0) (hα₂ : α₂ ≠ 0) : have C := {x : Fin 2 → ℝ | x 0 ^ 2 / α₁ ^ 2 + x 1 ^ 2 / α₂ ^ 2 ≤ 1}; {xStar : Fin 2 → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1} = {xStar : Fin 2 → ℝ | α₁ ^ 2 * xStar 0 ^ 2 + α₂ ^ 2 * xStar 1 ^ 2 ≤ 1}

Text 15.0.27: Let C ⊆ ℝ² be the elliptic disk

C = {(ξ₁, ξ₂) | (ξ₁^2 / α₁^2) + (ξ₂^2 / α₂^2) ≤ 1}.

Then its polar set is the elliptic disk

C^∘ = {(ξ₁⋆, ξ₂⋆) | α₁^2 * (ξ₁⋆)^2 + α₂^2 * (ξ₂⋆)^2 ≤ 1}.

theorem matrix_quadraticGauge_comp_convex {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) (g : EReal → EReal) (hgζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (hg_mono : Monotone g) (hg_convex : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have f := fun (x : Fin n → ℝ) => g (k x); ConvexFunction f

Convexity of the composition g ∘ k for the quadratic norm gauge.

theorem matrix_quadraticGauge_comp_lowerSemicontinuous {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) (g : EReal → EReal) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have f := fun (x : Fin n → ℝ) => g (k x); LowerSemicontinuous f

Lower semicontinuity of g ∘ k from the closed epigraph of g.

theorem matrix_quadraticGauge_comp_proper {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) (g : EReal → EReal) (hgζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (hg_mono : Monotone g) (hg_convex : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have f := fun (x : Fin n → ℝ) => g (k x); ProperConvexFunctionOn Set.univ f

Properness of g ∘ k once g is finite at the origin.

theorem matrix_quadraticGauge_comp_fenchelConjugate {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) (g : EReal → EReal) (hgζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (hg_mono : Monotone g) (hg_top : g ⊤ = ⊤) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have f := fun (x : Fin n → ℝ) => g (k x); have kStar := fun (xStar : Fin n → ℝ) => ↑√(xStar ⬝ᵥ Q⁻¹.mulVec xStar); fenchelConjugate n f = fun (xStar : Fin n → ℝ) => monotoneConjugateERealNonneg g (kStar xStar)

Conjugate of g ∘ k for the quadratic norm gauge.

theorem matrix_quadraticGauge_comp_closedProperConvex_and_fenchelConjugate {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQsymm : Q.IsSymm) (hQpos : Q.PosDef) (g : EReal → EReal) (hgζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (hg_mono : Monotone g) (hg_convex : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) (hg_top : g ⊤ = ⊤) : have k := fun (x : Fin n → ℝ) => ↑√(x ⬝ᵥ Q.mulVec x); have f := fun (x : Fin n → ℝ) => g (k x); have kStar := fun (xStar : Fin n → ℝ) => ↑√(xStar ⬝ᵥ Q⁻¹.mulVec xStar); ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ fenchelConjugate n f = fun (xStar : Fin n → ℝ) => monotoneConjugateERealNonneg g (kStar xStar)

Text 15.0.28: Let Q be a symmetric positive definite matrix and define k(x) = ⟪x, Q x⟫^{1/2}. Let g : [0, +∞) → (-∞, +∞] satisfy the hypotheses of Theorem 15.3, and define f(x) = g(k(x)). Then f is a closed proper convex function and its conjugate satisfies f^*(x⋆) = g⁺(k^∘(x⋆)) = g⁺(⟪x⋆, Q⁻¹ x⋆⟫^{1/2}), where g⁺ is the monotone conjugate of g and k^∘ is the polar gauge of k.

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

Text 15.0.29: Let f : ℝⁿ → [0, +∞] be a convex function such that f 0 = 0. Its polar fᵒ : ℝⁿ → [0, +∞] is defined by

fᵒ x⋆ = inf { μ⋆ ≥ 0 | ⟪x, x⋆⟫ ≤ 1 + μ⋆ * f x for all x }.

If f is a gauge, this reduces to the polar gauge (Text 15.0.5). If f = δ(· | C) for a closed convex set C containing 0, then fᵒ = δ(· | Cᵒ). Furthermore, whenever x ∈ dom f and x⋆ ∈ dom fᵒ, one has ⟪x, x⋆⟫ ≤ 1 + f x * fᵒ x⋆.

In this development, we represent [0, +∞] by EReal together with explicit nonnegativity assumptions, and effective-domain assumptions by f x ≠ ⊤.

Equations

• polarConvex f xStar = sInf {μStar : EReal | 0 ≤ μStar ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ 1 + μStar * f x}

theorem polarConvex_feasible_imp_polarGauge_feasible_of_isGauge {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGauge f) {xStar : Fin n → ℝ} {μ : EReal} (hμ : 0 ≤ μ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ 1 + μ * f x) : 0 ≤ μ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ μ * f x

A polarConvex feasible multiplier is feasible for the polar gauge of a gauge.

theorem polarConvex_eq_polarGauge_of_isGauge {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGauge f) : polarConvex f = polarGauge f

Text 15.0.29 (gauge case): if f is a gauge, then its polar (as in polarConvex) agrees with the polar gauge polarGauge.

theorem polarConvex_erealIndicator_eq_erealIndicator_polar {n : ℕ} (C : Set (Fin n → ℝ)) : have Cpolar := {xStar : Fin n → ℝ | ∀ x ∈ C, ↑(x ⬝ᵥ xStar) ≤ 1}; polarConvex (erealIndicator C) = erealIndicator Cpolar

Text 15.0.29 (indicator case): if f = δ(· | C) for a closed convex set C containing 0, then fᵒ = δ(· | Cᵒ) where Cᵒ = {x⋆ | ∀ x ∈ C, ⟪x, x⋆⟫ ≤ 1}.

theorem inner_le_one_add_mul_polarConvex {n : ℕ} (f : (Fin n → ℝ) → EReal) (x xStar : Fin n → ℝ) (hx : f x ≠ ⊤) (hxStar : polarConvex f xStar ≠ ⊤) : ↑(x ⬝ᵥ xStar) ≤ 1 + f x * polarConvex f xStar

Text 15.0.29 (polar inequality): whenever x ∈ dom f and x⋆ ∈ dom fᵒ, ⟪x, x⋆⟫ ≤ 1 + f x * fᵒ x⋆.