Sublevel sets of the gauge as dilates

For a convex neighbourhood s of 0 in a real topological vector space, Mathlib's gauge_le_one_iff_mem_closure identifies the sublevel set {x | gauge s x ≤ 1} with the closure of s. This file records the dilated form: for 0 < t, the sublevel set {x | gauge s x ≤ t} is t • closure s, which is also the closure of the dilate t • s (TauCeti.setOfPred_gauge_le_eq_closure_smul_of_pos); for a bounded s the identity extends to t = 0 (TauCeti.setOfPred_gauge_le_eq_closure_smul), via the zero-gauge characterization TauCeti.gauge_le_zero_iff_mem_closure_zero. For a convex body, which is closed, this turns bounds on the gauge into membership in a dilate of the body (ConvexBody.gauge_le_iff_mem_smul), which is how successive minima are stated. For such a body, the gauge is also positive away from 0 (ConvexBody.gauge_pos_iff). The gauge of the preimage of a set under a linear map is the gauge of the set at the image point (LinearMap.gauge_preimage).

References

The statements of TauCeti.setOfPred_gauge_le_eq_closure_smul_of_pos and TauCeti.setOfPred_gauge_le_eq_closure_smul follow setOf_gauge_le_eq_closure_smul_of_pos and setOf_gauge_le_eq_closure_smul in the successive-minima proposal for Mathlib by Kevin H. Wilson, Mathlib/Analysis/Convex/Gauge.lean at https://github.com/khwilson/mathlib4/blob/8423d1c878e50d8504a230ffd9b6ec76ce6a08eb/Mathlib/Analysis/Convex/Gauge.lean (Apache 2.0), renamed to Mathlib's current setOfPred_gauge_* prefix.

theorem gauge_le_iff_mem_smul_closure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {t : ℝ} {x : E} (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (ht : 0 < t) : gauge s x ≤ t ↔ x ∈ t • closure s

For a convex neighbourhood s of 0 and 0 < t, the gauge of x is at most t exactly when x lies in the dilate t • closure s.

theorem TauCeti.setOfPred_gauge_le_eq_closure_smul_of_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {t : ℝ} (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (ht : 0 < t) : {x : E | gauge s x ≤ t} = closure (t • s)

For a convex neighbourhood s of 0 and 0 < t, the sublevel set {x | gauge s x ≤ t} is the closure of the dilate t • s.

theorem TauCeti.gauge_le_zero_iff_mem_closure_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {x : E} (hb : Bornology.IsVonNBounded ℝ s) (hs₀ : s ∈ nhds 0) : gauge s x ≤ 0 ↔ x ∈ closure {0}

For a bounded neighbourhood s of 0, the gauge of x is at most 0 exactly when x lies in closure {0}. No separation axiom or convexity is needed.

theorem TauCeti.setOfPred_gauge_le_eq_closure_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {t : ℝ} (hc : Convex ℝ s) (hb : Bornology.IsVonNBounded ℝ s) (hs₀ : s ∈ nhds 0) (ht : 0 ≤ t) : {x : E | gauge s x ≤ t} = closure (t • s)

For a bounded convex neighbourhood s of 0 and 0 ≤ t, the sublevel set {x | gauge s x ≤ t} is the closure of the dilate t • s. At t = 0 both sides are closure {0}, which is {0} in a T1 space. See TauCeti.setOfPred_gauge_le_eq_closure_smul_of_pos for 0 < t, which needs no boundedness.

theorem LinearMap.gauge_preimage {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (f : E →ₗ[ℝ] F) (s : Set F) (x : E) : gauge (⇑f ⁻¹' s) x = gauge s (f x)

The gauge of the preimage of s under a linear map f is the gauge of s at f x.

theorem ConvexBody.gauge_le_iff_mem_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : ConvexBody E} (hK : 0 ∈ interior ↑K) {t : ℝ} (ht : 0 < t) {x : E} : gauge (↑K) x ≤ t ↔ x ∈ t • ↑K

For a convex body K with 0 in its interior and 0 < t, the gauge of x is at most t exactly when x lies in the dilate t • K.

theorem ConvexBody.gauge_pos_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : ConvexBody E} (hK : 0 ∈ interior ↑K) {x : E} : 0 < gauge (↑K) x ↔ x ≠ 0

For a convex body K with 0 in its interior, the gauge of x is positive exactly when x ≠ 0.