theorem piEuclideanNorm_smul {n : ℕ} (r : ℝ) (x : Fin n → ℝ) : √(r • x ⬝ᵥ r • x) = |r| * √(x ⬝ᵥ x)

The Euclidean norm scales linearly with scalar multiplication.

theorem supNorm_le_piEuclideanNorm_and_piEuclideanNorm_le_sqrt_n_mul_supNorm {n : ℕ} (x : Fin n → ℝ) : ‖x‖ ≤ √(x ⬝ᵥ x) ∧ √(x ⬝ᵥ x) ≤ √↑n * ‖x‖

Comparison of the sup norm with the Euclidean norm on Fin n → ℝ.

theorem exists_pos_smul_piEuclideanUnitBall_subset_of_zero_mem_interior {n : ℕ} {C : Set (Fin n → ℝ)} (hC0 : 0 ∈ interior C) : ∃ (α : ℝ), 0 < α ∧ (fun (x : Fin n → ℝ) => α • x) '' piEuclideanUnitBall n ⊆ C

A neighborhood of 0 contains a scaled Euclidean unit ball.

theorem exists_pos_smul_piEuclideanUnitBall_superset_of_isBounded {n : ℕ} {C : Set (Fin n → ℝ)} (hC_bdd : Bornology.IsBounded C) : ∃ (β : ℝ), 0 < β ∧ C ⊆ (fun (x : Fin n → ℝ) => β • x) '' piEuclideanUnitBall n

A bounded set is contained in a scaled Euclidean unit ball.

theorem rho_bounds_of_ball_eq_and_unitBall_sandwich {n : ℕ} {C : Set (Fin n → ℝ)} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} {α β : ℝ} (hαpos : 0 < α) (hβpos : 0 < β) (hCα : (fun (x : Fin n → ℝ) => α • x) '' piEuclideanUnitBall n ⊆ C) (hCβ : C ⊆ (fun (x : Fin n → ℝ) => β • x) '' piEuclideanUnitBall n) (hρdiag : ∀ (x : Fin n → ℝ), ρ x x = 0) (hρpos : ∀ (x y : Fin n → ℝ), x ≠ y → 0 < ρ x y) (hball : ∀ (x : Fin n → ℝ) (ε : ℝ), 0 < ε → {y : Fin n → ℝ | ρ x y ≤ ε} = (fun (c : Fin n → ℝ) => x + ε • c) '' C) (x y : Fin n → ℝ) : β⁻¹ * piEuclideanDist x y ≤ ρ x y ∧ ρ x y ≤ α⁻¹ * piEuclideanDist x y

Bounds on ρ from the unit-ball sandwich and the ball formula.

theorem isOpen_isClosed_cauchy_equiv_of_two_sided_bounds {α : Type u_1} {d₁ d₂ : α → α → ℝ} {c₁ c₂ : ℝ} (hc₁ : 0 < c₁) (hc₂ : 0 < c₂) (hbound : ∀ (x y : α), c₁ * d₁ x y ≤ d₂ x y ∧ d₂ x y ≤ c₂ * d₁ x y) : (∀ (s : Set α), IsOpenOfDistFun d₂ s ↔ IsOpenOfDistFun d₁ s) ∧ (∀ (s : Set α), IsClosedOfDistFun d₂ s ↔ IsClosedOfDistFun d₁ s) ∧ ∀ (u : ℕ → α), CauchySeqOfDistFun d₂ u ↔ CauchySeqOfDistFun d₁ u

Two-sided bounds between distance functions give equivalent open/closed/Cauchy notions.

theorem exists_constants_unitBall_sandwich_and_topologicalEquiv_of_minkowskiMetricFun_ball_eq {n : ℕ} {C : Set (Fin n → ℝ)} {ρ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ} (hρ : IsMinkowskiMetricFun ρ) (hC_bdd : Bornology.IsBounded C) (hC0 : 0 ∈ interior C) (hball : ∀ (x : Fin n → ℝ) (ε : ℝ), 0 < ε → {y : Fin n → ℝ | ρ x y ≤ ε} = (fun (c : Fin n → ℝ) => x + ε • c) '' C) : ∃ (α : ℝ) (β : ℝ), 0 < α ∧ 0 < β ∧ (fun (x : Fin n → ℝ) => α • x) '' piEuclideanUnitBall n ⊆ C ∧ C ⊆ (fun (x : Fin n → ℝ) => β • x) '' piEuclideanUnitBall n ∧ (∀ (x y : Fin n → ℝ), β⁻¹ * piEuclideanDist x y ≤ ρ x y ∧ ρ x y ≤ α⁻¹ * piEuclideanDist x y) ∧ (∀ (s : Set (Fin n → ℝ)), IsOpenOfDistFun ρ s ↔ IsOpenOfDistFun piEuclideanDist s) ∧ (∀ (s : Set (Fin n → ℝ)), IsClosedOfDistFun ρ s ↔ IsClosedOfDistFun piEuclideanDist s) ∧ ∀ (u : ℕ → Fin n → ℝ), CauchySeqOfDistFun ρ u ↔ CauchySeqOfDistFun piEuclideanDist u

Text 15.0.19: Since C is bounded and 0 ∈ int C, there exist α, β > 0 such that α B ⊆ C ⊆ β B, where B is the Euclidean unit ball.

Writing d(x,y) = ‖x - y‖₂, the associated Minkowski metric ρ satisfies the two-sided comparison α^{-1} d(x,y) ≥ ρ(x,y) ≥ β^{-1} d(x,y) for all x,y.

Consequently, Minkowski metrics on ℝⁿ are topologically equivalent to the Euclidean metric: they induce the same open/closed sets and the same Cauchy sequences.

def IsGaugeLike {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

Text 15.0.20: An extended-real-valued convex function f : ℝⁿ → (-∞, +∞] is gauge-like if f(0) = inf f and all its sublevel sets {x | f x ≤ α} for f(0) < α < +∞ are proportional, i.e. each is a positive scalar multiple of any other such sublevel set.

Equations

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

theorem sublevel_sets_homothetic_of_IsGaugeLike {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGaugeLike f) {α β : EReal} (hα0 : f 0 < α) (hαtop : α < ⊤) (hβ0 : f 0 < β) (hβtop : β < ⊤) : ∃ (t : ℝ), 0 < t ∧ {x : Fin n → ℝ | f x ≤ α} = t • {x : Fin n → ℝ | f x ≤ β}

Sublevel sets of a gauge-like function are homothetic.

theorem sublevel_eq_smul_sublevel_one_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) {t : ℝ} (ht : 0 < t) : {x : Fin n → ℝ | k x ≤ ↑t} = t • {x : Fin n → ℝ | k x ≤ 1}

Sublevel sets of a gauge scale by positive factors.

theorem exists_unit_level_of_pos_finite {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : (∃ (y : Fin n → ℝ), 0 < k y ∧ k y < ⊤) → ∃ (y1 : Fin n → ℝ), k y1 = 1

A gauge taking a positive finite value attains 1 on some point.

theorem supportFunctionEReal_isGauge_of_convex_zeroMem {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : IsGauge (supportFunctionEReal C)

The support function of a nonempty convex set containing 0 is a gauge.

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

A gauge is closed if its epigraph over univ is closed.

Equations

• IsClosedGauge k = (IsGauge k ∧ IsClosed (epigraph Set.univ k))

theorem supportFunctionEReal_isClosedGauge_of_convex_zeroMem {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : IsClosedGauge (supportFunctionEReal C)

The support function of a nonempty convex set containing 0 is a closed gauge.

theorem supportFunctionEReal_nonneg_of_zero_mem {n : ℕ} {C : Set (Fin n → ℝ)} (hC0 : 0 ∈ C) (xStar : Fin n → ℝ) : 0 ≤ supportFunctionEReal C xStar

The support function of a set containing 0 is nonnegative.

def IsGaugeLikeClosedProperConvex {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

A function is gauge-like closed proper convex if it is gauge-like and is a closed proper convex EReal-valued function on ℝⁿ (modeled as Fin n → ℝ).

Equations

• IsGaugeLikeClosedProperConvex f = (IsGaugeLike f ∧ ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f)

theorem exists_real_beta_between_f0_and_top {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGaugeLikeClosedProperConvex f) : ∃ (β : ℝ), f 0 < ↑β ∧ ↑β < ⊤

A gauge-like closed proper convex function has a finite level strictly above f 0.

theorem sublevel_closed_convex_of_closedConvex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ClosedConvexFunction f) (α : ℝ) : IsClosed {x : Fin n → ℝ | f x ≤ ↑α} ∧ Convex ℝ {x : Fin n → ℝ | f x ≤ ↑α}

Sublevel sets of a closed convex function are closed and convex.

theorem subset_bipolar_of_any {n : ℕ} {C : Set (Fin n → ℝ)} : C ⊆ {x : Fin n → ℝ | ∀ xStar ∈ {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}, x ⬝ᵥ xStar ≤ 1}

The bipolar set always contains the original set.

theorem linearMap_eq_dotProduct_piSingle {n : ℕ} (f : (Fin n → ℝ) →ₗ[ℝ] ℝ) (x : Fin n → ℝ) : f x = x ⬝ᵥ fun (i : Fin n) => f (Pi.single i 1)

Any linear functional on Fin n → ℝ is a dot product with its coordinates on the standard basis.

theorem bipolar_eq_of_closed_convex_zeroMem {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : C = {x : Fin n → ℝ | ∀ xStar ∈ {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}, x ⬝ᵥ xStar ≤ 1}

A closed convex set containing 0 coincides with its bipolar.

theorem closedGauge_from_baseSublevel_supportFunctionEReal_polar_and_unitSublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} {β : ℝ} (hf : IsGaugeLikeClosedProperConvex f) (hβ0 : f 0 < ↑β) : have C := {x : Fin n → ℝ | f x ≤ ↑β}; have Cpolar := {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}; have k := supportFunctionEReal Cpolar; IsClosedGauge k ∧ {x : Fin n → ℝ | k x ≤ 1} = C

Build a closed gauge from a base sublevel of a gauge-like closed proper convex function.

theorem exists_closedGauge_unitSublevel_eq_baseSublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGaugeLikeClosedProperConvex f) : ∃ (β : ℝ), f 0 < ↑β ∧ ↑β < ⊤ ∧ ∃ (k : (Fin n → ℝ) → EReal), IsClosedGauge k ∧ {x : Fin n → ℝ | k x ≤ 1} = {x : Fin n → ℝ | f x ≤ ↑β}

Pick a base sublevel and a closed gauge whose unit sublevel matches it.

theorem supportFunction_unitSublevel_le_polarGauge_of_isGauge {n : ℕ} {k : (Fin n → ℝ) → EReal} (xStar : Fin n → ℝ) : supportFunctionEReal {x : Fin n → ℝ | k x ≤ 1} xStar ≤ polarGauge k xStar

The support function of the unit sublevel of a gauge is bounded by its polar gauge.

theorem dotProduct_le_zero_of_k_eq_zero_of_supportFunction_ne_top {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) {xStar : Fin n → ℝ} (hμtop : supportFunctionEReal {x : Fin n → ℝ | k x ≤ 1} xStar ≠ ⊤) {x : Fin n → ℝ} (hx0 : k x = 0) : ↑(x ⬝ᵥ xStar) ≤ 0

If the unit-sublevel support function is finite, then any x with k x = 0 pairs nonpositively with the dual vector.