OAI/NumberTheory/Ostmann/Construction/ConstituentCopiedAssignment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.constituent_inverse_atom line 12
2. def OAI.Ostmann.constituentH line 20
3. def OAI.Ostmann.constituentY line 30
4. theorem OAI.Ostmann.constituentH_output line 40
5. theorem OAI.Ostmann.constituentY_output line 49
6. theorem OAI.Ostmann.constituent_copied_assignment_word line 58
7. theorem OAI.Ostmann.constituent_retained_assignment_word line 76
8. theorem OAI.Ostmann.constituent_copied_assignment line 93

   Source documentation

   Taking products of the copied prime slots is exactly the atom assignment used by the reverse transfer system.

   theorem constituent_copied_assignment {I : Type*} (role : I → CopyScheduleRole)
       (size : I → ℕ) (n : ℕ)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → ℕ)
       (l r : CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → ℕ) :
       (fun v => ((scheduleConstituentWord role size (n + 1) v).map
           (scheduledCopiedAssignment (fun i : Σ a, Fin (size a) => role i.1) n u l r)).prod) =
         scheduledCopiedAssignment role n
           (fun y => ∏ k, u (constituentY role size n y k))
           (fun h => ∏ k, l (constituentH role size n h k))
           (fun h => ∏ k, r (constituentH role size n h k)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.scheduledCopiedAssignment, OAI.Ostmann.constituentY, OAI.Ostmann.constituentH