The Minkowski functional, normed field version

In this file we define (egauge 𝕜 s ·) to be the Minkowski functional (gauge) of the set s in a topological vector space E over a normed field 𝕜, as a function E → ℝ≥0∞.

It is defined as the infimum of the norms of c : 𝕜 such that x ∈ c • s. In particular, for 𝕜 = ℝ≥0 this definition gives an ℝ≥0∞-valued version of gauge defined in Mathlib/Analysis/Convex/Gauge.lean.

This definition can be used to generalize the notion of Fréchet derivative to maps between topological vector spaces without norms.

Currently, we can't reuse results about egauge for gauge, because we lack a theory of normed semifields.

noncomputable def egauge (𝕜 : Type u_1) [ENorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (s : Set E) (x : E) : ENNReal

The Minkowski functional for vector spaces over normed fields. Given a set s in a vector space over a normed field 𝕜, egauge s is the functional which sends x : E to the infimum of ‖c‖ₑ over c such that x belongs to s scaled by c.

The definition only requires 𝕜 to have a ENorm instance and (· • ·) : 𝕜 → E → E to be defined. This way the definition applies, e.g., to 𝕜 = ℝ≥0. For 𝕜 = ℝ≥0, the function is equal (up to conversion to ℝ) to the usual Minkowski functional defined in gauge.

Equations

• egauge 𝕜 s x = ⨅ (c : 𝕜), ⨅ (_ : x ∈ c • s), ‖c‖ₑ

theorem Set.MapsTo.egauge_le (𝕜 : Type u_1) [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {E' : Type u_3} {F : Type u_4} [SMul 𝕜 E'] [FunLike F E E'] [MulActionHomClass F 𝕜 E E'] (f : F) {t : Set E'} (h : MapsTo (⇑f) s t) (x : E) : egauge 𝕜 t (f x) ≤ egauge 𝕜 s x

theorem egauge_anti (𝕜 : Type u_1) [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s t : Set E} (h : s ⊆ t) (x : E) : egauge 𝕜 t x ≤ egauge 𝕜 s x

@[simp]

theorem egauge_empty (𝕜 : Type u_1) [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (x : E) : egauge 𝕜 ∅ x = ⊤

theorem egauge_le_of_mem_smul {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {c : 𝕜} {s : Set E} {x : E} (h : x ∈ c • s) : egauge 𝕜 s x ≤ ‖c‖ₑ

theorem le_egauge_iff {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal} : r ≤ egauge 𝕜 s x ↔ ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ

theorem egauge_eq_top {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} : egauge 𝕜 s x = ⊤ ↔ ∀ (c : 𝕜), x ∉ c • s

theorem egauge_lt_iff {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal} : egauge 𝕜 s x < r ↔ ∃ (c : 𝕜), x ∈ c • s ∧ ‖c‖ₑ < r

theorem egauge_union {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (s t : Set E) (x : E) : egauge 𝕜 (s ∪ t) x = min (egauge 𝕜 s x) (egauge 𝕜 t x)

theorem le_egauge_inter {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (s t : Set E) (x : E) : max (egauge 𝕜 s x) (egauge 𝕜 t x) ≤ egauge 𝕜 (s ∩ t) x

theorem le_egauge_pi {𝕜 : Type u_1} [NNNorm 𝕜] {ι : Type u_3} {E : ι → Type u_4} [(i : ι) → SMul 𝕜 (E i)] {I : Set ι} {i : ι} (hi : i ∈ I) (s : (i : ι) → Set (E i)) (x : (i : ι) → E i) : egauge 𝕜 (s i) (x i) ≤ egauge 𝕜 (I.pi s) x

theorem le_egauge_prod {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {F : Type u_3} [SMul 𝕜 F] (s : Set E) (t : Set F) (a : E) (b : F) : max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b)

@[simp]

theorem egauge_zero_left_eq_top (𝕜 : Type u_1) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [Zero E] [SMulZeroClass 𝕜 E] {x : E} : egauge 𝕜 0 x = ⊤ ↔ x ≠ 0

@[simp]

theorem egauge_zero_left (𝕜 : Type u_1) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [Zero E] [SMulZeroClass 𝕜 E] {x : E} : x ≠ 0 → egauge 𝕜 0 x = ⊤

Alias of the reverse direction of egauge_zero_left_eq_top.

theorem egauge_le_of_smul_mem_of_ne {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} {s : Set E} {x : E} (h : c • x ∈ s) (hc : c ≠ 0) : egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹

If c • x ∈ s and c ≠ 0, then egauge 𝕜 s x is at most (‖c‖₊⁻¹ : ℝ≥0).

See also egauge_le_of_smul_mem.

theorem egauge_le_of_smul_mem {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} {s : Set E} {x : E} (h : c • x ∈ s) : egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

If c • x ∈ s, then egauge 𝕜 s x is at most ‖c‖ₑ⁻¹.

See also egauge_le_of_smul_mem_of_ne.

theorem mem_smul_of_egauge_lt {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} {s : Set E} {x : E} (hs : Balanced 𝕜 s) (hc : egauge 𝕜 s x < ‖c‖ₑ) : x ∈ c • s

theorem mem_of_egauge_lt_one {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (hs : Balanced 𝕜 s) (hx : egauge 𝕜 s x < 1) : x ∈ s

theorem egauge_eq_zero_iff {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} : egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in nhds 0, x ∈ c • s

@[simp]

theorem egauge_univ {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {x : E} [(nhdsWithin 0 {0}ᶜ).NeBot] : egauge 𝕜 Set.univ x = 0

@[simp]

theorem egauge_zero_right (𝕜 : Type u_1) [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : s.Nonempty) : egauge 𝕜 s 0 = 0

theorem egauge_zero_zero (𝕜 : Type u_1) [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] : egauge 𝕜 0 0 = 0

theorem egauge_le_one (𝕜 : Type u_1) [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (h : x ∈ s) : egauge 𝕜 s x ≤ 1

theorem le_egauge_smul_left {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] (c : 𝕜) (s : Set E) (x : E) : egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

theorem egauge_smul_left {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) : egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

theorem le_egauge_smul_right {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] (c : 𝕜) (s : Set E) (x : E) : ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)

theorem egauge_smul_right {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} {s : Set E} (h : c = 0 → s.Nonempty) (x : E) : egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x

theorem egauge_prod_mk {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] {U : Set E} {V : Set F} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a : E) (b : F) : egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b)

The extended gauge of a point (a, b) with respect to the product of balanced sets U and V is equal to the maximum of the extended gauges of a with respect to U and b with respect to V.

theorem egauge_add_add_le {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) : egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)

theorem egauge_pi' {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [NormedDivisionRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] {I : Set ι} (hI : I.Finite) {U : (i : ι) → Set (E i)} (hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : (i : ι) → E i) (hI₀ : I = Set.univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (nhdsWithin 0 {0}ᶜ).NeBot) : egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

The extended gauge of a point x in an indexed product with respect to a product of finitely many balanced sets U i, i ∈ I, (and the whole spaces for the other indices) is the supremum of the extended gauges of the components of x with respect to the corresponding balanced set.

This version assumes the following technical condition:

• either I is the universal set;
• or one of x i, i ∈ I, is nonzero;
• or 𝕜 is nontrivially normed.

theorem egauge_univ_pi {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [NormedDivisionRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [Finite ι] {U : (i : ι) → Set (E i)} (hU : ∀ (i : ι), Balanced 𝕜 (U i)) (x : (i : ι) → E i) : egauge 𝕜 (Set.univ.pi U) x = ⨆ (i : ι), egauge 𝕜 (U i) (x i)

The extended gauge of a point x in an indexed product with finite index type with respect to a product of balanced sets U i, is the supremum of the extended gauges of the components of x with respect to the corresponding balanced set.

theorem egauge_pi {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [NormedDivisionRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(nhdsWithin 0 {0}ᶜ).NeBot] {I : Set ι} {U : (i : ι) → Set (E i)} (hI : I.Finite) (hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : (i : ι) → E i) : egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

The extended gauge of a point x in an indexed product with respect to a product of finitely many balanced sets U i, i ∈ I, (and the whole spaces for the other indices) is the supremum of the extended gauges of the components of x with respect to the corresponding balanced set.

This version assumes that 𝕜 is a nontrivially normed division ring. See also egauge_univ_pi for when s = univ, and egauge_pi' for a version with more choices of the technical assumptions.

theorem div_le_egauge_closedBall (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : NNReal) (x : E) : ‖x‖ₑ / ↑r ≤ egauge 𝕜 (Metric.closedBall 0 ↑r) x

theorem le_egauge_closedBall_one (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (Metric.closedBall 0 1) x

theorem div_le_egauge_ball (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : NNReal) (x : E) : ‖x‖ₑ / ↑r ≤ egauge 𝕜 (Metric.ball 0 ↑r) x

theorem le_egauge_ball_one (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (Metric.ball 0 1) x

theorem egauge_ball_le_of_one_lt_norm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} {x : E} {r : NNReal} (hc : 1 < ‖c‖) (h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0) : egauge 𝕜 (Metric.ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

theorem egauge_ball_one_le_of_one_lt_norm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) (x : E) : egauge 𝕜 (Metric.ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ