OAI/NumberTheory/Ostmann/Construction/RoundedScheduleRanges.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventually_rounded_schedule_ranges line 14

   Source documentation

   The interval step's two integer inequalities follow from the original logarithmic product ranges with one uniform large-parameter threshold.

   theorem eventually_rounded_schedule_ranges (C : ℝ) :
       ∀ᶠ m : ℝ in atTop, ∀ Δ : ℝ, 0 ≤ Δ → ∀ j : ℕ, ∀ T : ℝ,
         ∀ M B L K : ℕ,
         Real.exp (T - C) ≤ M → B ≤ naturalProductCap (T + C) →
         Real.exp (T + transferNextGap Δ m j - C) ≤ L →
         K ≤ naturalProductCap (T + transferNextGap Δ m j + C) →
         2 * B * naturalTransferCutoff Δ m j < L ∧
         2 * naturalTransferCutoff Δ m j * K ≤ naturalTransferCutoff Δ m (j + 1) * M := by
   …

   Mentions: OAI.Ostmann.naturalProductCap, OAI.Ostmann.transferNextGap, OAI.Ostmann.naturalTransferCutoff