MRTGeneralFactorization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact coarse prime extraction with its prime-square discrepancy. Only coprime multiplicativity is needed when the discrepancy is bounded.

lemma OAI.TwoPointCorrelations.mrt_prime_cofactor_expansion line 13
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralFactorization.lean:13 (same declaration text).
def OAI.TwoPointCorrelations.mrtPrimeExtractionError line 72
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralFactorization.lean:72 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_extraction_error_zero line 78
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralFactorization.lean:78 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_general_prime_factorization line 94
Source documentation
The exact polynomial identity precedes all norm estimates and keeps one discrepancy coefficient per integer, rather than per prime bin.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralFactorization.lean:94 (same declaration text).
```
theorem mrt_general_prime_factorization (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (L : ℕ → ℝ) (N : ℕ)
    {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ P, L p ≤ p ∧ (p : ℝ) ≤ δ * L p)
    (C A B : ℕ → ℂ) (t : ℝ) :
    mrtCoarsePolynomial P L N C t -
      (∑ p ∈ P, mrtDirichletAtom A p t * mrtCofactorPolynomial P B N (L p) t) =
      mrtExponentialPolynomial (Ioc N (4 * N))
        (fun n => mrtPrimeExtractionError P L N C A B n / (n : ℂ))
        (fun n => -Real.log (n : ℝ)) t := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtCoarsePolynomial, OAI.TwoPointCorrelations.mrtDirichletAtom, OAI.TwoPointCorrelations.mrtCofactorPolynomial, OAI.TwoPointCorrelations.mrtExponentialPolynomial, OAI.TwoPointCorrelations.mrtPrimeExtractionError

theorem OAI.TwoPointCorrelations.mrt_general_prime_factorization_mean line 151

Source documentation

The coarse prime-product factorization is valid for general multiplicative coefficients up to the already controlled square error.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralFactorization.lean:151 (same declaration text).

theorem mrt_general_prime_factorization_mean (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (L : ℕ → ℝ) {N : ℕ} (hN : 0 < N)
    {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ P, L p ≤ p ∧ (p : ℝ) ≤ δ * L p)
    (C A B : ℕ → ℂ) (hC : OneBounded C) (hA : OneBounded A) (hB : OneBounded B)
    (hproduct : ∀ p ∈ P, ∀ m, 0 < m → ¬p ∣ m → C (p * m) = A p * B m)
    {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtCoarsePolynomial P L N C t -
      (∑ p ∈ P, mrtDirichletAtom A p t * mrtCofactorPolynomial P B N (L p) t)‖ ^ 2) ≤
      512 * Real.exp 1 * (T / (N : ℝ) + 1) *
        ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) + (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtCoarsePolynomial, OAI.TwoPointCorrelations.mrtDirichletAtom, OAI.TwoPointCorrelations.mrtCofactorPolynomial