OAI/NumberTheory/Ostmann/Construction/SelectedConstituentWord.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.wordLeafSlot_atom line 11
2. theorem OAI.Ostmann.wordLeafSlot_constituent_exists line 21
3. theorem OAI.Ostmann.constituent_outside_selected_word line 35
4. theorem OAI.Ostmann.other_constituent_outside_selected_primes line 48
5. theorem OAI.Ostmann.grouped_wordLeaf_outside line 71
6. theorem OAI.Ostmann.grouped_wordLeaf_selected line 85
7. theorem OAI.Ostmann.grouped_wordLeaf_assignment line 111

   Source documentation

   Grouping introduces a fixed multiplier in each selected word, while every other atom is independent of the unexposed selected primes.

   theorem grouped_wordLeaf_assignment :
       (fun a : CopyScheduleAtoms role n => ((scheduleConstituentWord role size n a).map
         (wordLeafAssignment (fun j : Σ a, Fin (size a) => role j.1) i hi n y x)).prod) =
       wordLeafAssignment role i.1 hi n
         (fun a => ((scheduleConstituentWord role size n a.val).map
           (wordLeafAssignment (fun j : Σ a, Fin (size a) => role j.1) i hi n y (fun _ => 1))).prod)
         (fun t => ((scheduleConstituentWord role size n (wordLeafSlot role i.1 hi n t)).map
           (wordLeafAssignment (fun j : Σ a, Fin (size a) => role j.1) i hi n y (fun _ => 1))).prod * x t) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.wordLeafAssignment, OAI.Ostmann.wordLeafSlot