English
A technical bound: the square of the second coordinate of Unitization.splitMul is bounded by the second coordinate of the star-conjugate product; this is a key step in establishing C*-norm for Unitization.
Русский
Техническое неравенство: квадрат второй координаты в распаковке Unitization.splitMul ограничен квадратом второй координаты произведения с звёздочкой, ключевой шаг для нормирования Unitization.
LaTeX
$$$\| (\mathrm{Unitization.splitMul}\; x).\text{snd} \|^2 \le \| (\mathrm{Unitization.splitMul}\; (\star x \cdot x)).\text{snd} \|$$$
Lean4
/-- A C⋆-algebra over a densely normed field is a regular normed algebra. -/
instance instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where
isometry_mul' :=
AddMonoidHomClass.isometry_of_norm (mul 𝕜 E) fun a =>
NNReal.eq_iff.mp <|
show ‖mul 𝕜 E a‖₊ = ‖a‖₊ by
rw [← sSup_unitClosedBall_eq_nnnorm]
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_
· exact (Metric.nonempty_closedBall.mpr zero_le_one).image _
· rintro - ⟨x, hx, rfl⟩
exact ((mul 𝕜 E a).unit_le_opNorm x <| mem_closedBall_zero_iff.mp hx).trans (opNorm_mul_apply_le 𝕜 E a)
· have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)
refine ⟨_, ⟨k • star a, ?_, rfl⟩, ?_⟩
·
simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using
(NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹)
· simp only [map_smul, nnnorm_smul, mul_apply', CStarRing.nnnorm_self_mul_star]
rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]
