theorem polarGauge_erealIndicator_eq_top_of_not_mem_Kpolar {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) {xStar : Fin n → ℝ} (hxStar : ¬∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0) : polarGauge (erealIndicator ↑K) xStar = ⊤

Outside the polar cone, the polar gauge of an indicator is ⊤.

theorem polarGauge_erealIndicator_eq_zero_of_mem_Kpolar {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) {xStar : Fin n → ℝ} (hxStar : ∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0) : polarGauge (erealIndicator ↑K) xStar = 0

On the polar cone, the polar gauge of an indicator is 0.

theorem kStar_eq_zero_of_mem_Kpolar {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) {xStar : Fin n → ℝ} (h0K : 0 ∈ ↑K) (hxStar : ∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0) : sSup (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - erealIndicator (↑K) x) = 0

On the polar cone, the conjugate of the indicator is 0.

theorem kStar_eq_top_of_not_mem_Kpolar {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) {xStar : Fin n → ℝ} (hxStar : ¬∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0) : sSup (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - erealIndicator (↑K) x) = ⊤

Outside the polar cone, the conjugate of the indicator is ⊤.

theorem polarGauge_erealIndicator_eq_conjugate_eq_erealIndicator_polarCone {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) (h0K : 0 ∈ ↑K) : have k := erealIndicator ↑K; have Kpolar := {xStar : Fin n → ℝ | ∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0}; have kStar := fun (xStar : Fin n → ℝ) => sSup (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - k x); polarGauge k = kStar ∧ polarGauge k = erealIndicator Kpolar

Text 15.0.7: Let K ⊆ ℝⁿ be a convex cone and let k = δ(· | K) be its indicator function. Then the polar kᵒ agrees with the conjugate k*, and it is the indicator of the polar cone Kᵒ := {x⋆ ∈ ℝⁿ | ⟪x, x⋆⟫ ≤ 0 for all x ∈ K}.

In this development, ℝⁿ is Fin n → ℝ, the indicator δ(· | K) is erealIndicator K, the polar kᵒ is polarGauge k, the conjugate k* is given by x⋆ ↦ sup_x (⟪x, x⋆⟫ - k x), and ⟪x, x⋆⟫ is x ⬝ᵥ x⋆.

noncomputable def gaugeSqrtSumSq_add_fst (x : Fin 2 → ℝ) : EReal

Text 15.0.8: Define k : ℝ² → [0, +∞) by k(ξ₁, ξ₂) = sqrt (ξ₁^2 + ξ₂^2) + ξ₁. Then k is a closed gauge function.

Its polar gauge k^∘ is given by the piecewise formula k^∘(ξ₁⋆, ξ₂⋆) = (1/2) * ((ξ₂⋆)^2 / ξ₁⋆ + ξ₁⋆) if 0 < ξ₁⋆, k^∘(0, 0) = 0, and k^∘(ξ₁⋆, ξ₂⋆) = +∞ otherwise.

Neither k nor k^∘ is a norm (e.g. neither is an even function).

Equations

• gaugeSqrtSumSq_add_fst x = ↑(√(x 0 ^ 2 + x 1 ^ 2) + x 0)

theorem gaugeSqrtSumSq_add_fst_eq_euclideanNorm_add_fst (x : Fin 2 → ℝ) : gaugeSqrtSumSq_add_fst x = ↑(‖(EuclideanSpace.equiv (Fin 2) ℝ).symm x‖ + x 0)

Rewrite gaugeSqrtSumSq_add_fst using the Euclidean norm on ℝ².

theorem gaugeSqrtSumSq_add_fst_convexFunctionOn : ConvexFunctionOn Set.univ gaugeSqrtSumSq_add_fst

Convexity of gaugeSqrtSumSq_add_fst on Set.univ.

theorem gaugeSqrtSumSq_add_fst_nonneg (x : Fin 2 → ℝ) : 0 ≤ gaugeSqrtSumSq_add_fst x

Nonnegativity of gaugeSqrtSumSq_add_fst.

theorem gaugeSqrtSumSq_add_fst_smul (x : Fin 2 → ℝ) (r : ℝ) (hr : 0 ≤ r) : gaugeSqrtSumSq_add_fst (r • x) = ↑r * gaugeSqrtSumSq_add_fst x

Positive homogeneity of gaugeSqrtSumSq_add_fst.

theorem isClosed_epigraph_gaugeSqrtSumSq_add_fst : IsClosed (epigraph Set.univ gaugeSqrtSumSq_add_fst)

The epigraph of gaugeSqrtSumSq_add_fst is closed.

theorem gaugeSqrtSumSq_add_fst_isGauge_isClosed : IsGauge gaugeSqrtSumSq_add_fst ∧ IsClosed (epigraph Set.univ gaugeSqrtSumSq_add_fst)

Text 15.0.8 (closed gauge): the function gaugeSqrtSumSq_add_fst is a gauge and its epigraph is closed.

noncomputable def polarGaugeSqrtSumSq_add_fst (xStar : Fin 2 → ℝ) : EReal

Text 15.0.8 (polar formula): explicit piecewise formula for the polar gauge of gaugeSqrtSumSq_add_fst.

Equations

• polarGaugeSqrtSumSq_add_fst xStar = if 0 < xStar 0 then ↑(1 / 2 * (xStar 1 ^ 2 / xStar 0 + xStar 0)) else if xStar 0 = 0 ∧ xStar 1 = 0 then 0 else ⊤

theorem sqrt_sq_add_sub_le (t b : ℝ) (ht : 0 < t) : √(t ^ 2 + b ^ 2) - t ≤ b ^ 2 / (2 * t)

Bound sqrt(t^2 + b^2) - t by b^2 / (2t) for t > 0.

theorem dotProduct_le_mul_sqrt_dotProduct_self_fin2 (x y : Fin 2 → ℝ) : x ⬝ᵥ y ≤ √(x 0 ^ 2 + x 1 ^ 2) * √(y 0 ^ 2 + y 1 ^ 2)

Cauchy–Schwarz inequality for Fin 2 → ℝ in dot-product form.

theorem polarGauge_gaugeSqrtSumSq_add_fst_eq_top_of_fst_lt_zero (xStar : Fin 2 → ℝ) (hx : xStar 0 < 0) : polarGauge gaugeSqrtSumSq_add_fst xStar = ⊤

If xStar 0 < 0, the polar gauge of gaugeSqrtSumSq_add_fst is ⊤.

theorem polarGauge_gaugeSqrtSumSq_add_fst_eq_top_of_fst_eq_zero_snd_ne_zero (xStar : Fin 2 → ℝ) (hx0 : xStar 0 = 0) (hx1 : xStar 1 ≠ 0) : polarGauge gaugeSqrtSumSq_add_fst xStar = ⊤

If xStar 0 = 0 and xStar 1 ≠ 0, the polar gauge is ⊤.

theorem polarGauge_gaugeSqrtSumSq_add_fst_mu0_feasible_of_fst_pos (xStar : Fin 2 → ℝ) (hpos : 0 < xStar 0) : have μ0 := 1 / 2 * (xStar 1 ^ 2 / xStar 0 + xStar 0); 0 ≤ ↑μ0 ∧ ∀ (x : Fin 2 → ℝ), ↑(x ⬝ᵥ xStar) ≤ ↑μ0 * gaugeSqrtSumSq_add_fst x

Feasible multiplier for the polar gauge when xStar 0 > 0.

theorem polarGauge_gaugeSqrtSumSq_add_fst_witness_of_fst_pos (xStar : Fin 2 → ℝ) (hpos : 0 < xStar 0) : have t := xStar 1 / xStar 0; have x := ![(1 - t ^ 2) / 2, t]; gaugeSqrtSumSq_add_fst x = 1 ∧ x ⬝ᵥ xStar = 1 / 2 * (xStar 1 ^ 2 / xStar 0 + xStar 0)

A point that attains the polar inequality when xStar 0 > 0.

theorem polarGauge_gaugeSqrtSumSq_add_fst_eq_mu0_of_fst_pos (xStar : Fin 2 → ℝ) (hpos : 0 < xStar 0) : polarGauge gaugeSqrtSumSq_add_fst xStar = ↑(1 / 2 * (xStar 1 ^ 2 / xStar 0 + xStar 0))

Compute the polar gauge value for xStar 0 > 0.

theorem polarGauge_gaugeSqrtSumSq_add_fst : polarGauge gaugeSqrtSumSq_add_fst = polarGaugeSqrtSumSq_add_fst

Text 15.0.8 (polar gauge): the polar gauge of gaugeSqrtSumSq_add_fst agrees with the explicit formula polarGaugeSqrtSumSq_add_fst.

theorem gaugeSqrtSumSq_add_fst_eval_vec10 : gaugeSqrtSumSq_add_fst ![1, 0] = 2 ∧ gaugeSqrtSumSq_add_fst (-![1, 0]) = 0

Evaluate gaugeSqrtSumSq_add_fst on ![1,0] and its negation.

theorem gaugeSqrtSumSq_add_fst_not_even_via_vec10 : ¬∀ (x : Fin 2 → ℝ), gaugeSqrtSumSq_add_fst (-x) = gaugeSqrtSumSq_add_fst x

The witness ![1,0] shows gaugeSqrtSumSq_add_fst is not even.

theorem gaugeSqrtSumSq_add_fst_not_even : ¬∀ (x : Fin 2 → ℝ), gaugeSqrtSumSq_add_fst (-x) = gaugeSqrtSumSq_add_fst x

Text 15.0.8 (not a norm): gaugeSqrtSumSq_add_fst is not even.

theorem polarGaugeSqrtSumSq_add_fst_eval_vec10 : polarGaugeSqrtSumSq_add_fst ![1, 0] = ↑(1 / 2) ∧ polarGaugeSqrtSumSq_add_fst (-![1, 0]) = ⊤

Evaluate polarGaugeSqrtSumSq_add_fst on ![1,0] and its negation.

theorem polarGaugeSqrtSumSq_add_fst_not_even_via_vec10 : ¬∀ (xStar : Fin 2 → ℝ), polarGaugeSqrtSumSq_add_fst (-xStar) = polarGaugeSqrtSumSq_add_fst xStar

The witness ![1,0] shows polarGaugeSqrtSumSq_add_fst is not even.

theorem polarGaugeSqrtSumSq_add_fst_not_even : ¬∀ (xStar : Fin 2 → ℝ), polarGaugeSqrtSumSq_add_fst (-xStar) = polarGaugeSqrtSumSq_add_fst xStar

Text 15.0.8 (not a norm): the polar gauge polarGaugeSqrtSumSq_add_fst is not even.

theorem inner_le_mul_polarGauge_real_eps {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x xStar : Fin n → ℝ) (hx : k x ≠ ⊤) (hxStar : polarGauge k xStar ≠ ⊤) (ε : ℝ) : ε > 0 → x ⬝ᵥ xStar ≤ ((polarGauge k xStar).toReal + ε) * (k x).toReal

Approximate the polar gauge inequality in ℝ with an ε-margin.

theorem inner_le_mul_polarGauge_real {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x xStar : Fin n → ℝ) (hx : k x ≠ ⊤) (hxStar : polarGauge k xStar ≠ ⊤) : x ⬝ᵥ xStar ≤ (k x).toReal * (polarGauge k xStar).toReal

Letting ε→0 in the real inequality gives the sharp product bound.

theorem inner_le_mul_polarGauge_via_toReal {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x xStar : Fin n → ℝ) (hx : k x ≠ ⊤) (hxStar : polarGauge k xStar ≠ ⊤) : ↑(x ⬝ᵥ xStar) ≤ k x * polarGauge k xStar

Cast the real inequality back to EReal.

theorem inner_le_mul_polarGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x xStar : Fin n → ℝ) (hx : k x ≠ ⊤) (hxStar : polarGauge k xStar ≠ ⊤) : ↑(x ⬝ᵥ xStar) ≤ k x * polarGauge k xStar

Text 15.0.9: Let k be a gauge and let kᵒ be its polar gauge. Then for every x in the effective domain of k and every x⋆ in the effective domain of kᵒ, ⟪x, x⋆⟫ ≤ k x * kᵒ x⋆.

In this development, we represent kᵒ by polarGauge k, the pairing ⟪x, x⋆⟫ by x ⬝ᵥ x⋆, and we model domain assumptions as k x ≠ ⊤ and polarGauge k x⋆ ≠ ⊤.

If k is a norm (i.e. k (-x) = k x and k is finite and positive away from 0), then |⟪x, x⋆⟫| ≤ k x * kᵒ x⋆ for all x, x⋆.

theorem abs_inner_le_mul_polarGauge_of_norm_like_casework {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_even : ∀ (x : Fin n → ℝ), k (-x) = k x) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) (x xStar : Fin n → ℝ) : ↑|x ⬝ᵥ xStar| ≤ k x * polarGauge k xStar

Absolute-value form of the polar gauge inequality under norm-like hypotheses.

theorem abs_inner_le_mul_polarGauge_of_norm_like {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_even : ∀ (x : Fin n → ℝ), k (-x) = k x) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) (x xStar : Fin n → ℝ) : ↑|x ⬝ᵥ xStar| ≤ k x * polarGauge k xStar

def innerMulFeasible {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (x : Fin n → ℝ) : Set EReal

Feasible multipliers for the inf-definition in Text 15.0.10.

Equations

• innerMulFeasible j x = {μ : EReal | 0 ≤ μ ∧ ∀ (y : ↑J), ↑(x ⬝ᵥ ↑y) ≤ μ * j y}

noncomputable def innerMulGauge {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (x : Fin n → ℝ) : EReal

Candidate gauge defined by infimum of feasible multipliers.

Equations

• innerMulGauge j x = sInf (innerMulFeasible j x)

theorem innerMulGauge_nonneg {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (x : Fin n → ℝ) : 0 ≤ innerMulGauge j x

The infimum definition yields a nonnegative value.

theorem innerMulGauge_zero {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) : innerMulGauge j 0 = 0

The infimum definition yields zero at the origin.

theorem le_mul_of_forall_pos_add_mul {a μ r : ℝ} (hr : 0 ≤ r) (h : ∀ ε > 0, a ≤ (μ + ε) * r) : a ≤ μ * r

If r ≥ 0 and a ≤ (μ + ε) * r for all ε > 0, then a ≤ μ * r.

theorem innerMulGauge_le_h_on_H {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 ≠ ⊤) (hineq : ∀ (x : ↑H) (y : ↑J), ↑(↑x ⬝ᵥ ↑y) ≤ h x * j y) (x : ↑H) : innerMulGauge j ↑x ≤ h x ∧ innerMulGauge j ↑x ≠ ⊤

If h is nonnegative and provides a feasible multiplier on H, then innerMulGauge ≤ h on H and hence innerMulGauge is finite on H.

theorem inner_le_innerMulGauge_mul_j_of_ne_top {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (j_nonneg : ∀ (y : ↑J), 0 ≤ j y) (j_ne_top : ∀ (y : ↑J), j y ≠ ⊤) (x : Fin n → ℝ) : innerMulGauge j x ≠ ⊤ → ∀ (y : ↑J), ↑(x ⬝ᵥ ↑y) ≤ innerMulGauge j x * j y

On the effective domain, innerMulGauge satisfies the defining inequality.

theorem innerMulGauge_ne_bot {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (x : Fin n → ℝ) : innerMulGauge j x ≠ ⊥

The inner-multiplier gauge never attains ⊥.

theorem innerMulFeasible_smul {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) {x : Fin n → ℝ} {μ : EReal} (hμ : μ ∈ innerMulFeasible j x) {t : ℝ} (ht : 0 ≤ t) : ↑t * μ ∈ innerMulFeasible j (t • x)

Scaling a feasible multiplier scales feasibility for the scaled vector.

theorem innerMulGauge_add_le {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (x z : Fin n → ℝ) : innerMulGauge j (x + z) ≤ innerMulGauge j x + innerMulGauge j z

The inner-multiplier gauge is subadditive.

theorem innerMulGauge_posHom {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) : PositivelyHomogeneous (innerMulGauge j)

The inner-multiplier gauge is positively homogeneous.

theorem innerMulGauge_isGauge {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) : IsGauge (innerMulGauge j)

The inner-multiplier gauge is a gauge.

theorem epigraph_innerMulGauge_eq_inter_iInter_halfspaces {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (j_nonneg : ∀ (y : ↑J), 0 ≤ j y) (j_ne_top : ∀ (y : ↑J), j y ≠ ⊤) : epigraph Set.univ (innerMulGauge j) = {p : (Fin n → ℝ) × ℝ | 0 ≤ p.2} ∩ ⋂ (y : ↑J), {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ ↑y ≤ p.2 * (j y).toReal}

Epigraph as an intersection of halfspaces for innerMulGauge.

theorem isClosed_epigraph_innerMulGauge {n : ℕ} {J : Set (Fin n → ℝ)} (j : ↑J → EReal) (j_nonneg : ∀ (y : ↑J), 0 ≤ j y) (j_ne_top : ∀ (y : ↑J), j y ≠ ⊤) : IsClosed (epigraph Set.univ (innerMulGauge j))

The epigraph of innerMulGauge is closed.