mathlib3 documentation

analysis.convex.gauge

The Minkowksi functional #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 Minkowksi functional. gauge s x is the least (actually, an infimum) r such that x ∈ r • s.
gauge_seminorm: The Minkowski functional as a seminorm, when s is symmetric, convex and absorbent.

References #

H. H. Schaefer, Topological Vector Spaces

Tags #

Minkowski functional, gauge

noncomputable def gauge {E : Type u_2} [add_comm_group 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 = has_Inf.Inf {r : ℝ | 0 < r ∧ x ∈ r • s}

theorem gauge_def {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} :

gauge s x = has_Inf.Inf {r ∈ set.Ioi 0 | x ∈ r • s}

theorem gauge_def' {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} :

gauge s x = has_Inf.Inf {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} [add_comm_group 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} [add_comm_group 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} [add_comm_group E] [module ℝ E] {s : set E} {a : ℝ} {x : E} (absorbs : absorbent ℝ s) (h : gauge s x < a) :

∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s

@[simp]

theorem gauge_zero {E : Type u_2} [add_comm_group 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} [add_comm_group E] [module ℝ E] :

@[simp]

theorem gauge_empty {E : Type u_2} [add_comm_group E] [module ℝ E] :

theorem gauge_of_subset_zero {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (h : s ⊆ 0) :

theorem gauge_nonneg {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (x : E) :

0 ≤ gauge s x

The gauge is always nonnegative.

theorem gauge_neg {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (x : E) :

gauge s (-x) = gauge s x

theorem gauge_neg_set_neg {E : Type u_2} [add_comm_group 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} [add_comm_group E] [module ℝ E] {s : set E} (x : E) :

gauge (-s) x = gauge s (-x)

theorem gauge_le_of_mem {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {a : ℝ} {x : E} (ha : 0 ≤ a) (hx : x ∈ a • s) :

gauge s x ≤ a

theorem gauge_le_eq {E : Type u_2} [add_comm_group 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 : ℝ) (H : a < r), r • s

theorem gauge_lt_eq' {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (absorbs : absorbent ℝ s) (a : ℝ) :

{x : E | gauge s x < a} = ⋃ (r : ℝ) (H : 0 < r) (H : r < a), r • s

theorem gauge_lt_eq {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (absorbs : absorbent ℝ s) (a : ℝ) :

{x : E | gauge s x < a} = ⋃ (r : ℝ) (H : r ∈ set.Ioo 0 a), r • s

theorem gauge_lt_one_subset_self {E : Type u_2} [add_comm_group 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} [add_comm_group E] [module ℝ E] {s : set E} {x : E} (hx : x ∈ s) :

gauge s x ≤ 1

theorem self_subset_gauge_le_one {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} :

s ⊆ {x : E | gauge s x ≤ 1}

theorem convex.gauge_le {E : Type u_2} [add_comm_group 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.star_convex {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : balanced ℝ s) :

star_convex ℝ 0 s

theorem le_gauge_of_not_mem {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {a : ℝ} {x : E} (hs₀ : star_convex ℝ 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} [add_comm_group E] [module ℝ E] {s : set E} {x : E} (hs₁ : star_convex ℝ 0 s) (hs₂ : absorbs ℝ s {x}) (hx : x ∉ s) :

1 ≤ gauge s x

theorem gauge_smul_of_nonneg {E : Type u_2} [add_comm_group E] [module ℝ E] {α : Type u_4} [linear_ordered_field α] [mul_action_with_zero α ℝ] [ordered_smul α ℝ] [mul_action_with_zero α E] [is_scalar_tower α ℝ (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} [add_comm_group E] [module ℝ E] {α : Type u_4} [linear_ordered_field α] [mul_action_with_zero α ℝ] [ordered_smul α ℝ] [mul_action_with_zero α E] [smul_comm_class α ℝ ℝ] [is_scalar_tower α ℝ ℝ] [is_scalar_tower α ℝ E] {s : set E} {a : α} (ha : 0 ≤ a) :

gauge (a • s) = a⁻¹ • gauge s

theorem gauge_smul_left {E : Type u_2} [add_comm_group E] [module ℝ E] {α : Type u_4} [linear_ordered_field α] [mul_action_with_zero α ℝ] [ordered_smul α ℝ] [module α E] [smul_comm_class α ℝ ℝ] [is_scalar_tower α ℝ ℝ] [is_scalar_tower α ℝ E] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (a : α) :

gauge (a • s) = |a|⁻¹ • gauge s

theorem gauge_norm_smul {𝕜 : Type u_1} {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 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} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 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 interior_subset_gauge_lt_one {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [has_continuous_smul ℝ E] (s : set E) :

interior s ⊆ {x : E | gauge s x < 1}

theorem gauge_lt_one_eq_self_of_open {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [topological_space E] [has_continuous_smul ℝ E] (hs₁ : convex ℝ s) (hs₀ : 0 ∈ s) (hs₂ : is_open s) :

{x : E | gauge s x < 1} = s

theorem gauge_lt_one_of_mem_of_open {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [topological_space E] [has_continuous_smul ℝ E] (hs₁ : convex ℝ s) (hs₀ : 0 ∈ s) (hs₂ : is_open s) {x : E} (hx : x ∈ s) :

gauge s x < 1

theorem gauge_lt_of_mem_smul {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [topological_space E] [has_continuous_smul ℝ E] (x : E) (ε : ℝ) (hε : 0 < ε) (hs₀ : 0 ∈ s) (hs₁ : convex ℝ s) (hs₂ : is_open s) (hx : x ∈ ε • s) :

gauge s x < ε

theorem gauge_add_le {E : Type u_2} [add_comm_group 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

noncomputable def gauge_seminorm {𝕜 : Type u_1} {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 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

gauge_seminorm hs₀ hs₁ hs₂ = seminorm.of (gauge s) _ _

@[simp]

theorem gauge_seminorm_to_fun {𝕜 : Type u_1} {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E] (hs₀ : balanced 𝕜 s) (hs₁ : convex ℝ s) (hs₂ : absorbent ℝ s) (x : E) :

⇑(gauge_seminorm hs₀ hs₁ hs₂) x = gauge s x

theorem gauge_seminorm_lt_one_of_open {𝕜 : Type u_1} {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E] {hs₀ : balanced 𝕜 s} {hs₁ : convex ℝ s} {hs₂ : absorbent ℝ s} [topological_space E] [has_continuous_smul ℝ E] (hs : is_open s) {x : E} (hx : x ∈ s) :

⇑(gauge_seminorm hs₀ hs₁ hs₂) x < 1

theorem gauge_seminorm_ball_one {𝕜 : Type u_1} {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E] {hs₀ : balanced 𝕜 s} {hs₁ : convex ℝ s} {hs₂ : absorbent ℝ s} [topological_space E] [has_continuous_smul ℝ E] (hs : is_open s) :

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

@[protected, simp]

theorem seminorm.gauge_ball {E : Type u_2} [add_comm_group E] [module ℝ E] (p : seminorm ℝ E) :

gauge (p.ball 0 1) = ⇑p

Any seminorm arises as the gauge of its unit ball.

theorem seminorm.gauge_seminorm_ball {E : Type u_2} [add_comm_group E] [module ℝ E] (p : seminorm ℝ E) :

gauge_seminorm _ _ _ = p

theorem gauge_unit_ball {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) :

gauge (metric.ball 0 1) x = ‖x‖

theorem gauge_ball {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {r : ℝ} (hr : 0 < r) (x : E) :

gauge (metric.ball 0 r) x = ‖x‖ / r

theorem mul_gauge_le_norm {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} {r : ℝ} {x : E} (hs : metric.ball 0 r ⊆ s) :

r * gauge s x ≤ ‖x‖

theorem convex.lipschitz_with_gauge {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} {r : nnreal} (hc : convex ℝ s) (hr : 0 < r) (hs : metric.ball 0 ↑r ⊆ s) :

lipschitz_with r⁻¹ (gauge s)

theorem convex.uniform_continuous_gauge {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} (hc : convex ℝ s) (h₀ : s ∈ nhds 0) :

uniform_continuous (gauge s)