OAI/NumberTheory/Ostmann/Arithmetic/MovingUnitSampleBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.RegularLengthLE line 11
2. theorem OAI.Ostmann.MovingSlotData.RegularLengthLE.mono line 17
3. theorem OAI.Ostmann.buildMovingSlotData_regular_length line 25
4. theorem OAI.Ostmann.MovingSlotData.RegularLengthLE.product_bound line 54
5. theorem OAI.Ostmann.MovingSlotData.RegularBound.mono line 65
6. theorem OAI.Ostmann.movingSample_unitPeriod_bound line 74

   Source documentation

   A concrete upper bound retaining the number of original small and bulk slots. Compensation contributes exactly four labels per bottom leaf per level.

   theorem movingSample_unitPeriod_bound {σ : Type*} (value : σ → ℕ)
       (P V : ℕ) (hP : 1 ≤ P) (hV : 1 ≤ V) (hvalue : ∀ i, value i ≤ P)
       (outside : List ℕ) (hout : 1 ≤ outside.prod)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (samples : MovingSampleSlots σ n) (A B : ℕ)
       (hsmall : MovingLeafLengthLE n small A) (hbulk : MovingLeafLengthLE n bulk B)
       (hfreq : (buildMovingSlotData n t small bulk samples).Frequencies (fun s => s.natAbs ≤ V)) :
       (movingGiantUnitPeriod value outside (buildMovingSlotData n t small bulk samples)).natAbs ≤
         (V * P ^ (2 ^ n * (A + B + 4 * n) + 4 * 2 ^ n) * outside.prod) ^ movingGiantUnitExponent n := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.MovingLeafLengthLE, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.movingGiantUnitPeriod, OAI.Ostmann.movingGiantUnitExponent