MovingSamplePeriod.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The residue period for actual four-slot samples

theorem OAI.Ostmann.movingNaturalProduct_le_pow line 11
theorem OAI.Ostmann.MovingSlotData.CompensationBound.mono line 20

theorem OAI.Ostmann.buildMovingSlotData_compensation_bound line 30

Source documentation

Only the four compensation samples at each leaf enter the denominator. The lengths of the bulk and initial small-prime lists do not enter this bound.

theorem buildMovingSlotData_compensation_bound {σ : Type*} (value : σ → ℕ)
    (P : ℕ) (hP : 1 ≤ P) (hvalue : ∀ i, value i ≤ P)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n) :
    (buildMovingSlotData n t small bulk samples).CompensationBound value (P ^ (4 * 2 ^ n)) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.buildMovingSlotData

theorem OAI.Ostmann.movingSample_topPeriod_bound line 49

Source documentation

The concrete common modulus is controlled by the frequency cutoff and compensation-prime cutoff alone, uniformly in both top giants.

theorem movingSample_topPeriod_bound {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (P V : ℕ) (hP : 1 ≤ P) (hV : 1 ≤ V)
    (hvalueP : ∀ i, value i ≤ P) (childBound pivotBound : ℕ → ℕ)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n)
    (hf : (buildMovingSlotData n t small bulk samples).Frequencies (· ≠ 0))
    (hfreq : (buildMovingSlotData n t small bulk samples).Frequencies (fun s => s.natAbs ≤ V)) :
    movingTopPeriod value hvalue childBound pivotBound
      (buildMovingSlotData n t small bulk samples) hf ≤
        (V * P ^ (4 * 2 ^ n)) ^ (4 * (4 ^ n - 1)) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.movingTopPeriod