OAI/Analysis/FactorGeneration/SpectralPinching.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Actual sign splitting inside a prescribed residual corner.

  1. theorem OAI.Generator.Tracial.positivePart_right_support line 25

    Source documentation

    Functional calculus positive parts retain a given right support.

    theorem positivePart_right_support (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x)
    (p : AlgebraProjection M) (hp : x*p.val=x) : x⁺*p.val=x⁺ := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  2. theorem OAI.Generator.Tracial.positiveSupport_le_corner line 41
  3. def OAI.Generator.Tracial.cornerSpectralShift line 48
  4. theorem OAI.Generator.Tracial.cornerSpectralShift_selfAdjoint line 51
  5. theorem OAI.Generator.Tracial.cornerSpectralShift_support line 58
  6. def OAI.Generator.Tracial.cornerSpectralCut line 62
  7. theorem OAI.Generator.Tracial.cornerSpectralCut_le line 65
  8. def OAI.Generator.Tracial.CornerPartition.binary line 72

    Source documentation

    Splitting p at an explicitly given subprojection q.

    def binary (p q : AlgebraProjection M) (hq : q ≤ p) : CornerPartition p :=
…

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

  9. theorem OAI.Generator.Tracial.CornerPartition.binary_pinch line 89
  10. def OAI.Generator.Tracial.cornerSpectralPartition line 97

    Source documentation

    The finite corner partition constructed from the shifted positive part.

    def cornerSpectralPartition (p : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : IsSelfAdjoint x) (t : ℝ) : CornerPartition p :=
…

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

  11. theorem OAI.Generator.Tracial.cornerSpectralCut_lower line 102

    Source documentation

    Its high block has the promised spectral lower bound.

    theorem cornerSpectralCut_lower (p : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : IsSelfAdjoint x) (t : ℝ) :
    0 ≤ (cornerSpectralCut p x t).val*x*(cornerSpectralCut p x t).val -
      (t : ℂ) • (cornerSpectralCut p x t).val := by
…

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

  12. theorem OAI.Generator.Tracial.cornerSpectralCut_upper line 121

    Source documentation

    The low block has the opposite shifted sign in the same corner.

    theorem cornerSpectralCut_upper (p : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : IsSelfAdjoint x) (t : ℝ) :
    let r := p.val-(cornerSpectralCut p x t).val
…

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

  13. theorem OAI.Generator.Tracial.CornerPartition.binary_pinch_of_commutes line 162
  14. theorem OAI.Generator.Tracial.cornerSpectralCut_commutes line 175
  15. theorem OAI.Generator.Tracial.cornerSpectralPartition_pinch line 191
  16. theorem OAI.Generator.Tracial.compress_scalar_shift line 215
  17. theorem OAI.Generator.Tracial.lower_bound_compress line 225
  18. theorem OAI.Generator.Tracial.upper_bound_compress line 233
  19. structure OAI.Generator.Tracial.SpectralInterval line 241
  20. def OAI.Generator.Tracial.SpectralInterval.midpoint line 251
  21. def OAI.Generator.Tracial.SpectralInterval.highProjection line 253
  22. def OAI.Generator.Tracial.SpectralInterval.lowProjection line 255
  23. theorem OAI.Generator.Tracial.SpectralInterval.high_le line 260
  24. theorem OAI.Generator.Tracial.SpectralInterval.low_le line 263
  25. def OAI.Generator.Tracial.SpectralInterval.high line 267
  26. def OAI.Generator.Tracial.SpectralInterval.low line 274
  27. def OAI.Generator.Tracial.SpectralInterval.child line 281
  28. theorem OAI.Generator.Tracial.SpectralInterval.child_le line 283
  29. theorem OAI.Generator.Tracial.SpectralInterval.child_width line 288
  30. theorem OAI.Generator.Tracial.SpectralInterval.child_total line 292
  31. theorem OAI.Generator.Tracial.SpectralInterval.child_orthogonal line 296
  32. theorem OAI.Generator.Tracial.SpectralInterval.child_compression_total line 308
  33. def OAI.Generator.Tracial.SpectralInterval.level line 328
  34. theorem OAI.Generator.Tracial.SpectralInterval.level_le line 332
  35. theorem OAI.Generator.Tracial.SpectralInterval.level_width line 336
  36. theorem OAI.Generator.Tracial.SpectralInterval.level_total line 344
  37. theorem OAI.Generator.Tracial.SpectralInterval.level_orthogonal line 357
  38. theorem OAI.Generator.Tracial.SpectralInterval.level_compression_total line 368
  39. def OAI.Generator.Tracial.SpectralInterval.partition line 386
  40. theorem OAI.Generator.Tracial.SpectralInterval.partition_pinch line 390
  41. theorem OAI.Generator.Tracial.SpectralInterval.error_upper line 408
  42. def OAI.Generator.Tracial.SpectralInterval.approximant line 415
  43. theorem OAI.Generator.Tracial.SpectralInterval.approximant_error_sum line 418
  44. theorem OAI.Generator.Tracial.SpectralInterval.approximant_error_nonneg line 425
  45. theorem OAI.Generator.Tracial.SpectralInterval.approximant_error_upper line 430
  46. theorem OAI.Generator.Tracial.SpectralInterval.approximant_norm_error line 441

    Source documentation

    Actual operator norm approximation, not an assumed energy budget.

    theorem approximant_norm_error (n : ℕ) (hab : I.lo ≤ I.hi) :
    ‖I.proj.val*x*I.proj.val-I.approximant hx n‖ ≤ (I.hi-I.lo)/(2:ℝ)^n := by
…
  47. theorem OAI.Generator.Tracial.SpectralInterval.exists_approximant line 453
  48. def OAI.Generator.Tracial.initialSpectralInterval line 466

    Source documentation

    Start the construction with the actual operator norm bounds in any corner.

    def initialSpectralInterval (p : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : IsSelfAdjoint x) : SpectralInterval x := by
…

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

  49. theorem OAI.Generator.Tracial.exists_finite_spectral_approximation line 486

    Source documentation

    An actual finite orthogonal spectral approximation of a compressed self-adjoint operator. All projections and coefficients are constructed.

    theorem exists_finite_spectral_approximation (p : AlgebraProjection M)
    (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (ε : ℝ) (hε : 0 < ε) :
    ∃ (Q : CornerPartition p) (c : Fin Q.size → ℝ),
      Q.pinch x=p.val*x*p.val ∧
      ‖p.val*x*p.val-∑ i, (c i : ℂ) • (Q.piece i).val‖ < ε := by
…

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

  50. theorem OAI.Generator.Tracial.kernel_invariant_of_commutes line 515
  51. theorem OAI.Generator.Tracial.kernelProjection_commutes line 523
  52. theorem OAI.Generator.Tracial.positiveSupport_commutes_of_commutes line 542
  53. theorem OAI.Generator.Tracial.selfAdjoint_commutes_star_right line 563
  54. theorem OAI.Generator.Tracial.positiveSupport_commutes_of_selfAdjoint line 569
  55. theorem OAI.Generator.Tracial.cornerSpectralCut_commutes_with line 574
  56. theorem OAI.Generator.Tracial.SpectralInterval.child_commutes line 586
  57. theorem OAI.Generator.Tracial.SpectralInterval.level_commutes line 593
  58. theorem OAI.Generator.Tracial.SpectralInterval.partition_commutes line 598
  59. theorem OAI.Generator.Tracial.exists_finite_spectral_approximation_commuting line 606

    Source documentation

    The finite construction retains a prescribed commutation relation.

    theorem exists_finite_spectral_approximation_commuting (p : AlgebraProjection M)
    (x y : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (hxy : Commute x y)
    (hp : Commute p.val y) (ε : ℝ) (hε : 0 < ε) :
    ∃ (Q : CornerPartition p) (c : Fin Q.size → ℝ),
      Q.pinch x=p.val*x*p.val ∧ (∀ i, Commute (Q.piece i).val y) ∧
      ‖p.val*x*p.val-∑ i, (c i : ℂ) • (Q.piece i).val‖ < ε := by
…

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

  60. theorem OAI.Generator.Tracial.exists_finite_spectral_approximation_preserving_commutant line 626

    Source documentation

    One constructed partition preserves the whole displayed commutant, not a separately selected partition for each test operator.

    theorem exists_finite_spectral_approximation_preserving_commutant (p : AlgebraProjection M)
    (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (ε : ℝ) (hε : 0 < ε) :
    ∃ (Q : CornerPartition p) (c : Fin Q.size → ℝ),
      Q.pinch x=p.val*x*p.val ∧
      (∀ y : M.toStarSubalgebra, Commute x y → Commute p.val y →
        ∀ i, Commute (Q.piece i).val y) ∧
      ‖p.val*x*p.val-∑ i, (c i : ℂ) • (Q.piece i).val‖ < ε := by
…

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