OAI/NumberTheory/Ostmann/Arithmetic/MovingAdaptiveSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSampledPivotHistory line 12
2. theorem OAI.Ostmann.movingSampledPivotHistory_valid line 25
3. theorem OAI.Ostmann.movingFrameConstants_compensation_coprime line 47
4. theorem OAI.Ostmann.movingSample_adaptive_support line 65

   Source documentation

   The prefix tests are built from actual samples and are passed by every nonzero original history. There is no assumed adaptive-support event.

   theorem movingSample_adaptive_support {σ : Type*} (value : σ → ℕ)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (S : Finset ℤ) (n R : ℕ) [NeZero (R ^ (n + 2))] (t : FrequencyTree S n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ∣ R)
       (small bulk : TreeLeafTuple (List σ) n) (a : MovingSampleSlots σ n) (XL XR : ℕ)
       (hsmall : ∀ i, IsCoprime (value i : ℤ) (R : ℤ))
       (y : TreeLeafTuple (ZMod (R ^ (n + 2)))ˣ n)
       (hy : treeIntegerResidues (R ^ (n + 2)) n
         (treeLeafMap (fun q : ℕ => (q : ℤ)) n (movingSlotValues value n bulk)) y)
       (hw : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound (movingGuardedExtra value outside E)) n
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.treeIntegerResidues, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingSlotValues, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingGuardedExtra