WeightedShiftAverage.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The finite correlation inequality for the arbitrary coefficients in the qualitative rough multiplier.

def OAI.TwoPointCorrelations.weightedRoughShiftProfile line 14
def OAI.TwoPointCorrelations.weightedRoughShiftAverage line 17
lemma OAI.TwoPointCorrelations.norm_weightedRoughShiftProfile_le line 20
lemma OAI.TwoPointCorrelations.translated_weightedRoughShiftProfile_eq line 27

theorem OAI.TwoPointCorrelations.weighted_rough_convolution_sum_bound line 46

Source documentation

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

theorem weighted_rough_convolution_sum_bound (f g : ℕ → ℂ) (hf : OneBounded f)
    (hg : OneBounded g) (Z : Finset ℕ) (c : ℕ → ℂ) (D h Y : ℕ)
    (ε U V K : ℝ) (hε : 0 < ε) (hU : 0 ≤ U) (hK : 0 ≤ K)
    (hB : ∀ θ, ‖weightedRoughFourier Z c h θ‖ ≤ U)
    (hV : (∫ θ, ‖weightedRoughFourier Z c h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V)
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤ K) :
    ‖∑ v ∈ range Y, ∫ θ,
      weightedRoughFourier Z c 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.weightedRoughFourier, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.backwardWindowPolynomial

lemma OAI.TwoPointCorrelations.normalized_translated_weightedRoughShift_bound line 76

theorem OAI.TwoPointCorrelations.weighted_rough_shift_average_bound line 96

Source documentation

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

theorem weighted_rough_shift_average_bound (f g : ℕ → ℂ) (hf : OneBounded f)
    (hg : OneBounded g) (Z : Finset ℕ) (c : ℕ → ℂ) (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 : ∀ θ, ‖weightedRoughFourier Z c h θ‖ ≤ U)
    (hV : (∫ θ, ‖weightedRoughFourier Z c h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V)
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤ K) :
    ‖weightedRoughShiftAverage f g Z c h Y‖ ≤
      2 * (D : ℝ) / Y * (∑ z ∈ Z, ‖c 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.weightedRoughFourier, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.weightedRoughShiftAverage