RoughShiftConvolution.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier convolution for the translated rough-shift average.

def OAI.TwoPointCorrelations.forwardWindowPolynomial line 13
def OAI.TwoPointCorrelations.backwardWindowPolynomial line 17

theorem OAI.TwoPointCorrelations.rough_shift_convolution line 23

Source documentation

Orthogonality imposes precisely a=m+hz; the long window contains every selected frequency, so there is no further truncation error.

theorem rough_shift_convolution (f g : ℕ → ℂ) (Z : Finset ℕ) (D h v : ℕ)
    (hZ : ∀ z ∈ Z, z ≤ 2 * D) :
    (∫ θ, roughFourierPolynomial Z h θ * forwardWindowPolynomial f D v θ *
      backwardWindowPolynomial g ((2 * h + 1) * D) v θ ∂AddCircle.haarAddCircle) =
      ∑ z ∈ Z, (z : ℂ)⁻¹ * ∑ m ∈ Icc 1 D, f (v + m) * g (v + m + h * z) := by
…

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

theorem OAI.TwoPointCorrelations.summed_rough_shift_convolution line 61

Source documentation

Summing the convolution identity gives the exact translated average used before the endpoint comparison.

theorem summed_rough_shift_convolution (f g : ℕ → ℂ) (Z : Finset ℕ)
    (D h Y : ℕ) (hZ : ∀ z ∈ Z, z ≤ 2 * D) :
    (∑ v ∈ range Y, ∫ θ,
      roughFourierPolynomial Z h θ * forwardWindowPolynomial f D (v + 1) θ *
      backwardWindowPolynomial g ((2 * h + 1) * D) (v + 1) θ
        ∂AddCircle.haarAddCircle) =
      ∑ m ∈ Icc 1 D, ∑ v ∈ range Y, ∑ z ∈ Z,
        (z : ℂ)⁻¹ * (f (v + 1 + m) * g (v + 1 + m + h * z)) := by
…

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