OAI/NumberTheory/Ostmann/Arithmetic/MovingDiagonalNumericalRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.diagonalOuterMajorant_eventually line 13
2. theorem OAI.Ostmann.movingPattern_diagonal_pointwise_rate line 28

   Source documentation

   The actual denominator and coefficient mass absorb all comparison costs. The remaining main term K is the nonnegative leaf/split contribution.

   theorem movingPattern_diagonal_pointwise_rate (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
       (A Wwin B D Cprior Cmass : ℝ)
       (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) (_hB : 0 ≤ B) (_hD : 0 ≤ D)
       (hCprior : 1 ≤ Cprior) (hCmass : 0 ≤ Cmass) :
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

   Mentions: OAI.Ostmann.spectatorBulkCount