OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeNodeFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingNodeArithmeticGuard line 11

   Source documentation

   The original nine arithmetic tests at a node, in terms of its products.

   def movingNodeArithmeticGuard (N B LH RH : ℕ) (s v w : ℤ) (P : ℕ) : Prop :=
   …

2. theorem OAI.Ostmann.movingRootState_arithmetic_guard line 16
3. def OAI.Ostmann.movingTopPivot line 32
4. def OAI.Ostmann.movingPrimeNodeFactor line 41

   Source documentation

   This factor uses only the current lists and three root frequencies. Descendant support is retained in the two child coefficients.

   noncomputable def movingPrimeNodeFactor {σ : Type*} (value : σ → ℕ)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (CL CR u : List σ) (XL XR : ℕ) (s v w : ℤ) : ℂ :=
   …

5. theorem OAI.Ostmann.movingPrimeNodeFactor_term line 55

   Source documentation

   The original guarded summand is exactly a root-only factor times the original two supported child coefficients. This is used only at actual prime outer giants, where the extra cross-branch frequency tests follow from size.

   theorem movingPrimeNodeFactor_term {σ : 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) :
       let u := movingCompensationSlots n a
   …

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