OAI/NumberTheory/Ostmann/Construction/ScheduledLeafProducts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledNodeLeafValues line 11
2. theorem OAI.Ostmann.scheduledNodeLeafValues_products line 17
3. theorem OAI.Ostmann.wordLeafScale_cast line 35

   Source documentation

   Transporting the root index does not change which word leaves scale.

   theorem wordLeafScale_cast {I G : Type*} [Mul G]
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
       {a b : ℕ} (e : a = b) (C : CopyScheduleAtoms role b → G) (x : TreeLeafIndex b → G) :
       (fun v => wordLeafScale role i hi b C x
         (Equiv.cast (congrArg (CopyScheduleAtoms role) e) v)) =
         wordLeafScale role i hi a
           (fun v => C (Equiv.cast (congrArg (CopyScheduleAtoms role) e) v))
           (fun v => x (Equiv.cast (congrArg TreeLeafIndex e) v)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.wordLeafScale

4. theorem OAI.Ostmann.scheduledNodeValues_wordLeafScale line 46
5. theorem OAI.Ostmann.scheduledNodeValues_H_product line 59

   Source documentation

   These are exactly the two bulk factors used by SampledPivotHistory.

   theorem scheduledNodeValues_H_product {I G : Type*} [Fintype I] [Zero G] [CommMonoid G]
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
       (n : ℕ) (j : Fin (2 ^ n - 1)) (b : Bool) (C : CopyScheduleAtoms role n → G)
       (x : TreeLeafIndex n → G) (p : Fin (2 ^ n - 1) → G) :
       (∏ a : CopyScheduleH role (scheduledNodeLevel n j),
         scheduledNodeValues role n j (wordLeafScale role i hi n C x) p
           ⟨.inl (b, a.val), a.property⟩) =
         (∏ a : CopyScheduleH role (scheduledNodeLevel n j),
           scheduledNodeValues role n j C p ⟨.inl (b, a.val), a.property⟩) *
           (if b then
             ((actualChildProducts n ((treeLeafTupleEquiv G n).symm x)).getD j.val (1, 1)).1
           else ((actualChildProducts n ((treeLeafTupleEquiv G n).symm x)).getD j.val (1, 1)).2) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduledNodeLevel, OAI.Ostmann.scheduledNodeValues, OAI.Ostmann.wordLeafScale, OAI.Ostmann.actualChildProducts, OAI.Ostmann.treeLeafTupleEquiv