OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplateCoefficient line 11
2. theorem OAI.Ostmann.movingTemplateCompensationEquiv_restore line 20
3. theorem OAI.Ostmann.movingTemplateCoefficient_restored line 28
4. theorem OAI.Ostmann.movingTemplateCoefficient_prime_node line 45

   Source documentation

   Pair the surviving templates and restore each sampled compensation vector in both children. This is the actual product recursion on the prescribed roles.

   theorem movingTemplateCoefficient_prime_node {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (hs : s ≠ 0) (hsV : s.natAbs ≤ V (n + 1))
       (left right : MovingRegularSlot n r m → σ) (XL XR : ℕ)
       (hXL : XL.Prime) (hXR : XR.Prime)
       (hVL : V (n + 1) < XL) (hVR : V (n + 1) < XR) :
       movingTemplateCoefficient value outside μ childBound pivotBound V F φ G (n + 1) r m s
         (movingTemplatePairSample n r m left right) XL XR =
       ∑ a : TreeLeafTuple (Fin 4 → σ) n, (movingCompensationPrior (μ n) n a : ℂ) *
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateCoefficient, OAI.Ostmann.movingTemplatePairSample, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationPrior