OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.halaszUnitReciprocal line 15

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:15 (same declaration text).

2. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_nonneg line 18

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:18 (same declaration text).

3. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_one line 21

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:21 (same declaration text).

4. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_mul line 24

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:24 (same declaration text).

5. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prime_pow line 31

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:31 (same declaration text).

6. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_local_summable line 38

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:38 (same declaration text).

7. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_local_bound line 52

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:52 (same declaration text).

8. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prefix_le_prod line 93

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:93 (same declaration text).

9. lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prod_bound line 122

   Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:122 (same declaration text).

10. theorem OAI.TwoPointCorrelations.halasz_unit_correction_reciprocal line 146

    Source documentation

    Absolute reciprocal mass of the exact constant-one correction.

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:146 (same declaration text).

    theorem halasz_unit_correction_reciprocal (F : ℕ → ℂ) (hF : OneBounded F)
        (hF1 : F 1 = 1) (N : ℕ) :
        (∑ n ∈ Icc 1 N, ‖halaszUnitCorrection F n‖ / (n : ℝ)) ≤
          Real.exp (halaszPrimeDiscrepancy F 0 N + 8) :=
    …

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszUnitCorrection, OAI.TwoPointCorrelations.halaszPrimeDiscrepancy

11. lemma OAI.TwoPointCorrelations.halasz_twisted_prime_discrepancy line 153

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:153 (same declaration text).

12. theorem OAI.TwoPointCorrelations.halasz_twisted_unit_reciprocal line 158

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:158 (same declaration text).

13. theorem OAI.TwoPointCorrelations.halasz_near_correction_reciprocal line 168

    Source documentation

    Uniform reciprocal correction bound for every permitted near-twist missing-prime mask.

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitEuler.lean:168 (same declaration text).

    theorem halasz_near_correction_reciprocal :
        ∀ᶠ N : ℕ in Filter.atTop, ∀ (F : ℕ → ℂ), F 1 = 1 → OneBounded F →
          ∀ (Q : Finset ℕ), (∀ p ∈ Q, p.Prime) →
          (∀ p ∈ Q, (p : ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
          ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) N ≤
            Real.log (Real.log N) / 8 →
          (∑ n ∈ Icc 1 N,
            ‖halaszUnitCorrection (halaszTwistedFunction (mrtMissingCoefficient F Q) t) n‖ / (n : ℝ)) ≤
              Real.exp 8 * (Real.log N) ^ (7 / (8 : ℝ)) := by
    …

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszUnitCorrection, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtMissingCoefficient