MRTTypicalCoarse.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coarse Ramaré factorization on the actual typical-factorization set. Removing a prime from the selected band leaves precisely the other-band mask; the square and endpoint errors retain their uniform finite bounds.

def OAI.TwoPointCorrelations.mrtTypicalCoefficient line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_oneBounded line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_supported line 28
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:28 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_prime_mul line 35
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:35 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_typical_coarse_bins line 51

Source documentation

The factorization on a fixed typical band produces the literal short prime polynomial and the other-band cofactor polynomial.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:51 (same declaration text).

theorem mrt_typical_coarse_bins {ι κ : Type*} [DecidableEq κ]
    (J : Finset ι) (P : ι → Finset ℕ)
    (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (hdis : Set.PairwiseDisjoint (J : Set ι) P) {j : ι} (hj : j ∈ J)
    (K : Finset κ) (bin : ℕ → κ) (hbin : ∀ p ∈ P j, bin p ∈ K)
    (lower : κ → ℝ) (N : ℕ) {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ P j, lower (bin p) ≤ p ∧ (p : ℝ) ≤ δ * lower (bin p))
    (F : ℕ → ℂ)
    (hF : ∀ a b, 0 < a → 0 < b → F (a * b) = F a * F b) (t : ℝ) :
    mrtCoarsePolynomial (P j) (fun p => lower (bin p)) N
      (mrtTypicalCoefficient J P F) t =
      ∑ k ∈ K,
…

Mentions: OAI.TwoPointCorrelations.mrtCoarsePolynomial, OAI.TwoPointCorrelations.mrtTypicalCoefficient

theorem OAI.TwoPointCorrelations.mrt_typical_coarse_mean_square line 74

Source documentation

The binned factorization approximates the actual typical polynomial in mean square, with no bin-count loss in the error.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalCoarse.lean:74 (same declaration text).

theorem mrt_typical_coarse_mean_square {ι κ : Type*} [DecidableEq κ]
    (J : Finset ι) (P : ι → Finset ℕ)
    (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (hdis : Set.PairwiseDisjoint (J : Set ι) P) {j : ι} (hj : j ∈ J)
    (K : Finset κ) (bin : ℕ → κ) (hbin : ∀ p ∈ P j, bin p ∈ K)
    (lower : κ → ℝ) {N : ℕ} (hN : 0 < N) {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ P j, lower (bin p) ≤ p ∧ (p : ℝ) ≤ δ * lower (bin p))
    (F : ℕ → ℂ)
    (hF : ∀ a b, 0 < a → 0 < b → F (a * b) = F a * F b)
    (hFb : OneBounded F) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial (mrtTypicalCoefficient J P F) N t -
      ∑ k ∈ K,
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtTypicalCoefficient