OAI/NumberTheory/Ostmann/Construction/ConstituentWords.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.SurvivingConstituent line 13
2. def OAI.Ostmann.scheduleConstituentWord line 16
3. theorem OAI.Ostmann.scheduleConstituentWord_length line 22
4. theorem OAI.Ostmann.scheduleConstituentWord_nodup line 27
5. theorem OAI.Ostmann.scheduleConstituentWord_disjoint line 35
6. theorem OAI.Ostmann.scheduleConstituentWord_prod line 44
7. theorem OAI.Ostmann.scheduleConstituentWord_total_prod line 54

   Source documentation

   Multiplying all grouped words gives the original total prime product, without omission or repeated use of a constituent.

   theorem scheduleConstituentWord_total_prod {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (q : SurvivingConstituent role size n → ℕ) :
       (∏ v : CopyScheduleAtoms role n, ((scheduleConstituentWord role size n v).map q).prod) = ∏ i, q i := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduleConstituentWord

8. theorem OAI.Ostmann.scheduleConstituentWord_pairwise line 64

   Source documentation

   Constituent-level pairwise coprimality implies the exact top grouped coprimality required by the full Fourier coefficient.

   theorem scheduleConstituentWord_pairwise {I : Type*}
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (q : SurvivingConstituent role size n → ℕ)
       (hq : Pairwise (fun i j => (q i).Coprime (q j))) :
       Pairwise (fun v w : CopyScheduleAtoms role n =>
         ((scheduleConstituentWord role size n v).map q).prod.Coprime
           ((scheduleConstituentWord role size n w).map q).prod) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduleConstituentWord