HalaszNearDiscrepancy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Prime discrepancy for the near-minimizing twist in MRT Appendix A. The deleted-prime contribution is kept separate in Cauchy--Schwarz; this retains the strict exponent needed by the renormalization error.

def OAI.TwoPointCorrelations.halaszPrimeDiscrepancy line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_one_sub_norm_sq line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_prime_unit_bound line 25
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:25 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_masked_discrepancy_split line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_undeleted_discrepancy_sq line 51
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:51 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_near_discrepancy_numeric line 90
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:90 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_near_masked_discrepancy line 106
Source documentation
The 7/8 prime-discrepancy estimate used for near-twist renormalization. Only primes below the actual Appendix-A cutoff may be deleted.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean:106 (same declaration text).
```
theorem halasz_near_masked_discrepancy :
    ∀ᶠ N : ℕ in atTop, ∀ (F : ℕ → ℂ), 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 →
      halaszPrimeDiscrepancy (mrtMissingCoefficient F Q) t N ≤
        7 / 8 * Real.log (Real.log N) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszPrimeDiscrepancy, OAI.TwoPointCorrelations.mrtMissingCoefficient