English
The gaugeSeminorm constructed from the unit ball of p equals p.
Русский
Гауж-семинорм, построенный из единичной сферы p, равен p.
LaTeX
$$$$ gaugeSeminorm (p.\\ balanced\\_ball\\_zero\\ 1) (p.\\ convex\\_ball 0 1) (p.\\ absorbent\\_ball\\_zero\\ zero\\_lt\\_one) = p. $$$$
Lean4
/-- If `s` is a convex neighborhood of the origin in a topological real vector space, then `gauge s`
is continuous. If the ambient space is a normed space, then `gauge s` is Lipschitz continuous, see
`Convex.lipschitz_gauge`. -/
theorem continuousAt_gauge (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) : ContinuousAt (gauge s) x :=
by
have ha : Absorbent ℝ s := absorbent_nhds_zero hs₀
refine (nhds_basis_Icc_pos _).tendsto_right_iff.2 fun ε hε₀ ↦ ?_
rw [← map_add_left_nhds_zero, eventually_map]
have : ε • s ∩ -(ε • s) ∈ 𝓝 0 :=
inter_mem ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀)
(neg_mem_nhds_zero _ ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀))
filter_upwards [this] with y hy
constructor
· rw [sub_le_iff_le_add]
calc
gauge s x = gauge s (x + y + (-y)) := by simp
_ ≤ gauge s (x + y) + gauge s (-y) := (gauge_add_le hc ha _ _)
_ ≤ gauge s (x + y) + ε := add_le_add_left (gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)) _
·
calc
gauge s (x + y) ≤ gauge s x + gauge s y := gauge_add_le hc ha _ _
_ ≤ gauge s x + ε := add_le_add_left (gauge_le_of_mem hε₀.le hy.1) _
