OAI/NumberTheory/Ostmann/Arithmetic/MovingRecursiveCompensation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingCompensatedExtra line 11
2. theorem OAI.Ostmann.movingSlotCutoff_compensated line 16
3. theorem OAI.Ostmann.MovingSlotState.compensation_rootData line 24
4. theorem OAI.Ostmann.movingLocalExtra_compensated line 31
5. theorem OAI.Ostmann.movingRecursiveWeight_compensated line 40

   Source documentation

   Each node contributes its newly sampled compensation exactly once, including off-support samples where both sides vanish.

   theorem movingRecursiveWeight_compensated {σ : Type*} (value : σ → ℕ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (a : MovingSampleSlots σ n) (XL XR : ℕ) :
       recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound (movingCompensatedExtra value E)) n
         ⟨n, buildMovingSlotData n t small bulk a, XL, XR⟩ t =
           (movingSampleProduct value a : ℂ) *
             recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
               (movingSlotCutoff value childBound pivotBound E) n
               ⟨n, buildMovingSlotData n t small bulk a, XL, XR⟩ t := by
   …

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

6. theorem OAI.Ostmann.movingSupportedWeight_mul line 85
7. theorem OAI.Ostmann.movingSampledWeight_compensated_supported line 94

   Source documentation

   Exact compensated prior times the supported coefficient with node compensations removed. This is the scalar used by the pattern comparison.

   theorem movingSampledWeight_compensated_supported {σ : Type*} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (XL XR : ℕ) :
       movingSampledWeight value μ childBound pivotBound (movingGuardedLeaf value outside F)
         (movingGuardedExtra value outside (movingLocalExtra (movingCompensatedExtra value E)))
         n t small bulk XL XR =
         ∑ a : MovingSampleSlots σ n,
           (((movingSampleProduct value a : ℝ) * movingSamplesPrior μ a : ℝ) : ℂ) *
             movingSupportedWeight value outside (buildMovingSlotData n t small bulk a) XL XR
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingSampledWeight, OAI.Ostmann.movingGuardedLeaf, OAI.Ostmann.movingGuardedExtra, OAI.Ostmann.movingLocalExtra, OAI.Ostmann.movingCompensatedExtra, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSampleProduct, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.movingSupportedWeight, OAI.Ostmann.buildMovingSlotData