English
Let a≥0 and b≥0 with b unit. Then a ≤ b if and only if the norm of sqrt(a) times b^(-1/2) is at most 1.
Русский
Пусть a≥0, b≥0 и b единично. Тогда a ≤ b тогда и только тогда, когда норма sqrt(a) · b^(-1/2) не превосходит 1.
LaTeX
$$a \\le b \\quad\\Longleftrightarrow\\quad \\|\\sqrt a \\cdot b^{-(1/2)}\\| \\le 1$$
Lean4
theorem le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
a ≤ b ↔ ‖sqrt a * (b : A) ^ (-(1 / 2) : ℝ)‖ ≤ 1 :=
by
lift b to Aˣ using hbu
have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) := conjugate_nonneg_of_nonneg ha rpow_nonneg
conv_rhs =>
rw [← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul,
IsSelfAdjoint.of_nonneg (sqrt_nonneg a), IsSelfAdjoint.of_nonneg rpow_nonneg, ← mul_assoc, mul_assoc _ _ (sqrt a),
sqrt_mul_sqrt_self a, CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
·
calc
_ ≤ ↑b ^ (-(1 / 2) : ℝ) * (b : A) * ↑b ^ (-(1 / 2) : ℝ) :=
IsSelfAdjoint.of_nonneg rpow_nonneg |>.conjugate_le_conjugate h
_ = 1 := conjugate_rpow_neg_one_half b.isUnit
·
calc
a = (sqrt ↑b * ↑b ^ (-(1 / 2) : ℝ)) * a * (↑b ^ (-(1 / 2) : ℝ) * sqrt ↑b) :=
by
simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]
norm_num
simp [CFC.rpow_zero (b : A)]
_ = sqrt ↑b * (↑b ^ (-(1 / 2) : ℝ) * a * ↑b ^ (-(1 / 2) : ℝ)) * sqrt ↑b := by simp only [mul_assoc]
_ ≤ b := conjugate_le_conjugate_of_nonneg h (sqrt_nonneg _) |>.trans <| by simp [CFC.sqrt_mul_sqrt_self (b : A)]
