OAI/Analysis/FactorGeneration/SpectralApproximation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Generator.Tracial.CornerPartition.jointPiece line 19
2. theorem OAI.Generator.Tracial.CornerPartition.jointPiece_le_left line 23
3. theorem OAI.Generator.Tracial.CornerPartition.jointPiece_le_right line 27
4. theorem OAI.Generator.Tracial.CornerPartition.jointPiece_orthogonal line 31
5. theorem OAI.Generator.Tracial.CornerPartition.jointPiece_total line 40
6. def OAI.Generator.Tracial.CornerPartition.joint line 46
7. theorem OAI.Generator.Tracial.CornerPartition.joint_refines_left line 49
8. theorem OAI.Generator.Tracial.CornerPartition.joint_refines_right line 54
9. theorem OAI.Generator.Tracial.CornerPartition.joint_sum_left line 60

   Source documentation

   A spectral sum on Q is represented exactly on the common refinement.

   theorem joint_sum_left (c : Fin Q.size → ℂ) :
       (∑ a : Fin Q.size × Fin R.size, c a.1 • (Q.jointPiece R hc a).val)=
         ∑ i, c i • (Q.piece i).val := by
   …

10. theorem OAI.Generator.Tracial.CornerPartition.joint_sum_right line 69
11. theorem OAI.Generator.Tracial.exists_joint_spectral_approximation line 85
12. theorem OAI.Generator.Tracial.exists_complex_spectral_approximation line 111

    Source documentation

    Complex finite spectral sums are constructed from the joint real and imaginary approximations. No small pinching-energy premise occurs.

    theorem exists_complex_spectral_approximation (p : AlgebraProjection M)
        (a b : M.toStarSubalgebra) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b)
        (hab : Commute a b) (hpa : Commute p.val a) (hpb : Commute p.val b)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ (S : CornerPartition p) (c : Fin S.size → ℂ),
          ‖p.val*(a+Complex.I • b)*p.val-∑ i, c i • (S.piece i).val‖ < ε := by
    …

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

13. def OAI.Generator.Tracial.identityProjection line 142
14. theorem OAI.Generator.Tracial.exists_normal_spectral_approximation line 144
15. theorem OAI.Generator.Tracial.exists_unitary_spectral_approximation line 154
16. def OAI.Generator.Tracial.algebraInclusion line 171
17. def OAI.Generator.Tracial.includedProjection line 174
18. def OAI.Generator.Tracial.includedUnitPartition line 182
19. theorem OAI.Generator.Tracial.includedUnitPartition_mem line 194
20. theorem OAI.Generator.Tracial.exists_unitary_subalgebra_spectral_approximation line 198
21. theorem OAI.Generator.Tracial.CornerPartition.joint_preserves_commutant line 231
22. theorem OAI.Generator.Tracial.CornerPartition.joint_spectral_sum_left line 240
23. theorem OAI.Generator.Tracial.CornerPartition.joint_spectral_sum_right line 250
24. theorem OAI.Generator.Tracial.exists_finite_abelian_spectral_refinement line 262
25. theorem OAI.Generator.Tracial.orthogonal_family_sum_projection line 306
26. theorem OAI.Generator.Tracial.exists_completed_orthogonal_family line 324
27. def OAI.Generator.Tracial.CornerPartition.blockIndices line 376
28. theorem OAI.Generator.Tracial.CornerPartition.blockIndices_disjoint line 380
29. theorem OAI.Generator.Tracial.CornerPartition.sum_blockIndices line 387