OAI/Analysis/FactorGeneration/SpectralStates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Additivity on commuting self-adjoint operators, proved using actual common spectral refinements. The commutation hypothesis is essential to this proof.

  1. theorem OAI.Generator.Tracial.dimensionSpectralValue_add_of_commute line 22
  2. theorem OAI.Generator.Tracial.dimensionSpectralValue_sub_of_commute line 90
  3. theorem OAI.Generator.Tracial.dimensionSpectralValue_sub_norm_le_of_commute line 100
  4. theorem OAI.Generator.Tracial.SpectralInterval.child_endpoints line 127
  5. theorem OAI.Generator.Tracial.SpectralInterval.level_endpoints line 134
  6. theorem OAI.Generator.Tracial.exists_positive_spectral_approximation line 147

    Source documentation

    A positive operator has arbitrarily accurate finite positive spectral approximants preserving its entire commutant.

    theorem exists_positive_spectral_approximation
    (x : M.toStarSubalgebra) (hx : 0 ≤ x) (ε : ℝ) (hε : 0 < ε) :
    ∃ (Q : CornerPartition (⟨1,IsStarProjection.one _⟩ : AlgebraProjection M))
      (c : Fin Q.size → ℝ),
      (∀ i, 0 ≤ c i) ∧
      (∀ y : M.toStarSubalgebra, Commute x y → ∀ i, Commute (Q.piece i).val y) ∧
      ‖x-∑ i, (c i : ℂ) • (Q.piece i).val‖ < ε := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.CornerPartition, OAI.Generator.Tracial.AlgebraProjection

  7. theorem OAI.Generator.Tracial.dimensionSpectralValue_nonneg line 182
  8. theorem OAI.Generator.Tracial.dimensionSpectralValue_mono_of_commute line 202
  9. theorem OAI.Generator.Tracial.positive_spectral_cut_domination line 228
  10. theorem OAI.Generator.Tracial.positive_spectral_cut_ne_zero line 247
  11. theorem OAI.Generator.Tracial.dimensionSpectralValue_spectral_cut_lower line 266
  12. theorem OAI.Generator.Tracial.dimensionSpectralValue_pos line 287
  13. theorem OAI.Generator.Tracial.dimensionSpectralValue_eq_zero_iff_of_nonneg line 299
  14. def OAI.Generator.Tracial.AlgebraProjection.unitaryConjugate line 321
  15. theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_unitaryConjugate line 326
  16. theorem OAI.Generator.Tracial.traceFreeDimension_unitaryConjugate line 348
  17. theorem OAI.Generator.Tracial.dimensionSpectralValue_unitary_conjugate line 354
  18. theorem OAI.Generator.Tracial.dimensionSpectralValue_star_mul_self line 437