HalaszUnitEuler.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Absolute Euler control of the constant-one convolution correction. The first-order exponent is the actual prime discrepancy.

def OAI.TwoPointCorrelations.halaszUnitReciprocal line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_nonneg line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_one line 21
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:21 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_mul line 24
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prime_pow line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_local_summable line 38
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:38 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_local_bound line 52
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:52 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prefix_le_prod line 93
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:93 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_reciprocal_prod_bound line 122
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:122 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_unit_correction_reciprocal line 146
Source documentation
Absolute reciprocal mass of the exact constant-one correction.
Also declared: OAI/NumberTheory/TwoPointCorrelations/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
lemma OAI.TwoPointCorrelations.halasz_twisted_prime_discrepancy line 153
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:153 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_twisted_unit_reciprocal line 158
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitEuler.lean:158 (same declaration text).

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/TwoPointCorrelations/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