OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeRootGuard.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotData.Follows.frequencies line 12
2. theorem OAI.Ostmann.movingFrequencySkeleton_follows line 22
3. theorem OAI.Ostmann.movingRootState_prime_support_iff line 28
4. theorem OAI.Ostmann.movingRootState_prime_guard_product line 48

   Source documentation

   Nonzero child coefficients remove the zero-history cases. Thus the remaining top guard depends only on the actual prime lists and the two root frequencies, as required before the child sums are multiplied.

   theorem movingRootState_prime_guard_product {σ : Type*} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
       (hs : s ≠ 0) (hsV : s.natAbs ≤ V (n + 1))
       (l r : ScheduledFrequencyIndex V n)
       (small bulk : TreeLeafTuple (List σ) (n + 1))
       (a : TreeLeafTuple (Fin 4 → σ) n) (XL XR : ℕ)
       (hXL : XL.Prime) (hXR : XR.Prime)
       (hVL : V (n + 1) < XL) (hVR : V (n + 1) < XR) (C : ℂ) (guard : Prop) :
       let u := movingCompensationSlots n a
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationSlots