OAI/NumberTheory/Ostmann/Arithmetic/MovingCompensatedEquations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSampleAncestorScheme line 10
2. def OAI.Ostmann.movingSampleCompensation line 18
3. theorem OAI.Ostmann.movingSampleNode_products line 23
4. theorem OAI.Ostmann.movingSample_compensatedEquations line 67

   Source documentation

   No node equation is assumed here: all are forced by a nonzero original recursive coefficient and its compensation cutoff.

   theorem movingSample_compensatedEquations {σ : Type*} (value : σ → ℕ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (S : Finset ℤ) (n : ℕ) (t : FrequencyTree S n)
       (small bulk : TreeLeafTuple (List σ) n) (a : MovingSampleSlots σ n) (XL XR : ℕ)
       (hw : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound E) n
         ⟨n, buildMovingSlotData n (frequencyTreeMap Subtype.val n t) small bulk a, XL, XR⟩
         (frequencyTreeMap Subtype.val n t) ≠ 0) :
       let tz := frequencyTreeMap Subtype.val n t
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.frequencyTreeMap