OAI/NumberTheory/TwoPointCorrelations/HalaszNearDiscrepancy.lean

GitHub source file

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.

  1. def OAI.TwoPointCorrelations.halaszPrimeDiscrepancy line 15

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

  2. lemma OAI.TwoPointCorrelations.halasz_one_sub_norm_sq line 18

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

  3. lemma OAI.TwoPointCorrelations.halasz_prime_unit_bound line 25

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszNearDiscrepancy.lean:25 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_masked_discrepancy_split line 31

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

  5. lemma OAI.TwoPointCorrelations.halasz_undeleted_discrepancy_sq line 51

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszNearDiscrepancy.lean:51 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_near_discrepancy_numeric line 90

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszNearDiscrepancy.lean:90 (same declaration text).

  7. 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/TwoPoint/Halasz/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