MRTSparseSplit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The extra-prime split in the no-small-band argument. Small values of the prime polynomial use a cofactor mean square; large values use a prime-supported mean square and a pointwise cofactor estimate.

theorem OAI.TwoPointCorrelations.mrt_sparse_product_split line 16

Source documentation

The finite split retains the restricted prime mean square on the large-prime-polynomial samples.

theorem mrt_sparse_product_split (S : Finset ℝ) (Q R : ℝ → ℂ)
    {θ U CR CQ : ℝ}
    (hR : (∑ t ∈ S, ‖R t‖^2) ≤ CR)
    (hQ : (∑ t ∈ S.filter (fun t => θ ≤ ‖Q t‖), ‖Q t‖^2) ≤ CQ)
    (hpoint : ∀ t ∈ S, θ ≤ ‖Q t‖ → ‖R t‖ ≤ U) :
    (∑ t ∈ S, ‖Q t*R t‖^2) ≤ θ^2*CR+U^2*CQ := by
…

theorem OAI.TwoPointCorrelations.mrt_set_product_split line 56

Source documentation

A bound for all separated samples yields the actual integral on the no-small set, without leaving the set when choosing sample points.

theorem mrt_set_product_split (Q R : ℝ → ℂ)
    (hQc : Continuous Q) (hRc : Continuous R)
    {E : Set ℝ} (hE : MeasurableSet E) {T θ U CR CQ : ℝ}
    (hT : 0 ≤ T) (hET : E ⊆ Set.Ioc (-T) T)
    (hR : ∀ S : Finset ℝ, (∀ t ∈ S, t ∈ E) →
      (∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) → (∑ t ∈ S, ‖R t‖^2) ≤ CR)
    (hQ : ∀ S : Finset ℝ, (∀ t ∈ S, t ∈ E ∧ θ ≤ ‖Q t‖) →
      (∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) → (∑ t ∈ S, ‖Q t‖^2) ≤ CQ)
    (hpoint : ∀ t ∈ E, θ ≤ ‖Q t‖ → ‖R t‖ ≤ U) :
    (∫ t in E, ‖Q t*R t‖^2) ≤ 4*(θ^2*CR+U^2*CQ) := by
…