mathlib documentation

analysis.convex.gauge

The Minkowksi 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,

References #

Tags #

Minkowski functional, gauge

noncomputable def gauge {E : Type u_1} [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
theorem gauge_def {E : Type u_1} [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_1} [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_1} [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_1} [add_comm_group E] [module E] {s t : set E} (hs : absorbent s) (h : s t) :
theorem exists_lt_of_gauge_lt {E : Type u_1} [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_1} [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_1} [add_comm_group E] [module E] :
gauge 0 = 0
@[simp]
theorem gauge_empty {E : Type u_1} [add_comm_group E] [module E] :
theorem gauge_of_subset_zero {E : Type u_1} [add_comm_group E] [module E] {s : set E} (h : s 0) :
gauge s = 0
theorem gauge_nonneg {E : Type u_1} [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_1} [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_le_of_mem {E : Type u_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [add_comm_group E] [module E] {s : set E} :
s {x : E | gauge s x 1}
theorem convex.gauge_le {E : Type u_1} [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_1} [add_comm_group E] [module E] {s : set E} (hs : balanced s) :
theorem le_gauge_of_not_mem {E : Type u_1} [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_1} [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_1} [add_comm_group E] [module E] {α : Type u_2} [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 {E : Type u_1} [add_comm_group E] [module E] {α : Type u_2} [linear_ordered_field α] [mul_action_with_zero α ] [ordered_smul α ] [module α E] [is_scalar_tower α (set E)] {s : set E} (symmetric : ∀ (x : E), x s-x s) (r : α) (x : E) :
gauge s (r x) = |r| gauge s x

In textbooks, this is the homogeneity of the Minkowksi functional.

theorem gauge_smul_left_of_nonneg {E : Type u_1} [add_comm_group E] [module E] {α : Type u_2} [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) :
theorem gauge_smul_left {E : Type u_1} [add_comm_group E] [module E] {α : Type u_2} [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 : α) :
theorem interior_subset_gauge_lt_one {E : Type u_1} [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_1} [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_1} [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_1} [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_1} [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 {E : Type u_1} [add_comm_group E] [module E] {s : set E} (hs₀ : ∀ (x : E), x s-x s) (hs₁ : convex s) (hs₂ : absorbent s) :

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

Equations
@[simp]
theorem gauge_seminorm_to_fun {E : Type u_1} [add_comm_group E] [module E] {s : set E} (hs₀ : ∀ (x : E), x s-x 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 {E : Type u_1} [add_comm_group E] [module E] {s : set E} {hs₀ : ∀ (x : E), x s-x 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
@[protected, simp]
theorem seminorm.gauge_ball {E : Type u_1} [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_1} [add_comm_group E] [module E] (p : seminorm E) :
theorem gauge_unit_ball {E : Type u_1} [semi_normed_group E] [normed_space E] (x : E) :
theorem gauge_ball {E : Type u_1} [semi_normed_group E] [normed_space E] {r : } (hr : 0 < r) (x : E) :
theorem mul_gauge_le_norm {E : Type u_1} [semi_normed_group E] [normed_space E] {s : set E} {r : } {x : E} (hs : metric.ball 0 r s) :
r * gauge s x x