WeightedShiftRight.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The same finite Fourier argument when the nonpretentious function is in the second factor. No supremum is moved inside a sum over origins.

lemma OAI.TwoPointCorrelations.backwardWindowPolynomial_eq_forward_neg line 13
theorem OAI.TwoPointCorrelations.weighted_rough_convolution_sum_bound_right line 19

theorem OAI.TwoPointCorrelations.weighted_rough_shift_average_bound_right line 68

Source documentation

The second-factor version of the complete finite three-term bound.

theorem weighted_rough_shift_average_bound_right (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)
    (hG : ∀ θ, (∑ v ∈ range Y,
      ‖backwardWindowPolynomial g ((2 * h + 1) * 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))) +
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.weightedRoughFourier, OAI.TwoPointCorrelations.backwardWindowPolynomial, OAI.TwoPointCorrelations.weightedRoughShiftAverage

theorem OAI.TwoPointCorrelations.weighted_rough_shift_parameter_bound_right line 98

Source documentation

The sixth-power condition has the same exponent for either factor.

theorem weighted_rough_shift_parameter_bound_right (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)
    (q η U V K : ℝ) (hq : 0 ≤ q) (hη : 0 < η)
    (hU : 0 ≤ U) (hV : 0 ≤ V) (hK : 0 ≤ K)
    (hmass : (∑ z ∈ Z, ‖c z / (z : ℂ)‖) ≤ 1)
    (hendpoint : (D : ℝ) / Y ≤ η) (hgap : q ^ 6 ≤ η ^ 5)
    (hB : ∀ θ, ‖weightedRoughFourier Z c h θ‖ ≤ U * q)
    (hfourth : (∫ θ, ‖weightedRoughFourier Z c h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V / D * q ^ 4)
    (hG : ∀ θ, (∑ v ∈ range Y,
      ‖backwardWindowPolynomial g ((2 * h + 1) * D) (v + 1) θ‖) ≤
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.weightedRoughFourier, OAI.TwoPointCorrelations.backwardWindowPolynomial