RoughShiftAverage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A finite rough-shift correlation inequality

The three terms are the explicit translation error, the low-frequency Cauchy--Schwarz term, and the high-frequency fourth-moment term. Sieve estimates and MRT scale estimates enter only through their numerical bounds.

def OAI.TwoPointCorrelations.roughShiftProfile line 19
def OAI.TwoPointCorrelations.roughShiftAverage line 22
lemma OAI.TwoPointCorrelations.norm_roughShiftProfile_le line 25
lemma OAI.TwoPointCorrelations.translated_roughShiftProfile_eq line 33
lemma OAI.TwoPointCorrelations.rough_window_energy_sum_bound line 51

theorem OAI.TwoPointCorrelations.rough_convolution_sum_bound line 69

Source documentation

All Fourier ingredients are now attached to the concrete two windows.

theorem rough_convolution_sum_bound (f g : ℕ → ℂ) (hf : OneBounded f)
    (hg : OneBounded g) (Z : Finset ℕ) (D h Y : ℕ)
    (ε U V K : ℝ) (hε : 0 < ε) (hU : 0 ≤ U) (hK : 0 ≤ K)
    (hB : ∀ θ, ‖roughFourierPolynomial Z h θ‖ ≤ U)
    (hV : (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V)
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤ K) :
    ‖∑ v ∈ range Y, ∫ θ,
      roughFourierPolynomial Z h θ * forwardWindowPolynomial f D (v + 1) θ *
        backwardWindowPolynomial g ((2 * h + 1) * D) (v + 1) θ
          ∂AddCircle.haarAddCircle‖ ≤
      ε * ((Y : ℝ) * (Real.sqrt D * Real.sqrt ((2 * h + 1) * D))) +
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.roughFourierPolynomial, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.backwardWindowPolynomial

lemma OAI.TwoPointCorrelations.normalized_translated_roughShift_bound line 99

theorem OAI.TwoPointCorrelations.rough_shift_average_bound line 119

Source documentation

The finite correlation bound before inserting the sieve estimates and the size estimates for the published MRT error.

theorem rough_shift_average_bound (f g : ℕ → ℂ) (hf : OneBounded f)
    (hg : OneBounded g) (Z : Finset ℕ) (D h Y : ℕ) (hD : 0 < D) (hY : 0 < Y)
    (hZ : ∀ z ∈ Z, z ≤ 2 * D)
    (ε U V K : ℝ) (hε : 0 < ε) (hU : 0 ≤ U) (hK : 0 ≤ K)
    (hB : ∀ θ, ‖roughFourierPolynomial Z h θ‖ ≤ U)
    (hV : (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V)
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤ K) :
    ‖roughShiftAverage f g Z h Y‖ ≤
      2 * (D : ℝ) / Y * (∑ z ∈ Z, (z : ℝ)⁻¹) +
      (ε * ((Y : ℝ) * (Real.sqrt D * Real.sqrt ((2 * h + 1) * D))) +
        (U * ((2 * h + 1) * D) * K / ε ^ 4) * V) / ((Y : ℝ) * D) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.roughFourierPolynomial, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.roughShiftAverage