Documentation

Mathlib.Analysis.Convex.Gauge

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

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.

Equations

gauge s x = sInf {r : ℝ | 0 < r ∧ x ∈ r • s}

Instances For

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) :

Set.Nonempty {r : ℝ | 0 < r ∧ x ∈ r • s}

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 : Set E} {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] :

@[simp]

theorem gauge_empty {E : Type u_2} [AddCommGroup E] [Module ℝ E] :

theorem gauge_of_subset_zero {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} (h : 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 : E) (y : E) :

gauge s (x + y) ≤ gauge s x + gauge s y

Gauge is subadditive.

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_not_mem {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_not_mem {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_4} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] [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_4} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] [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_4} [LinearOrderedField α] [MulActionWithZero α ℝ] [OrderedSMul α ℝ] [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} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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' {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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) :

gauge s x = 1 ↔ x ∈ frontier s

@[simp]

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

(gaugeSeminorm hs₀ hs₁ hs₂) x = gauge s x

def gaugeSeminorm {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [IsROrC 𝕜] [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.

Equations

gaugeSeminorm hs₀ hs₁ hs₂ = Seminorm.of (gauge s) (_ : ∀ (x y : E), gauge s (x + y) ≤ gauge s x + gauge s y) (_ : ∀ (r : 𝕜) (x : E), gauge s (r • x) = ‖r‖ * gauge s x)

Instances For

theorem gaugeSeminorm_lt_one_of_isOpen {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [IsROrC 𝕜] [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} [IsROrC 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : IsOpen s) :

Seminorm.ball (gaugeSeminorm hs₀ hs₁ hs₂) 0 1 = s

@[simp]

theorem Seminorm.gauge_ball {E : Type u_2} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) :

gauge (Seminorm.ball p 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 (_ : Balanced ℝ (Seminorm.ball p 0 1)) (_ : Convex ℝ (Seminorm.ball p 0 1)) (_ : Absorbent ℝ (Seminorm.ball p 0 1)) = 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

@[deprecated gauge_ball]

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