-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
/-- 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`. -/
lemma spectrum_star_mul_self_nonneg {b : A} : ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x

Proof state:
case refine_1
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ IsSelfAdjoint (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2))

Tactic:
exact .smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)

Result:
no goals

Proof state:
case refine_3
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (↑2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2)) ⇑ContinuousMap.realToNNReal

Tactic:
refine (ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
  (ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <| by norm_num

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : cfc 0 a = cfc (fun x => x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
have h_eqOn := eqOn_of_cfc_eq_cfc (ha := ha) h_eq_negPart_a

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : cfc 0 a = cfc (fun x => x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
h_eqOn : Set.EqOn 0 (fun x => x⁻ ^ 3) (spectrum ℝ a)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
case refine_2
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ IsSelfAdjoint (-(star c * c))

Tactic:
exact .neg <| .star_mul_self c

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ spectrum ℝ (cfcₙ (fun x => x⁻) a ^ 3), 0 ≤ x

Tactic:
rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ (fun x => x⁻ ^ 3) '' spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ IsSelfAdjoint a

Tactic:
simp [a_def]

Result:
no goals

Proof state:
case refine_3
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2)) ⇑ContinuousMap.realToNNReal

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℝ]

Result:
case refine_3
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (↑2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2)) ⇑ContinuousMap.realToNNReal

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ -a⁻ * (a⁺ - a⁻) * a⁻ = a⁻ ^ 3

Tactic:
simp [mul_sub, sub_mul, ← mul_assoc, pow_succ]

Result:
no goals

Proof state:
case intro.intro
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
x : ℝ
⊢ 0 ≤ (fun x => x⁻ ^ 3) x

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x

Tactic:
simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ spectrum ℝ (cfcₙ (fun x => x⁻) a ^ 3), 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
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

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : cfc 0 a = cfc (fun x => x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
set c := b * a⁻

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal

Tactic:
rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)) ⇑ContinuousMap.realToNNReal

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
have ha : IsSelfAdjoint a := by simp [a_def]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ 0⁻ = 0

Tactic:
simp

Result:
no goals