OAI/NumberTheory/Ostmann/Construction/ScheduledDistinctSources.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordTransferTemplate.DistinctProducts line 11
2. theorem OAI.Ostmann.scheduledHWord_nodup line 16
3. theorem OAI.Ostmann.scheduled_reverse_source_after line 25
4. theorem OAI.Ostmann.scheduledWordTemplate_distinctProducts line 40

   Source documentation

   The exact finite pivot addresses are fresh, and a single grouped pivot atom is inserted at each node. Thus the products use sets of ancestor pivots.

   theorem scheduledWordTemplate_distinctProducts {I A : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (depth n : ℕ) (hn : n ≤ depth)
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b)
       (path : List Bool) (current : CopyScheduleAtoms role n → ExpandedScheduledVariable A depth)
       (hinj : Function.Injective current) (hafter : ∀ v, ExpandedCoordinateAfter n (current v)) :
       (scheduledWordTemplate role (expandedPivotAddress A depth) childBound pivotBound n path current).DistinctProducts := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.ExpandedCoordinateAfter, OAI.Ostmann.scheduledWordTemplate, OAI.Ostmann.expandedPivotAddress