OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternTree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternSamples line 13

   Source documentation

   Fixed external labels and internal equality classes are kept separate. The latter number depends only on depth, not on the bulk length.

   def movingPatternSamples (C : Type*) (n : ℕ)
       (pattern : Bool × MovingSampleIndex n → C) (side : Bool) : MovingSampleSlots C n :=
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingSampleSlots

2. theorem OAI.Ostmann.movingPatternSamples_map line 17
3. theorem OAI.Ostmann.movingPatternSamples_pair line 26
4. theorem OAI.Ostmann.treeLeafMap_list_comp line 31
5. def OAI.Ostmann.movingPatternSlotData line 39
6. theorem OAI.Ostmann.movingPatternSlotData_evaluate line 48

   Source documentation

   Evaluating the fixed pattern tree gives precisely the original sampled constructor with those class values. No new sampler is introduced.

   theorem movingPatternSlotData_evaluate {A B C : Type*} (external : B → A) (internal : C → A)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List B) n)
       (pattern : Bool × MovingSampleIndex n → C) (side : Bool) :
       (movingPatternSlotData n t small bulk pattern side).map (Sum.elim external internal) =
         buildMovingSlotData n t (treeLeafMap (List.map external) n small)
           (treeLeafMap (List.map external) n bulk)
           (movingPatternSamples A n (internal ∘ pattern) side) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternSlotData, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingPatternSamples

7. theorem OAI.Ostmann.movingPatternSlotData_levels line 60