OAI/NumberTheory/Ostmann/Construction/DyadicHarmonicBias.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.harmonicQuadraticBias line 12
2. def OAI.Ostmann.iteratedLogPrimeBand line 15
3. def OAI.Ostmann.harmonicQuadraticBandMass line 19
4. theorem OAI.Ostmann.harmonicQuadraticBias_nonneg line 22
5. theorem OAI.Ostmann.harmonicQuadratic_closedBand_le line 25
6. theorem OAI.Ostmann.exists_dyadic_cover line 46

   Source documentation

   Closed dyadic intervals cover the specified finite logarithmic range.

   theorem exists_dyadic_cover (X u : ℝ) (n : ℕ) (hX : 0 < X) (hlo : X ≤ u)
       (hhi : u ≤ (2 : ℝ) ^ n * X) :
       ∃ j ≤ n, (2 : ℝ) ^ j * X ≤ u ∧ u ≤ 2 * ((2 : ℝ) ^ j * X) := by
   …

7. theorem OAI.Ostmann.harmonicQuadraticBandMass_dyadic_bound line 61