OAI/RepresentationTheory/FiniteUnitary/CommutingBlocks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.CommutingBlocks.orthogonal_sum_norm_sq line 11
2. lemma OAI.CubeShuffle.CommutingBlocks.projection_inner_zero line 24
3. lemma OAI.CubeShuffle.CommutingBlocks.projection_sandwich_norm line 31
4. theorem OAI.CubeShuffle.CommutingBlocks.resolution_norm_bound line 41

   Source documentation

   Orthogonal sector norm bound, without tensor-product classification.

   theorem resolution_norm_bound (P : ι → V →L[ℂ] V)
       (hP : ∀ i, IsStarProjection (P i))
       (horth : ∀ i j, i≠j → P i*P j=0) (hsum : ∑ i,P i=1)
       (A : V →L[ℂ] V) (hcomm : ∀ i, Commute A (P i))
       (c : ℝ) (hc : 0≤c) (hbound : ∀ i, ‖A*P i‖≤c) : ‖A‖≤c := by
   …

5. theorem OAI.CubeShuffle.CommutingBlocks.sector_sandwich_le line 71

   Source documentation

   Sandwich comparison for one orthogonal sector subordinate to a coarser invariant projection. This proves the needed PSD comparison at the norm level.

   theorem sector_sandwich_le (T P A B : V →L[ℂ] V)
       (hT : IsStarProjection T) (hP : IsStarProjection P)
       (hTP : T*P=T) (hcomm : Commute A T) (hA : ‖A‖≤1) :
       ‖B.adjoint*A*T*B‖≤‖B.adjoint*P*B‖ := by
   …

6. lemma OAI.CubeShuffle.CommutingBlocks.resolution_commute line 93
7. lemma OAI.CubeShuffle.CommutingBlocks.resolution_sum_mul line 100
8. lemma OAI.CubeShuffle.CommutingBlocks.resolution_truncated_norm line 110
9. theorem OAI.CubeShuffle.CommutingBlocks.resolution_exception_bound line 127

   Source documentation

   Exceptional-sector comparison, faithful to FAC's positive sandwich argument but not requiring tensor-product representation machinery.

   theorem resolution_exception_bound (T Q : ι → V →L[ℂ] V)
       (hT : ∀ i, IsStarProjection (T i))
       (horth : ∀ i j, i≠j → T i*T j=0) (hsum : ∑ i,T i=1)
       (hQ : ∀ i, IsStarProjection (Q i)) (hTQ : ∀ i,T i*Q i=T i)
       (A B : V →L[ℂ] V) (hcomm : ∀ i, Commute A (T i))
       (hA : ‖A‖≤1) (hB : ‖B‖≤1)
       (S : Finset ι) (c : ℝ) (hc : 0≤c) (hbound : ∀ i∉S, ‖A*T i‖≤c) :
       ‖B.adjoint*A*B‖≤c+∑ i∈S,‖B.adjoint*Q i*B‖ := by
   …

10. def OAI.CubeShuffle.CommutingBlocks.choice line 162
11. lemma OAI.CubeShuffle.CommutingBlocks.choice_commute line 167
12. def OAI.CubeShuffle.CommutingBlocks.sector line 176
13. lemma OAI.CubeShuffle.CommutingBlocks.sector_insert line 180
14. lemma OAI.CubeShuffle.CommutingBlocks.sector_congr line 185
15. lemma OAI.CubeShuffle.CommutingBlocks.sector_factor_commute line 192
16. lemma OAI.CubeShuffle.CommutingBlocks.sector_projection line 197
17. lemma OAI.CubeShuffle.CommutingBlocks.sector_sum line 211
18. lemma OAI.CubeShuffle.CommutingBlocks.sector_absorb_factor line 236
19. lemma OAI.CubeShuffle.CommutingBlocks.sector_orthogonal line 252
20. def OAI.CubeShuffle.CommutingBlocks.blockProduct line 278
21. lemma OAI.CubeShuffle.CommutingBlocks.norm_noncommProd_le line 283
22. def OAI.CubeShuffle.CommutingBlocks.blocks line 293
23. lemma OAI.CubeShuffle.CommutingBlocks.blocks_norm_le_one line 297
24. lemma OAI.CubeShuffle.CommutingBlocks.blocks_sector_commute line 302
25. lemma OAI.CubeShuffle.CommutingBlocks.blocks_sector_norm line 316
26. def OAI.CubeShuffle.CommutingBlocks.coarse line 345
27. lemma OAI.CubeShuffle.CommutingBlocks.coarse_projection line 348
28. lemma OAI.CubeShuffle.CommutingBlocks.sector_coarse line 357
29. theorem OAI.CubeShuffle.CommutingBlocks.blocks_exception_bound line 377

    Source documentation

    Actual commuting-block exceptional estimate, with no tensor irreducible hypothesis. The local gaps are for each represented finite block.

    theorem blocks_exception_bound (hP : ∀ i, IsStarProjection (P i))
        (A : ι → V →L[ℂ] V) (hA : ∀ i j, Commute (A i) (A j))
        (hAP : ∀ i j, Commute (A i) (P j)) (hn : ∀ i,‖A i‖≤1)
        (θ : ℝ) (hθ : 0≤θ) (hθ1 : θ≤1) (hgap : ∀ i,‖A i*(1-P i)‖≤θ)
        (B : V →L[ℂ] V) (hB : ‖B‖≤1) (n : ℕ) :
        ‖B.adjoint*blocks A hA*B‖≤θ^n+
          ∑ E : Finset ι, if E.card<n then ‖B.adjoint*coarse P hcomm E*B‖ else 0 := by
    …

    Mentions: OAI.CubeShuffle.CommutingBlocks.blocks, OAI.CubeShuffle.CommutingBlocks.coarse