OAI/NumberTheory/Ostmann/Construction/ScheduleFullCoprime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduleAtomFullCoprimeValid line 13

   Source documentation

   The original requirements at every reversed transfer: current atoms are pairwise coprime, and the inserted pivot is coprime to every current atom.

   noncomputable def scheduleAtomFullCoprimeValid {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ) :
       (n : ℕ) → (CopyScheduleAtoms role n → ℕ) → FrequencyTree ℤ n → Prop
     | 0, x, _ => Pairwise (fun i j => (x i).Coprime (x j))
     | n + 1, x, t =>
         let P := historyPivot (scheduleAtomSystem role childBound pivotBound) ⟨n + 1, x⟩
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyPivot, OAI.Ostmann.scheduleAtomSystem

2. theorem OAI.Ostmann.schedule_full_coprime_reduced line 26
3. theorem OAI.Ostmann.schedule_full_coprime_iff_reduced line 40

   Source documentation

   There is no loss of original support: all the omitted H tests follow from the reconstruction equation and the retained frequency-unit tests.

   theorem schedule_full_coprime_iff_reduced {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n)
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b)
       (hv : ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) n ⟨n, x⟩ t)
       (hunits : scheduleAtomUnitsValid role childBound pivotBound (totalAtomUnitRanges role) n x t) :
       scheduleAtomFullCoprimeValid role childBound pivotBound n x t ↔
         Pairwise (fun i j => (x i).Coprime (x j)) ∧
           scheduleAtomCoprimalitiesValid role childBound pivotBound n x t := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleAtomUnitsValid, OAI.Ostmann.totalAtomUnitRanges, OAI.Ostmann.scheduleAtomFullCoprimeValid, OAI.Ostmann.scheduleAtomCoprimalitiesValid