OAI/Algebra/Finitistic/Bar/BlockIndexEquiv.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.Multibar.base_run_injective line 8

   Source documentation

   The first X uniquely determines the length of the preceding D block.

   theorem base_run_injective (i j : ℕ) (p q : List Bool)
       (h : List.replicate i false ++ true :: p = List.replicate j false ++ true :: q) :
       i=j ∧ p=q := by
   …

2. theorem OAI.DerivedBar.Multibar.pattern_injective line 26

   Source documentation

   Consecutive block lengths have a unique literal D/X word.

   theorem pattern_injective (r : ℕ) : Function.Injective (pattern r) := by
   …

   Mentions: OAI.DerivedBar.Multibar.pattern

3. def OAI.DerivedBar.Multibar.parseOfCount line 38

   Source documentation

   Parse a word of a specified count without changing its block data.

   def parseOfCount (r : ℕ) (p : List Bool) (h : count p=r) : Blocks r := h ▸ parse p

   Mentions: OAI.DerivedBar.Multibar.count, OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.parse

4. theorem OAI.DerivedBar.Multibar.pattern_parseOfCount line 40
5. theorem OAI.DerivedBar.Multibar.parseOfCount_pattern line 45
6. def OAI.DerivedBar.Multibar.Indexed.shapeOfList line 52
7. theorem OAI.DerivedBar.Multibar.Indexed.toList_shapeOfList line 57
8. def OAI.DerivedBar.Multibar.Indexed.castShape line 65
9. theorem OAI.DerivedBar.Multibar.Indexed.toList_castShape line 67
10. def OAI.DerivedBar.Multibar.Indexed.shapeOfBlocks line 73

    Source documentation

    Construct the degree-indexed tensor shape of a tuple of block lengths.

    def shapeOfBlocks (r : ℕ) (b : Blocks r) : Shape (r+total r b) r :=
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.total

11. theorem OAI.DerivedBar.Multibar.Indexed.toList_shapeOfBlocks line 76
12. def OAI.DerivedBar.Multibar.Indexed.blocksOfShape line 80
13. theorem OAI.DerivedBar.Multibar.Indexed.pattern_blocksOfShape line 83
14. theorem OAI.DerivedBar.Multibar.Indexed.total_blocksOfShape line 86
15. def OAI.DerivedBar.Multibar.Indexed.blockDegreeEquiv line 93

    Source documentation

    Reindex the finite block-length diagonal by the existing tensor shapes. The shift by r occurs in the degree, not in a hidden tensor-power replacement.

    def blockDegreeEquiv (r m : ℕ) : {b : Blocks r // total r b=m} ≃ Shape (r+m) r where
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.total, OAI.DerivedBar.Multibar.Indexed.Shape