OAI/NumberTheory/Ostmann/Construction/ScheduledWordLeafProducts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.wordLeafHSlot line 10
2. abbrev OAI.Ostmann.WordLeafHOutside line 22
3. def OAI.Ostmann.wordLeafHPartition line 26
4. theorem OAI.Ostmann.copied_wordLeafHSlot line 32
5. def OAI.Ostmann.copiedWordLeafOutside line 44

   Source documentation

   Every other H coordinate is among the primes held fixed in the conditional leaf expectation, including the currently sampled pivot groups.

   noncomputable def copiedWordLeafOutside {I : Type*} (role : I → CopyScheduleRole)
       (i : I) (hi : role i = .word) (n : ℕ) (b : Bool)
       (h : WordLeafHOutside role i hi n) : WordLeafOutside role i hi (n + 1) :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.WordLeafHOutside, OAI.Ostmann.WordLeafOutside

6. theorem OAI.Ostmann.wordLeaf_H_product line 64

   Source documentation

   The actual H product factors into a fixed coefficient and the selected leaf-prime product. This is an equality before any coprimality restriction.

   theorem wordLeaf_H_product {I M : Type*} [Fintype I] [CommMonoid M]
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n : ℕ) (b : Bool)
       (y : WordLeafOutside role i hi (n + 1) → M) (x : TreeLeafIndex (n + 1) → M) :
       (∏ h : CopyScheduleH role n,
         wordLeafAssignment role i hi (n + 1) y x ⟨.inl (b, h.val), h.property⟩) =
         (∏ h : WordLeafHOutside role i hi n, y (copiedWordLeafOutside role i hi n b h)) *
           ∏ t : TreeLeafIndex n, x (if b then .inl t else .inr t) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.wordLeafAssignment, OAI.Ostmann.WordLeafHOutside, OAI.Ostmann.copiedWordLeafOutside