OAI/NumberTheory/Ostmann/Arithmetic/MovingPairAdaptiveSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPairAdaptiveData line 11
2. theorem OAI.Ostmann.movingPairAdaptiveData_frequencies line 28
3. theorem OAI.Ostmann.movingPairAdaptiveData_actual_support line 54

   Source documentation

   Each nonzero original weight forces its own tests; both use precisely the same bulk tuple. Their paired support is consequently one.

   theorem movingPairAdaptiveData_actual_support {σ : Type*} (value : σ → ℕ)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : Bool → MovingSlotState σ → ℤ → ℂ)
       (E : Bool → MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (S : Finset ℤ) (n R : ℕ) [NeZero (R ^ (n + 2))] (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0) (hR : ∀ s ∈ S, s.natAbs ∣ R)
       (small : Bool → TreeLeafTuple (List σ) n) (bulk : TreeLeafTuple (List σ) n)
       (a : Bool → 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)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.treeIntegerResidues, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingSlotValues