RoughShiftScale.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit power arithmetic in the rough-shift Fourier argument.

lemma OAI.TwoPointCorrelations.rough_reciprocal_mass_le_sup line 13
lemma OAI.TwoPointCorrelations.rough_window_sqrt_bound line 23
lemma OAI.TwoPointCorrelations.rough_fourier_exponent_identity line 34
lemma OAI.TwoPointCorrelations.rough_low_term_bound line 43
lemma OAI.TwoPointCorrelations.rough_high_term_identity line 57

theorem OAI.TwoPointCorrelations.rough_shift_power_bound line 75

Source documentation

The Fourier bound has the exact exponent -21/20. The stronger -31/20 contribution is absorbed only at this final numerical step.

theorem rough_shift_power_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) (L U V K : ℝ)
    (hL : 1 ≤ L) (hU : 0 ≤ U) (hV : 0 ≤ V) (hK : 0 ≤ K)
    (hendpoint : (D : ℝ) / Y ≤ L ^ (-21 / 20 : ℝ))
    (hB : ∀ θ, ‖roughFourierPolynomial Z h θ‖ ≤ U * L ^ (-99 / 100 : ℝ))
    (hfourth : (∫ θ, ‖roughFourierPolynomial Z h θ‖ ^ 4
      ∂AddCircle.haarAddCircle) ≤ V / D * L ^ (-99 / 25 : ℝ))
    (hF : ∀ θ, (∑ v ∈ range Y, ‖forwardWindowPolynomial f D (v + 1) θ‖) ≤
      K * Y * D * L ^ (-4 / 5 : ℝ)) :
    ‖roughShiftAverage f g Z h Y‖ ≤
      (2 * U + (2 * (h : ℝ) + 1) + (2 * (h : ℝ) + 1) * U * V * K) *
…

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