English
Let s be a convex absorbent subset of a real vector space E with 0 ∈ s. For every a ≥ 0, the sublevel set {x ∈ E : gauge s x ≤ a} equals the intersection over all real r with a < r of r · s.
Русский
Пусть s — выпуклое поглощающее множество в вещественном векторном пространстве E и 0 ∈ s. Для любого a ≥ 0 множество {x ∈ E : gauge s x ≤ a} равно ⋂_{r> a} r · s.
LaTeX
$$$$(\\operatorname{Convex}_{\\mathbb{R}}(s)) \\land (0 \\in s) \\land (\\operatorname{Absorbent}_{\\mathbb{R}}(s)) \\land a \\ge 0 \\Rightarrow \\{x \\in E \\mid \\mathrm{gauge}(s,x) \\le a\\} = \\bigcap_{r \\in \\mathbb{R}, a < r} r\\,s.$$$$
Lean4
theorem gauge_le_eq (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : Absorbent ℝ s) (ha : 0 ≤ a) :
{x | gauge s x ≤ a} = ⋂ (r : ℝ) (_ : a < r), r • s :=
by
ext x
simp_rw [Set.mem_iInter, Set.mem_setOf_eq]
refine ⟨fun h r hr => ?_, fun h => le_of_forall_pos_lt_add fun ε hε => ?_⟩
· have hr' := ha.trans_lt hr
rw [mem_smul_set_iff_inv_smul_mem₀ hr'.ne']
obtain ⟨δ, δ_pos, hδr, hδ⟩ := exists_lt_of_gauge_lt hs₂ (h.trans_lt hr)
suffices (r⁻¹ * δ) • δ⁻¹ • x ∈ s by rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ
refine hs₁.smul_mem_of_zero_mem hs₀ hδ ⟨by positivity, ?_⟩
rw [inv_mul_le_iff₀ hr', mul_one]
exact hδr.le
· have hε' := (lt_add_iff_pos_right a).2 (half_pos hε)
exact (gauge_le_of_mem (ha.trans hε'.le) <| h _ hε').trans_lt (add_lt_add_left (half_lt_self hε) _)
