English
If spectra of a and b are restricted, the spectrum of a+b is restricted accordingly.
Русский
Если спектры a и b ограничены, спектр a+b ограничен должным образом.
LaTeX
$$SpectrumRestricts (a+b) ContinuousMap.realToNNReal$$
Lean4
/-- The `ℝ`-spectrum of an element of the form `star b * b` in a C⋆-algebra is nonnegative.
This is the key result used to establish `CStarAlgebra.instNonnegSpectrumClass`. -/
theorem spectrum_star_mul_self_nonneg {b : A} : ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x := by
-- for convenience we'll work with `a := star b * b`, which is selfadjoint.
set a := star b * b with a_def
have ha : IsSelfAdjoint a := by
simp [a_def]
-- the key element to consider is `c := b * a⁻`, which satisfies `- (star c * c) = a⁻ ^ 3`.
set c := b * a⁻
have h_eq_negPart_a : -(star c * c) = a⁻ ^ 3 :=
calc
-(star c * c) = -a⁻ * a * a⁻ := by
simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def, neg_mul,
IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]
_ = -a⁻ * (a⁺ - a⁻) * a⁻ := congr(-a⁻ * $(CFC.posPart_sub_negPart a ha) * a⁻).symm
_ = a⁻ ^ 3 := by
simp [mul_sub, pow_succ]
-- the spectrum of `- (star c * c) = a⁻ ^ 3` is nonnegative, since the function on the right
-- is nonnegative on the spectrum of `a`.
have h_c_spec₀ : SpectrumRestricts (-(star c * c)) (ContinuousMap.realToNNReal ·) :=
by
simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]
rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]
rintro - ⟨x, -, rfl⟩
positivity
-- the spectrum of `c * star c` is nonnegative, since squares of selfadjoint elements have
-- nonnegative spectrum, and `c * star c = 2 • (ℜ c ^ 2 + ℑ c ^ 2) + (- (star c * c))`,
-- and selfadjoint elements with nonnegative spectrum are closed under addition.
have h_c_spec₁ : SpectrumRestricts (c * star c) ContinuousMap.realToNNReal :=
by
rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]
refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
· exact .smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)
· exact .neg <| .star_mul_self c
· rw [← Nat.cast_smul_eq_nsmul ℝ]
refine
(ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
(ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <|
by
simp
-- therefore `- (star c * c) = 0` and so `a⁻ ^ 3 = 0`. By properties of the continuous functional
-- calculus, `fun x ↦ x⁻ ^ 3` is zero on the spectrum of `a`, `0 ≤ x` for `x ∈ spectrum ℝ a`.
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a
have h_eqOn := eqOn_of_cfc_eq_cfc (ha := ha) h_eq_negPart_a
exact fun x hx ↦ negPart_eq_zero.mp <| pow_eq_zero (h_eqOn hx).symm
