OAI/NumberTheory/Ostmann/Construction/ScheduledSampledValidity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_scaled_history_coefficient_units line 12
2. theorem OAI.Ostmann.fullAtomTransferWeight_sampled_valid line 49

   Source documentation

   No equation or unit condition is added to the analytic assumptions: both are obtained from the actual nonzero full coefficient and its original guards.

   theorem fullAtomTransferWeight_sampled_valid {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ)
       (i : I) (hi : role i = .word) (S : Finset ℤ) (n : ℕ)
       (C : CopyScheduleAtoms role n → ℕ) (P : Finset ℕ) (Q : ℕ)
       (hunit : ∀ p : P, (p : ℕ).Coprime Q) (x : TreeLeafIndex n → P)
       (t : FrequencyTree S n)
       (hu : ∀ k < n, ∀ a b, role a = .pivot k → role b = .pivot k → a = b)
       (hw : fullAtomTransferWeight role childBound pivotBound ranges leaf n
         (wordLeafScale role i hi n C (fun j => (x j : ℕ))) (frequencyTreeMap Subtype.val n t) ≠ 0) :
       let p := transferPivotArray (scheduleAtomSystem role childBound pivotBound) n
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.wordLeafScale, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.transferPivotArray, OAI.Ostmann.scheduleAtomSystem