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

Text 15.0.1: A function k : ℝⁿ → (-∞, +∞] is a gauge if it is convex, nonnegative, positively homogeneous of degree 1 (i.e. k (λ x) = λ k x for all λ ≥ 0), and satisfies k 0 = 0.

Equivalently, its epigraph epi k = {(x, μ) | k x ≤ μ} is a convex cone in ℝⁿ⁺¹ containing (0, 0) and containing no vector (x, μ) with μ < 0.

In this formalization, we use Fin n → ℝ for ℝⁿ, EReal for (-∞, +∞], and the epigraph construction epigraph (S := Set.univ) k from Books.ConvexAnalysis_Rockafellar_1970.Chapters.Chap01.section04_part1.

Equations

• IsGauge k = (ConvexFunctionOn Set.univ k ∧ (∀ (x : Fin n → ℝ), 0 ≤ k x) ∧ (∀ (x : Fin n → ℝ) (r : ℝ), 0 ≤ r → k (r • x) = ↑r * k x) ∧ k 0 = 0)

theorem IsGauge.ne_bot {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x : Fin n → ℝ) : k x ≠ ⊥

A gauge never attains ⊥ because it is nonnegative.

theorem IsGauge.add_le {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (x y : Fin n → ℝ) : k (x + y) ≤ k x + k y

A gauge is subadditive.

theorem IsGauge.sublevel_one_nonempty {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : {x : Fin n → ℝ | k x ≤ 1}.Nonempty

The unit sublevel set of a gauge is nonempty (it contains 0).

theorem IsGauge.convex_sublevel_one {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : Convex ℝ {x : Fin n → ℝ | k x ≤ 1}

The unit sublevel set of a gauge is convex.

theorem IsGauge.gaugeFunction_sublevel_one_eq_toReal {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (x : Fin n → ℝ) : gaugeFunction {x : Fin n → ℝ | k x ≤ 1} x = (k x).toReal

The gauge of the unit sublevel set of a finite-valued gauge agrees with toReal.

theorem IsGauge.gaugeFunction_sublevel_one_eq {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) : (fun (x : Fin n → ℝ) => ↑(gaugeFunction {x : Fin n → ℝ | k x ≤ 1} x)) = k

The gauge of the unit sublevel set of a finite-valued gauge agrees with k.

theorem IsGauge.exists_set_eq_gaugeFunction {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) : ∃ (C : Set (Fin n → ℝ)), C.Nonempty ∧ Convex ℝ C ∧ k = fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)

Text 15.0.2: Every gauge k can be represented as k = γ(· | C) for some nonempty convex set C. In this development, γ(· | C) is represented by fun x => (gaugeFunction C x : EReal).

theorem gaugeFunction_eq_of_convex_nonempty_eq_sublevel {n : ℕ} {k : (Fin n → ℝ) → EReal} {C : Set (Fin n → ℝ)} (hC : C = {x : Fin n → ℝ | k x ≤ 1}) (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) : (fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) = k

Text 15.0.3: For a nonempty convex set C = {x ∈ ℝⁿ | k x ≤ 1}, one has γ(· | C) = k.

In this development, γ(· | C) is represented by fun x => (gaugeFunction C x : EReal).

theorem set_eq_gaugeFunction_sublevel_one {n : ℕ} {D : Set (Fin n → ℝ)} (hDclosed : IsClosed D) (hDconv : Convex ℝ D) (hD0 : 0 ∈ D) (hDabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' D) : D = {x : Fin n → ℝ | ↑(gaugeFunction D x) ≤ 1}

A closed convex absorbing set is the unit sublevel set of its gauge function.

theorem eq_sublevel_one_of_gaugeFunction_eq {n : ℕ} {k : (Fin n → ℝ) → EReal} {D : Set (Fin n → ℝ)} (hDclosed : IsClosed D) (hDconv : Convex ℝ D) (hD0 : 0 ∈ D) (hDabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' D) (hg : (fun (x : Fin n → ℝ) => ↑(gaugeFunction D x)) = k) : D = {x : Fin n → ℝ | k x ≤ 1}

If a set's gauge function agrees with k, then the set is the k ≤ 1 sublevel.

theorem sublevel_one_unique_closed_convex_of_isClosed_epigraph {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) (hk_closed : IsClosed (epigraph Set.univ k)) : have C := {x : Fin n → ℝ | k x ≤ 1}; IsClosed C ∧ Convex ℝ C ∧ 0 ∈ C ∧ (fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) = k ∧ ∀ (D : Set (Fin n → ℝ)), IsClosed D → Convex ℝ D → 0 ∈ D → (fun (x : Fin n → ℝ) => ↑(gaugeFunction D x)) = k → D = C

Text 15.0.4: If k is closed (and finite, positive away from 0), then the set C = {x ∈ ℝⁿ | k x ≤ 1} is the unique closed convex set containing 0 such that γ(· | C) = k.

In this development, we express "closedness of k" as closedness of the book epigraph epigraph univ k, and γ(· | C) is represented by fun x => (gaugeFunction C x : EReal).

noncomputable def polarGauge {n : ℕ} (k : (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : EReal

Text 15.0.5: Let k be a gauge on ℝⁿ. Its polar kᵒ : ℝⁿ → [0, +∞] is defined by kᵒ x⋆ = inf { μ⋆ ≥ 0 | ⟪x, x⋆⟫ ≤ μ⋆ * k x for all x }.

In this development, ℝⁿ is Fin n → ℝ and we represent the inf as sInf in EReal.

Equations

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

theorem polarGauge_nonneg {n : ℕ} {k : (Fin n → ℝ) → EReal} (xStar : Fin n → ℝ) : 0 ≤ polarGauge k xStar

The polar gauge is nonnegative.

theorem polarGauge_zero {n : ℕ} (k : (Fin n → ℝ) → EReal) : polarGauge k 0 = 0

The polar gauge of any function vanishes at 0.

theorem polarGauge_ne_bot {n : ℕ} {k : (Fin n → ℝ) → EReal} (xStar : Fin n → ℝ) : polarGauge k xStar ≠ ⊥

The polar gauge never attains ⊥.

theorem polarGauge_feasible_smul {n : ℕ} {k : (Fin n → ℝ) → EReal} {xStar : Fin n → ℝ} {μ : EReal} (hμ : 0 ≤ μ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ μ * k x) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ ↑t * μ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ t • xStar) ≤ ↑t * μ * k x

Scaling a feasible multiplier remains feasible for the scaled dual vector.

theorem polarGauge_feasible_add {n : ℕ} {k : (Fin n → ℝ) → EReal} {xStar₁ xStar₂ : Fin n → ℝ} {μ₁ μ₂ : EReal} (hμ₁ : 0 ≤ μ₁ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar₁) ≤ μ₁ * k x) (hμ₂ : 0 ≤ μ₂ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar₂) ≤ μ₂ * k x) : 0 ≤ μ₁ + μ₂ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ (xStar₁ + xStar₂)) ≤ (μ₁ + μ₂) * k x

Adding feasible multipliers is feasible for the sum of dual vectors.

theorem polarGauge_le_of_feasible_add {n : ℕ} {k : (Fin n → ℝ) → EReal} {xStar₁ xStar₂ : Fin n → ℝ} {μ₁ μ₂ : EReal} (hμ₁ : 0 ≤ μ₁ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar₁) ≤ μ₁ * k x) (hμ₂ : 0 ≤ μ₂ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar₂) ≤ μ₂ * k x) : polarGauge k (xStar₁ + xStar₂) ≤ μ₁ + μ₂

A feasible sum bounds the polar gauge of the summed dual vector.

theorem polarGauge_le_of_feasible_smul {n : ℕ} {k : (Fin n → ℝ) → EReal} {xStar : Fin n → ℝ} {μ : EReal} (hμ : 0 ≤ μ ∧ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ μ * k x) {t : ℝ} (ht : 0 ≤ t) : polarGauge k (t • xStar) ≤ ↑t * μ

A feasible scaling bounds the polar gauge of the scaled dual vector.

theorem polarGauge_posHom {n : ℕ} {k : (Fin n → ℝ) → EReal} : PositivelyHomogeneous (polarGauge k)

The polar gauge is positively homogeneous.

theorem polarGauge_add_le {n : ℕ} {k : (Fin n → ℝ) → EReal} (xStar₁ xStar₂ : Fin n → ℝ) : polarGauge k (xStar₁ + xStar₂) ≤ polarGauge k xStar₁ + polarGauge k xStar₂

The polar gauge is subadditive.

theorem polarGauge_isGauge {n : ℕ} (k : (Fin n → ℝ) → EReal) : IsGauge (polarGauge k)

The polar gauge is a gauge.

theorem polarGauge_ratio_le_of_feasible {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) {xStar : Fin n → ℝ} {μ : EReal} (hμ0 : 0 ≤ μ) (hμ : ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ μ * k x) {x : Fin n → ℝ} (hx : x ≠ 0) : ↑(x ⬝ᵥ xStar / (k x).toReal) ≤ μ

A feasible μ for the polar gauge bounds each ratio ⟪x, x⋆⟫ / k x when x ≠ 0.

theorem polarGauge_mul_le_of_ratio_le {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) {xStar : Fin n → ℝ} {μ : EReal} (hμ_top : μ ≠ ⊤) (hμ_ne_bot : μ ≠ ⊥) {x : Fin n → ℝ} (hx : x ≠ 0) (hμ : ↑(x ⬝ᵥ xStar / (k x).toReal) ≤ μ) : ↑(x ⬝ᵥ xStar) ≤ μ * k x

A bound on the ratio yields the product bound when the coefficient is finite.

theorem polarGauge_eq_sSup_div {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hk_finite : ∀ (x : Fin n → ℝ), k x ≠ ⊤) (hk_pos : ∀ (x : Fin n → ℝ), x ≠ 0 → 0 < k x) (h_nonempty : ∃ (x : Fin n → ℝ), x ≠ 0) (xStar : Fin n → ℝ) : polarGauge k xStar = sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar / (k x).toReal)) '' {x : Fin n → ℝ | x ≠ 0})

Text 15.0.6: If a gauge k is finite everywhere and positive except at the origin, then kᵒ admits the equivalent formula kᵒ x⋆ = sup_{x ≠ 0} ⟪x, x⋆⟫ / k x.

In this development, kᵒ is polarGauge k, and we express sup as a sSup over the image of x ↦ ⟪x, x⋆⟫ / (k x) (using EReal.toReal to form a real quotient).