OAI/Analysis/KadisonKastler/IndexedCuts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.noPreservationCut line 15
2. def OAI.KadisonKastler.preservationCut line 21
3. theorem OAI.KadisonKastler.noPreservationCut_zero line 26
4. theorem OAI.KadisonKastler.noPreservationCut_append line 32

   Source documentation

   Cutting between two subwords leaves exactly the creation prefix and the annihilation suffix, in their original order.

   theorem noPreservationCut_append (C A : ι → B) (l₁ l₂ : List ι) :
       noPreservationCut C A (l₁ ++ l₂) l₁.length =
         (l₁.map C).prod * annihilationProduct A l₂ := by
   …

   Mentions: OAI.KadisonKastler.noPreservationCut, OAI.KadisonKastler.annihilationProduct

5. theorem OAI.KadisonKastler.preservationCut_append line 41
6. theorem OAI.KadisonKastler.freeCutSum_eq_indexedCuts line 51

   Source documentation

   There are n+1 cuts without preservation and n with preservation.

   theorem freeCutSum_eq_indexedCuts (C D A : ι → B) (l : List ι) :
       freeCutSum C D A l =
         (∑ k ∈ range (l.length + 1), noPreservationCut C A l k) +
         ∑ k ∈ range l.length, preservationCut C D A l k := by
   …

   Mentions: OAI.KadisonKastler.freeCutSum, OAI.KadisonKastler.noPreservationCut, OAI.KadisonKastler.preservationCut

7. theorem OAI.KadisonKastler.centeredLetterProduct_eq_indexedCuts line 72