OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeNodeTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPrimeNodeFactor_transfer_product line 13

   Source documentation

   On a retained integer substitution, the supported child coefficients supply the pairwise and frequency-unit tests of the new node. Its remaining bounds are exactly the range inequalities used by the full transfer theorem.

   theorem movingPrimeNodeFactor_transfer_product {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ)
       (u : TreeLeafTuple (List σ) n) (small bulk : TreeLeafTuple (List σ) (n + 1))
       (XL XR : ℕ) (s v w : ℤ) (I : Finset ℕ)
       (hI : ∀ p ∈ I, 0 < p)
       (hsV : s.natAbs ≤ V (n + 1))
       (hv : v.natAbs ≤ childBound (n + 1)) (hw : w.natAbs ≤ childBound (n + 1)) :
       let U := MovingSlotReversal.naturalProduct value (flattenMovingSlots n u)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots