[Merged by Bors] - feat(CstarRing): various lemmas related to the spectral order and the CFC

[dupuisf]

This PR proves various lemmas for C*-algebras, such as

• if a ≤ b, then ‖a‖ ≤ ‖b‖
• star a * b *a ≤ ‖b‖ • (star a * a)
• if a is positive, then ‖a‖ ∈ spectrum ℝ a.

It also puts an order instance on Unitization ℂ A, needed to prove the above.

• depends on: [Merged by Bors] - feat(ContinuousMapZero): add StarOrderedRing instances #13650
• depends on: [Merged by Bors] - feat(IsSelfAdjoint): add aesop tags relevant for proving IsSelfAdjoint a automatically #13673

---

[github-actions]

PR summary 67968682d3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
15 files Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.NormedSpace.Star.GelfandDuality Mathlib.Analysis.NormedSpace.Spectrum Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus Mathlib.Analysis.NormedSpace.Star.Spectrum Mathlib.Analysis.NormedSpace.Algebra Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Order Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict Mathlib.Topology.ContinuousFunction.UniqueCFC Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus Mathlib.Topology.ContinuousFunction.FunctionalCalculus Mathlib.Tactic Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus	1
Mathlib.Tactic.ContinuousFunctionalCalculus	122

---

Declarations diff

+ CstarRing.conjugate_le_norm_smul
+ CstarRing.conjugate_le_norm_smul'
+ CstarRing.instNonnegSpectrumClassComplexNonUnital
+ CstarRing.instNonnegSpectrumClassComplexUnital
+ CstarRing.mul_star_le_algebraMap_norm_sq
+ CstarRing.nnnorm_mem_spectrum_of_nonneg
+ CstarRing.norm_le_norm_of_nonneg_of_le
+ CstarRing.norm_mem_spectrum_of_nonneg
+ CstarRing.norm_or_neg_norm_mem_spectrum
+ CstarRing.star_mul_le_algebraMap_norm_sq
+ IsSelfAdjoint.coe_mem_spectrum_complex
+ IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm
+ IsSelfAdjoint.toReal_spectralRadius_eq_norm
+ StarOrderedRing.nonneg_iff_quasispectrum_nonneg
+ StarOrderedRing.nonneg_iff_spectrum_nonneg
+ _root_.NNReal.spectralRadius_mem_spectrum
+ _root_.Real.spectralRadius_mem_spectrum
+ _root_.Real.spectralRadius_mem_spectrum_or
+ algebraMap_eq_coe
+ coe_mem_spectrum_real_of_nonneg
+ inl_sub
+ inr_le_iff
+ inr_nonneg_iff
+ inr_sub
+ instPartialOrder
+ instStarOrderedRing
- mul_star_le_algebraMap_norm_sq
- star_mul_le_algebraMap_norm_sq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(ContinuousMapZero): add StarOrderedRing instances #13650
• [Merged by Bors] - feat(IsSelfAdjoint): add aesop tags relevant for proving IsSelfAdjoint a automatically #13673
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

Lots of simplifications. Probably for most to work you need to merge master. You may also need to add the lemmas I suggest.

I'm very happy with how this is working out. Just appealing to the Unitization as in normal arguments is great. Thanks for doing this work. It really justifies the design of everything we've done so far.

[j-loreaux]

In the long comment above, I think actually we want selfadjoint versions of everything. Here's what I have now. (Sorry for the complicated review; I just kept realizing things weren't quite as nice as we wanted and I knew we would want more lemmas.) Obviously not all of this goes in this file.

open ComplexOrder in
instance CstarRing.instNonnegSpectrumClassComplex {A : Type*} [NormedRing A] [CompleteSpace A]
    [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedAlgebra ℂ A]
    [StarModule ℂ A] : NonnegSpectrumClass ℂ A where
  quasispectrum_nonneg_of_nonneg a ha x := by
    rw [mem_quasispectrum_iff]
    refine (Or.elim · ge_of_eq fun hx ↦ ?_)
    obtain ⟨y, hy, rfl⟩ := (IsSelfAdjoint.of_nonneg ha).spectrumRestricts.algebraMap_image ▸ hx
    simpa using spectrum_nonneg_of_nonneg ha hy

lemma Real.spectralRadius_mem_spectrum_or {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
    [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty) :
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a := by
  obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha
  simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, norm_eq_abs]
  exact abs_choice x |>.imp (fun h ↦ by rwa [h]) (fun h ↦ by simpa [h])

lemma NNReal.spectralRadius_mem_spectrum {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
    [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty)
    (ha' : SpectrumRestricts a ContinuousMap.realToNNReal) :
    (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a := by
  rw [← spectrum.algebraMap_mem_iff ℝ, NNReal.algebraMap_eq_coe, ← ENNReal.toReal]
  have := Real.spectralRadius_mem_spectrum_or ha
  rwa [or_iff_left_of_imp (fun h ↦ ?_)] at this
  have : (spectralRadius ℝ a).toReal ≤ 0 :=
    nonpos_of_neg_nonneg <| ha'.rightInvOn h ▸ NNReal.zero_le_coe
  simpa [le_antisymm this ENNReal.toReal_nonneg] using h

lemma Real.spectralRadius_mem_spectrum {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
    [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty)
    (ha' : SpectrumRestricts a ContinuousMap.realToNNReal) :
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a :=
  NNReal.spectralRadius_mem_spectrum ha ha'

lemma IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm {a : A} (ha : IsSelfAdjoint a) :
    (spectralRadius ℂ a).toReal = ‖a‖ := by
  simp [ha.spectralRadius_eq_nnnorm]

lemma IsSelfAdjoint.toReal_spectralRadius_eq_norm {a : A} (ha : IsSelfAdjoint a) :
    (spectralRadius ℝ a).toReal = ‖a‖ := by
  simp [ha.spectrumRestricts.spectralRadius_eq, ha.spectralRadius_eq_nnnorm]

lemma CstarRing.norm_or_neg_norm_mem_spectrum [Nontrivial A] {a : A}
    (ha : IsSelfAdjoint a := by cfc_tac) : ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a := by
  have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts
  have := ha.toReal_spectralRadius_eq_norm
  convert Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

lemma CstarRing.nnnorm_mem_spectrum_of_nonneg [Nontrivial A] {a : A} (ha : 0 ≤ a := by cfc_tac) :
    ‖a‖₊ ∈ spectrum ℝ≥0 a := by
  have : IsSelfAdjoint a := .of_nonneg ha
  convert NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)
  · simp [this.spectrumRestricts.spectralRadius_eq, this.spectralRadius_eq_nnnorm]
  · exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

lemma CstarRing.norm_mem_spectrum_of_nonneg [Nontrivial A] {a : A} (ha : 0 ≤ a := by cfc_tac) :
    ‖a‖ ∈ spectrum ℝ a := by
  simpa using spectrum.algebraMap_mem ℝ <| CstarRing.nnnorm_mem_spectrum_of_nonneg ha

[dupuisf]

Thanks for the extensive review, @j-loreaux ! I think I've addressed everything except for the two comments I've left open.

[j-loreaux]

Thanks!

bors d+

[mathlib-bors]

✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dupuisf]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style