OAI/NumberTheory/Ostmann/Construction/ConstituentPartitionAssignment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.copyConstituentEquiv_positive_inverse line 13
2. theorem OAI.Ostmann.constituent_pivot_entry line 23
3. theorem OAI.Ostmann.constituent_partition_assignment line 37

   Source documentation

   The current prime assignment groups to the inserted atom state. In particular the pivot value is the product of all its original constituents.

   theorem constituent_partition_assignment {I : Type*} (role : I → CopyScheduleRole)
       (size : I → ℕ) (n : ℕ) (p : I) (hp : role p = .pivot n)
       (hu : ∀ i, role i = .pivot n → i = p)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → ℕ)
       (x : Fin (size p) → ℕ)
       (l : CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → ℕ) :
       (fun v => ((scheduleConstituentWord role size n v).map
           (scheduledPartitionAssignment (fun i : Σ a, Fin (size a) => role i.1)
             n (size p) (pivotConstituentEquiv role size n p hp hu) u x l)).prod) =
         scheduledInsertedAtoms role n (∏ k, x k)
           (fun h => ∏ k, l (constituentH role size n h k))
           (fun y => ∏ k, u (constituentY role size n y k)) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.scheduledPartitionAssignment, OAI.Ostmann.pivotConstituentEquiv, OAI.Ostmann.scheduledInsertedAtoms, OAI.Ostmann.constituentH, OAI.Ostmann.constituentY