English
For any x, the gauge on the unit ball equals the norm of x.
Русский
Для любого x gauge на единичном шаре равен норме x.
LaTeX
$$$$ gauge (ball (0: E) 1) x = \\|x\\| $$$$
Lean4
/-- Any seminorm arises as the gauge of its unit ball. -/
@[simp]
protected theorem gauge_ball (p : Seminorm ℝ E) : gauge (p.ball 0 1) = p :=
by
ext x
obtain hp | hp := {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}.eq_empty_or_nonempty
· rw [gauge, hp, Real.sInf_empty]
by_contra h
have hpx : 0 < p x := (apply_nonneg _ _).lt_of_ne h
have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx
refine hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpx₂), inv_mul_lt_iff₀ hpx₂, mul_one]
exact lt_mul_of_one_lt_left hpx one_lt_two
refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp
· rintro ⟨hr, y, hy, rfl⟩
rw [p.mem_ball_zero] at hy
rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos hr]
exact mul_le_of_le_one_right hr.le hy.le
· have hpε : 0 < p x + ε := by positivity
refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε), inv_mul_lt_iff₀ hpε, mul_one]
exact lt_add_of_pos_right _ hε
