OAI/NumberTheory/Ostmann/Arithmetic/MovingPeriodScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSample_topPeriod_exp line 12
2. theorem OAI.Ostmann.movingSample_period_exponent_budget line 32

   Source documentation

   Fixed depth and all fixed constants are absorbed by the strict .010/.012 exponent gap in the source. The cutoff is uniform in the sampled primes.

   theorem movingSample_period_exponent_budget (n : ℕ) (C : ℝ) :
       ∀ᶠ L : ℝ in atTop,
         ((4 * (4 ^ n - 1) : ℕ) : ℝ) *
             (C * L + (4 * 2 ^ n : ℕ) * (C * Real.exp ((1 / 100 : ℝ) * L))) ≤
           Real.exp ((12 / 1000 : ℝ) * L) := by
   …

3. theorem OAI.Ostmann.movingSample_topPeriod_progression_range line 55

   Source documentation

   An actual integer modulus bound for the published giant progression input. Neither the tree, frequencies, primes nor top giants enter the eventual cutoff.

   theorem movingSample_topPeriod_progression_range {σ : Type*} (n : ℕ) (C : ℝ) :
       ∀ᶠ L : ℝ in atTop, ∀ (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
         (P V : ℕ), 1 ≤ P → 1 ≤ V → (∀ i, value i ≤ P) →
         (V : ℝ) ≤ Real.exp (C * L) → (P : ℝ) ≤ Real.exp (C * Real.exp ((1 / 100 : ℝ) * L)) →
         ∀ (childBound pivotBound : ℕ → ℕ) (t : FrequencyTree ℤ n)
           (small bulk : TreeLeafTuple (List σ) n) (samples : MovingSampleSlots σ n)
           (hf : (buildMovingSlotData n t small bulk samples).Frequencies (· ≠ 0)),
           (buildMovingSlotData n t small bulk samples).Frequencies (fun s => s.natAbs ≤ V) →
           movingTopPeriod value hvalue childBound pivotBound
             (buildMovingSlotData n t small bulk samples) hf ≤
             ⌊Real.exp (Real.exp ((12 / 1000 : ℝ) * L))⌋₊ := by
   …

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