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

• Eq (egauge 𝕜 s x) (iInf fun (c : 𝕜) => iInf fun (x : Membership.mem (HSMul.hSMul c s) x) => ENorm.enorm c)

theorem egauge_anti (𝕜 : Type u_1) [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s t : Set E} (h : HasSubset.Subset s t) (x : E) : LE.le (egauge 𝕜 t x) (egauge 𝕜 s x)

theorem egauge_empty (𝕜 : Type u_1) [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (x : E) : Eq (egauge 𝕜 EmptyCollection.emptyCollection x) Top.top

theorem egauge_le_of_mem_smul {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {c : 𝕜} {s : Set E} {x : E} (h : Membership.mem (HSMul.hSMul c s) x) : LE.le (egauge 𝕜 s x) (ENorm.enorm c)

theorem le_egauge_iff {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal} : Iff (LE.le r (egauge 𝕜 s x)) (∀ (c : 𝕜), Membership.mem (HSMul.hSMul c s) x → LE.le r (ENorm.enorm c))

theorem egauge_eq_top {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} : Iff (Eq (egauge 𝕜 s x) Top.top) (∀ (c : 𝕜), Not (Membership.mem (HSMul.hSMul c s) x))

theorem egauge_lt_iff {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal} : Iff (LT.lt (egauge 𝕜 s x) r) (Exists fun (c : 𝕜) => And (Membership.mem (HSMul.hSMul c s) x) (LT.lt (ENorm.enorm c) r))

theorem egauge_union {𝕜 : Type u_1} [NNNorm 𝕜] {E : Type u_2} [SMul 𝕜 E] (s t : Set E) (x : E) : Eq (egauge 𝕜 (Union.union s t) x) (Min.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) : LE.le (Max.max (egauge 𝕜 s x) (egauge 𝕜 t x)) (egauge 𝕜 (Inter.inter s t) x)

theorem egauge_zero_left_eq_top (𝕜 : Type u_1) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [Zero E] [SMulZeroClass 𝕜 E] {x : E} : Iff (Eq (egauge 𝕜 0 x) Top.top) (Ne x 0)

theorem egauge_zero_left (𝕜 : Type u_1) [NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [Zero E] [SMulZeroClass 𝕜 E] {x : E} : Ne x 0 → Eq (egauge 𝕜 0 x) Top.top

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 : Membership.mem s (HSMul.hSMul c x)) (hc : Ne c 0) : LE.le (egauge 𝕜 s x) (ENNReal.ofNNReal (Inv.inv (NNNorm.nnnorm 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 : Membership.mem s (HSMul.hSMul c x)) : LE.le (egauge 𝕜 s x) (Inv.inv (ENorm.enorm c))

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

See also egauge_le_of_smul_mem_of_ne.

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 : LT.lt (egauge 𝕜 s x) 1) : Membership.mem s x

theorem egauge_eq_zero_iff {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} : Iff (Eq (egauge 𝕜 s x) 0) (Filter.Frequently (fun (c : 𝕜) => Membership.mem (HSMul.hSMul c s) x) (nhds 0))

theorem egauge_univ {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {x : E} [(nhdsWithin 0 (HasCompl.compl (Singleton.singleton 0))).NeBot] : Eq (egauge 𝕜 Set.univ x) 0

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

theorem egauge_zero_zero (𝕜 : Type u_1) [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] : Eq (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 : Membership.mem s x) : LE.le (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) : LE.le (HDiv.hDiv (egauge 𝕜 s x) (ENorm.enorm c)) (egauge 𝕜 (HSMul.hSMul c s) x)

theorem egauge_smul_left {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} (hc : Ne c 0) (s : Set E) (x : E) : Eq (egauge 𝕜 (HSMul.hSMul c s) x) (HDiv.hDiv (egauge 𝕜 s x) (ENorm.enorm c))

theorem le_egauge_smul_right {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] (c : 𝕜) (s : Set E) (x : E) : LE.le (HMul.hMul (ENorm.enorm c) (egauge 𝕜 s x)) (egauge 𝕜 s (HSMul.hSMul c x))

theorem egauge_smul_right {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {c : 𝕜} {s : Set E} (h : Eq c 0 → s.Nonempty) (x : E) : Eq (egauge 𝕜 s (HSMul.hSMul c x)) (HMul.hMul (ENorm.enorm c) (egauge 𝕜 s x))

theorem egauge_add_add_le {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) : LE.le (egauge 𝕜 (HAdd.hAdd U V) (HAdd.hAdd a b)) (Max.max (egauge 𝕜 U a) (egauge 𝕜 V b))

theorem div_le_egauge_closedBall (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : NNReal) (x : E) : LE.le (HDiv.hDiv (ENorm.enorm x) (ENNReal.ofNNReal r)) (egauge 𝕜 (Metric.closedBall 0 r.toReal) x)

theorem le_egauge_closedBall_one (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : LE.le (ENorm.enorm 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) : LE.le (HDiv.hDiv (ENorm.enorm x) (ENNReal.ofNNReal r)) (egauge 𝕜 (Metric.ball 0 r.toReal) x)

theorem le_egauge_ball_one (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : LE.le (ENorm.enorm 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 : LT.lt 1 (Norm.norm c)) (h₀ : Or (Ne r 0) (Ne (Norm.norm x) 0)) : LE.le (egauge 𝕜 (Metric.ball 0 r.toReal) x) (HDiv.hDiv (HMul.hMul (ENorm.enorm c) (ENorm.enorm x)) (ENNReal.ofNNReal r))

theorem egauge_ball_one_le_of_one_lt_norm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : LT.lt 1 (Norm.norm c)) (x : E) : LE.le (egauge 𝕜 (Metric.ball 0 1) x) (HMul.hMul (ENorm.enorm c) (ENorm.enorm x))