OAI/NumberTheory/Ostmann/Construction/TransferRoundedCutoffs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.naturalTransferCutoff line 14
2. def OAI.Ostmann.naturalProductCap line 17
3. theorem OAI.Ostmann.natural_exp_cutoff_bounds line 19
4. theorem OAI.Ostmann.eventually_transfer_integer_ranges line 32

   Source documentation

   The same explicit rounded cutoffs supply the strict determinant gap and the next signed-frequency bound, at every transfer level.

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

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