OAI/NumberTheory/Ostmann/ZeroDensity/ReciprocalProgressionVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.discreteVariation_nonneg line 11
2. theorem OAI.Ostmann.discreteVariation_congr line 14
3. theorem OAI.Ostmann.discreteVariation_ofReal_antitone line 24
4. theorem OAI.Ostmann.reciprocal_progression_antitone line 36
5. theorem OAI.Ostmann.reciprocal_progression_variation line 45
6. theorem OAI.Ostmann.reciprocal_progression_norm line 50
7. theorem OAI.Ostmann.reciprocal_progression_product_variation line 57

   Source documentation

   Multiplying by 1/n costs only twice the endpoint bound divided by the left endpoint, with no dependence on the progression length.

   theorem reciprocal_progression_product_variation (b d : ℝ) (hb : 0 < b) (hd : 0 ≤ d)
       (f : ℕ → ℂ) (N : ℕ) (B V : ℝ) (hBV : B ≤ V)
       (hf : ∀ j, ‖f j‖ ≤ B) (hv : discreteVariation f N ≤ V) :
       discreteVariation (fun j => Complex.ofReal ((b + d * (j : ℝ))⁻¹) * f j) N ≤ 2 * b⁻¹ * V := by
   …

   Mentions: OAI.Ostmann.discreteVariation

8. theorem OAI.Ostmann.discreteVariation_const_mul line 69