English
If s is star-convex at 0 and s is absorbed by {x}, and x ∉ a · s, then a ≤ gauge s x.
Русский
Если s звездо-выпукло относительно 0, и s абсорбирует {x}, и x ∉ a · s, тогда a ≤ gauge s x.
LaTeX
$$$$(\\text{StarConvex}(0,s)) \\land (\\text{Absorbs}(s, {x})) \\land (x \\notin a \\cdot s) \\Rightarrow a \\le gauge(s,x).$$$$
Lean4
theorem le_gauge_of_notMem (hs₀ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s { x }) (hx : x ∉ a • s) : a ≤ gauge s x :=
by
rw [starConvex_zero_iff] at hs₀
obtain ⟨r, hr, h⟩ := hs₂.exists_pos
refine le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_
rintro b ⟨hb, x, hx', rfl⟩
refine not_lt.1 fun hba => hx ?_
have ha := hb.trans hba
refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩
· rw [← div_eq_inv_mul]
exact div_le_one_of_le₀ hba.le ha.le
· dsimp only
rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']
