WeightedShiftParameters.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The three quantitative terms in the qualitative weighted shift argument, separated from their eventual scale estimates.

lemma OAI.TwoPointCorrelations.rough_coefficient_mass_le_one line 14
lemma OAI.TwoPointCorrelations.weighted_shift_high_identity line 30

theorem OAI.TwoPointCorrelations.weighted_rough_shift_parameter_bound line 41

Source documentation

The high-frequency cost is controlled by q^6 ≤ η^5; all actual correlation, boundary and short-window terms remain explicit.

theorem weighted_rough_shift_parameter_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)
    (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)
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤
      K * Y * D * q) :
…

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