OAI/NumberTheory/Ostmann/ZeroDensity/ComplexPrimeWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.complexPrimeInterval line 12
2. theorem OAI.Ostmann.complexPrimeInterval_add line 16
3. theorem OAI.Ostmann.complexPrimeInterval_freeze line 23
4. theorem OAI.Ostmann.complex_density_integral_freeze line 53

   Source documentation

   Freezing a continuous complex weight costs its oscillation times the length of the log interval. In particular the cost is additive over meshes.

   theorem complex_density_integral_freeze (φ χ β s t : ℝ) (hφ : 1 ≤ φ)
       (hχ : |χ| ≤ 1) (hβ : β ≤ 1) (hs : 1 ≤ s) (hst : s ≤ t)
       (w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc s t)) (c : ℂ) (η : ℝ) (hη : 0 ≤ η)
       (hw : ∀ y ∈ Set.Ioc s t, ‖w y - c‖ ≤ η) :
       ‖(∫ y in Set.Ioc s t, w y * (primeLogDensity φ χ β y : ℂ)) -
         c * (∫ y in Set.Ioc s t, primeLogDensity φ χ β y : ℝ)‖ ≤ 2 * η * (t - s) := by
   …

   Mentions: OAI.Ostmann.primeLogDensity