OAI/NumberTheory/Ostmann/Arithmetic/MovingSpectatorScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSpectator_exponent_budget line 10
2. theorem OAI.Ostmann.movingSpectator_progression_range line 39

   Source documentation

   The cutoff is uniform in the actual tree and the spectator prime set. The period includes both integer division denominators and all spectators.

   theorem movingSpectator_progression_range {σ : Type*} (n : ℕ) (C : ℝ) :
       ∀ᶠ L : ℝ in atTop, ∀ (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
         (childBound pivotBound : ℕ → ℕ) (T : MovingSlotData σ n)
         (hf : T.Frequencies (· ≠ 0)) (B : ℕ), 1 ≤ B →
         T.Frequencies (fun s => s.natAbs ≤ B) → T.CompensationBound value B →
         (B : ℝ) ≤ Real.exp (C * L + C * Real.exp ((1 / 100 : ℝ) * L)) →
         ∀ (S : Finset ℕ) (R : ℕ), (∀ q ∈ S, 0 < q ∧ q ≤ R) →
         (R : ℝ) ≤ Real.exp ((1 / 1000 : ℝ) * L) →
         movingSpectatorModulus value hvalue childBound pivotBound T hf id S ≤
           ⌊Real.exp (Real.exp ((12 / 1000 : ℝ) * L))⌋₊ := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSpectatorModulus