OAI/NumberTheory/TwoPointCorrelations/MRTCoarseFactorization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.mrtDirichletAtom line 13

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:13 (same declaration text).

2. def OAI.TwoPointCorrelations.mrtCofactorPolynomial line 16

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:16 (same declaration text).

3. lemma OAI.TwoPointCorrelations.mrt_dirichlet_atom_mul_of_product line 23

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:23 (same declaration text).

4. lemma OAI.TwoPointCorrelations.mrt_dirichlet_atom_mul line 39

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:39 (same declaration text).

5. lemma OAI.TwoPointCorrelations.mrt_coarse_polynomial_prime_sum line 46

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:46 (same declaration text).

6. lemma OAI.TwoPointCorrelations.mrt_coarse_polynomial_cofactor_sum line 74

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:74 (same declaration text).

7. theorem OAI.TwoPointCorrelations.mrt_coarse_polynomial_factorization_of_product line 101

   Source documentation

   Each prime has the same cofactor cutoff as the lower endpoint of its bin. The extension of its finite range introduces only zero terms.

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:101 (same declaration text).

   theorem mrt_coarse_polynomial_factorization_of_product (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (L : ℕ → ℝ) (N : ℕ)
       {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
       (hL : ∀ p ∈ P, L p ≤ p ∧ (p : ℝ) ≤ δ * L p)
       (F A B : ℕ → ℂ)
       (hF : ∀ p ∈ P, ∀ m, 0 < m → F (p * m) = A p * B m) (t : ℝ) :
       mrtCoarsePolynomial P L N F t =
         ∑ p ∈ P, mrtDirichletAtom A p t * mrtCofactorPolynomial P B N (L p) t := by
   …

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

8. theorem OAI.TwoPointCorrelations.mrt_coarse_polynomial_factorization line 148

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:148 (same declaration text).

9. theorem OAI.TwoPointCorrelations.mrt_coarse_polynomial_bins_of_product line 161

   Source documentation

   Grouping by a finite bin index produces exactly one short prime polynomial times one fixed-window cofactor polynomial per bin.

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:161 (same declaration text).

   theorem mrt_coarse_polynomial_bins_of_product {ι : Type*} [DecidableEq ι]
       (J : Finset ι) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (bin : ℕ → ι) (hbin : ∀ p ∈ P, bin p ∈ J)
       (lower : ι → ℝ) (N : ℕ) {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
       (hL : ∀ p ∈ P, lower (bin p) ≤ p ∧ (p : ℝ) ≤ δ * lower (bin p))
       (F A B : ℕ → ℂ)
       (hF : ∀ p ∈ P, ∀ m, 0 < m → F (p * m) = A p * B m) (t : ℝ) :
       mrtCoarsePolynomial P (fun p => lower (bin p)) N F t =
         ∑ j ∈ J,
           mrtExponentialPolynomial (P.filter (fun p => bin p = j))
             (fun p => A p / (p : ℂ)) (fun p => -Real.log (p : ℝ)) t *
           mrtCofactorPolynomial P B N (lower j) t := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtCoarsePolynomial, OAI.TwoPointCorrelations.mrtExponentialPolynomial, OAI.TwoPointCorrelations.mrtCofactorPolynomial

10. theorem OAI.TwoPointCorrelations.mrt_coarse_polynomial_bins line 184

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseFactorization.lean:184 (same declaration text).