MRTCoarseMean.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The literal coarse-bin polynomial differs from the supported dyadic polynomial by the prime-square correction and the two short boundary strips. Both errors are estimated before any sum over prime bins.

def OAI.TwoPointCorrelations.mrtWeightedRamareCoefficient line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:15 (same declaration text).
def OAI.TwoPointCorrelations.mrtCoarsePolynomial line 18
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:18 (same declaration text).
def OAI.TwoPointCorrelations.mrtCoarseBoundaryPolynomial line 24
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_dyadic_polynomial_extend line 30
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:30 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_coarse_boundary_identity line 54
Source documentation
Exact boundary identity, with the original and coarse polynomials both retaining their actual numerical coefficients.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:54 (same declaration text).
```
theorem mrt_coarse_boundary_identity (P : Finset ℕ) (L : ℕ → ℝ)
    {N : ℕ} (hN : 0 < N) {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
    (hL : ∀ p ∈ P, L p ≤ p ∧ (p : ℝ) ≤ δ * L p)
    (F : ℕ → ℂ) (t : ℝ) :
    mrtDyadicPolynomial (mrtWeightedRamareCoefficient P F) N t -
        mrtCoarsePolynomial P L N F t =
      mrtCoarseBoundaryPolynomial P L N δ F t := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtWeightedRamareCoefficient, OAI.TwoPointCorrelations.mrtCoarsePolynomial, OAI.TwoPointCorrelations.mrtCoarseBoundaryPolynomial
lemma OAI.TwoPointCorrelations.mrt_coarse_boundary_coefficient_norm line 87
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:87 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_coarse_boundary_mean line 95
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:95 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_weighted_ramare_sum line 107
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:107 (same declaration text).
def OAI.TwoPointCorrelations.mrtSupportedCoefficient line 122
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:122 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_supported_ramare_split line 125
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:125 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_dyadic_polynomial_add line 132
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:132 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_coarse_error_identity line 138
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:138 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_coarse_error_mean_square line 155

Source documentation

Coarse-bin decoupling costs the reciprocal square mass and the bin width. There is no loss depending on the number of bins.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseMean.lean:155 (same declaration text).

theorem mrt_coarse_error_mean_square (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)
    (F : ℕ → ℂ) (hF : OneBounded F) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T, ‖mrtDyadicPolynomial (mrtSupportedCoefficient P F) N t -
      mrtCoarsePolynomial P L N F t‖ ^ 2) ≤
      192 * Real.exp 1 * (T / (N : ℝ) + 1) *
        ((∑ p ∈ P, 1 / (p : ℝ) ^ 2) +
          (∑ p ∈ P, 1 / (p : ℝ) ^ 2) ^ 2 + (δ - 1)) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtSupportedCoefficient, OAI.TwoPointCorrelations.mrtCoarsePolynomial