The Minkowski functional

This file defines the Minkowski functional, aka gauge.

The Minkowski functional of a set s is the function which associates each point to how much you need to scale s for x to be inside it. When s is symmetric, convex and absorbent, its gauge is a seminorm. Reciprocally, any seminorm arises as the gauge of some set, namely its unit ball. This induces the equivalence of seminorms and locally convex topological vector spaces.

Main declarations

For a real vector space,

• gauge: Aka Minkowski functional. gauge s x is the least (actually, an infimum) r such that x ∈ r • s.
• gaugeSeminorm: The Minkowski functional as a seminorm, when s is symmetric, convex and absorbent.

References

• [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

Minkowski functional, gauge

noncomputable def gauge {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : Set E) (x : E) : ℝ

The Minkowski functional. Given a set s in a real vector space, gauge s is the functional which sends x : E to the smallest r : ℝ such that x is in s scaled by r.

theorem gauge_def {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} : gauge s x = sInf {r : ℝ | r ∈ Set.Ioi 0 ∧ x ∈ r • s}

theorem gauge_def' {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} : gauge s x = sInf {r : ℝ | r ∈ Set.Ioi 0 ∧ r⁻¹ • x ∈ s}

An alternative definition of the gauge using scalar multiplication on the element rather than on the set.

theorem Absorbent.gauge_set_nonempty {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} (absorbs : Absorbent ℝ s) : {r : ℝ | 0 < r ∧ x ∈ r • s}.Nonempty

If the given subset is Absorbent then the set we take an infimum over in gauge is nonempty, which is useful for proving many properties about the gauge.

theorem gauge_mono {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s t : Set E} (hs : Absorbent ℝ s) (h : s ⊆ t) : gauge t ≤ gauge s

theorem exists_lt_of_gauge_lt {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} {a : ℝ} (absorbs : Absorbent ℝ s) (h : gauge s x < a) : ∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s

@[simp]

theorem gauge_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : gauge s 0 = 0

The gauge evaluated at 0 is always zero (mathematically this requires 0 to be in the set s but, the real infimum of the empty set in Lean being defined as 0, it holds unconditionally).

@[simp]

theorem gauge_zero' {E : Type u_2} [AddCommGroup E] [Module ℝ E] : gauge 0 = 0

@[simp]

theorem gauge_empty {E : Type u_2} [AddCommGroup E] [Module ℝ E] : gauge ∅ = 0

theorem gauge_of_subset_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (h : s ⊆ 0) : gauge s = 0

theorem gauge_nonneg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (x : E) : 0 ≤ gauge s x

The gauge is always nonnegative.

theorem gauge_neg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (symmetric : ∀ x ∈ s, -x ∈ s) (x : E) : gauge s (-x) = gauge s x

theorem gauge_neg_set_neg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (x : E) : gauge (-s) (-x) = gauge s x

theorem gauge_neg_set_eq_gauge_neg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (x : E) : gauge (-s) x = gauge s (-x)

theorem gauge_le_of_mem {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} {a : ℝ} (ha : 0 ≤ a) (hx : x ∈ a • s) : gauge s x ≤ a

theorem gauge_le_eq {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {a : ℝ} (hs₁ : Convex ℝ s) (hs₀ : 0 ∈ s) (hs₂ : Absorbent ℝ s) (ha : 0 ≤ a) : {x : E | gauge s x ≤ a} = ⋂ (r : ℝ), ⋂ (_ : a < r), r • s

theorem gauge_lt_eq' {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (absorbs : Absorbent ℝ s) (a : ℝ) : {x : E | gauge s x < a} = ⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s

theorem gauge_lt_eq {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (absorbs : Absorbent ℝ s) (a : ℝ) : {x : E | gauge s x < a} = ⋃ r ∈ Set.Ioo 0 a, r • s

theorem mem_openSegment_of_gauge_lt_one {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} (absorbs : Absorbent ℝ s) (hgauge : gauge s x < 1) : ∃ y ∈ s, x ∈ openSegment ℝ 0 y

theorem gauge_lt_one_subset_self {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : 0 ∈ s) (absorbs : Absorbent ℝ s) : {x : E | gauge s x < 1} ⊆ s

theorem gauge_le_one_of_mem {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} (hx : x ∈ s) : gauge s x ≤ 1

theorem gauge_add_le {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (x y : E) : gauge s (x + y) ≤ gauge s x + gauge s y

Gauge is subadditive.

theorem gauge_sum_le {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {ι : Type u_3} (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (t : Finset ι) (f : ι → E) : gauge s (∑ i ∈ t, f i) ≤ ∑ i ∈ t, gauge s (f i)

theorem self_subset_gauge_le_one {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : s ⊆ {x : E | gauge s x ≤ 1}

theorem Convex.gauge_le {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : 0 ∈ s) (absorbs : Absorbent ℝ s) (a : ℝ) : Convex ℝ {x : E | gauge s x ≤ a}

theorem Balanced.starConvex {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Balanced ℝ s) : StarConvex ℝ 0 s

theorem le_gauge_of_notMem {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} {a : ℝ} (hs₀ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s {x}) (hx : x ∉ a • s) : a ≤ gauge s x

theorem one_le_gauge_of_notMem {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} (hs₁ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s {x}) (hx : x ∉ s) : 1 ≤ gauge s x

theorem gauge_smul_of_nonneg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ] [MulActionWithZero α E] [IsScalarTower α ℝ (Set E)] {s : Set E} {a : α} (ha : 0 ≤ a) (x : E) : gauge s (a • x) = a • gauge s x

theorem gauge_smul_left_of_nonneg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ] [MulActionWithZero α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ] [IsScalarTower α ℝ E] {s : Set E} {a : α} (ha : 0 ≤ a) : gauge (a • s) = a⁻¹ • gauge s

theorem gauge_smul_left {E : Type u_2} [AddCommGroup E] [Module ℝ E] {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ] [Module α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ] [IsScalarTower α ℝ E] {s : Set E} (symmetric : ∀ x ∈ s, -x ∈ s) (a : α) : gauge (a • s) = |a|⁻¹ • gauge s

theorem gauge_norm_smul {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (‖r‖ • x) = gauge s (r • x)

theorem gauge_smul {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (r • x) = ‖r‖ * gauge s x

If s is balanced, then the Minkowski functional is ℂ-homogeneous.

theorem comap_gauge_nhds_zero_le {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] (ha : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) : Filter.comap (gauge s) (nhds 0) ≤ nhds 0

theorem gauge_eq_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [T1Space E] (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) : gauge s x = 0 ↔ x = 0

theorem gauge_pos {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [T1Space E] (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) : 0 < gauge s x ↔ x ≠ 0

theorem interior_subset_gauge_lt_one {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] (s : Set E) : interior s ⊆ {x : E | gauge s x < 1}

theorem gauge_lt_one_eq_self_of_isOpen {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs₁ : Convex ℝ s) (hs₀ : 0 ∈ s) (hs₂ : IsOpen s) : {x : E | gauge s x < 1} = s

theorem gauge_lt_one_of_mem_of_isOpen {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs₂ : IsOpen s) {x : E} (hx : x ∈ s) : gauge s x < 1

theorem gauge_lt_of_mem_smul {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (x : E) (ε : ℝ) (hε : 0 < ε) (hs₂ : IsOpen s) (hx : x ∈ ε • s) : gauge s x < ε

theorem mem_closure_of_gauge_le_one {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) (h : gauge s x ≤ 1) : x ∈ closure s

theorem mem_frontier_of_gauge_eq_one {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) (h : gauge s x = 1) : x ∈ frontier s

theorem tendsto_gauge_nhds_zero_nhdsGE {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : s ∈ nhds 0) : Filter.Tendsto (gauge s) (nhds 0) (nhdsWithin 0 (Set.Ici 0))

theorem tendsto_gauge_nhds_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : s ∈ nhds 0) : Filter.Tendsto (gauge s) (nhds 0) (nhds 0)

theorem continuousAt_gauge_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : s ∈ nhds 0) : ContinuousAt (gauge s) 0

If s is a neighborhood of the origin, then gauge s is continuous at the origin. See also continuousAt_gauge.

theorem comap_gauge_nhds_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hb : Bornology.IsVonNBounded ℝ s) (h₀ : s ∈ nhds 0) : Filter.comap (gauge s) (nhds 0) = nhds 0

theorem continuousAt_gauge {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : ContinuousAt (gauge s) x

If s is a convex neighborhood of the origin in a topological real vector space, then gauge s is continuous. If the ambient space is a normed space, then gauge s is Lipschitz continuous, see Convex.lipschitz_gauge.

theorem continuous_gauge {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : Continuous (gauge s)

If s is a convex neighborhood of the origin in a topological real vector space, then gauge s is continuous. If the ambient space is a normed space, then gauge s is Lipschitz continuous, see Convex.lipschitz_gauge.

theorem gauge_lt_one_eq_interior {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : {x : E | gauge s x < 1} = interior s

theorem gauge_lt_one_iff_mem_interior {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : gauge s x < 1 ↔ x ∈ interior s

theorem gauge_le_one_iff_mem_closure {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : gauge s x ≤ 1 ↔ x ∈ closure s

theorem gauge_eq_one_iff_mem_frontier {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : gauge s x = 1 ↔ x ∈ frontier s

noncomputable def gaugeSeminorm {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s) (hs₂ : Absorbent ℝ s) : Seminorm 𝕜 E

gauge s as a seminorm when s is balanced, convex and absorbent.

@[simp]

theorem gaugeSeminorm_toFun {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s) (hs₂ : Absorbent ℝ s) (x : E) : (gaugeSeminorm hs₀ hs₁ hs₂) x = gauge s x

theorem gaugeSeminorm_lt_one_of_isOpen {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : IsOpen s) {x : E} (hx : x ∈ s) : (gaugeSeminorm hs₀ hs₁ hs₂) x < 1

theorem gaugeSeminorm_ball_one {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : IsOpen s) : (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s

@[simp]

theorem Seminorm.gauge_ball {E : Type u_2} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) : gauge (p.ball 0 1) = ⇑p

Any seminorm arises as the gauge of its unit ball.

theorem Seminorm.gaugeSeminorm_ball {E : Type u_2} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) : gaugeSeminorm ⋯ ⋯ ⋯ = p

theorem gauge_unit_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : gauge (Metric.ball 0 1) x = ‖x‖

theorem gauge_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : gauge (Metric.ball 0 r) x = ‖x‖ / r

@[simp]

theorem gauge_closure_zero {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : gauge (closure 0) = 0

@[simp]

theorem gauge_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : gauge (Metric.closedBall 0 r) x = ‖x‖ / r

theorem mul_gauge_le_norm {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {r : ℝ} {x : E} (hs : Metric.ball 0 r ⊆ s) : r * gauge s x ≤ ‖x‖

theorem Convex.lipschitzWith_gauge {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {r : NNReal} (hc : Convex ℝ s) (hr : 0 < r) (hs : Metric.ball 0 ↑r ⊆ s) : LipschitzWith r⁻¹ (gauge s)

theorem Convex.lipschitz_gauge {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hc : Convex ℝ s) (h₀ : s ∈ nhds 0) : ∃ (K : NNReal), LipschitzWith K (gauge s)

theorem Convex.uniformContinuous_gauge {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hc : Convex ℝ s) (h₀ : s ∈ nhds 0) : UniformContinuous (gauge s)

theorem le_gauge_of_subset_closedBall {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {r : ℝ} {x : E} (hs : Absorbent ℝ s) (hr : 0 ≤ r) (hsr : s ⊆ Metric.closedBall 0 r) : ‖x‖ / r ≤ gauge s x