WeightedShiftConvolution.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact convolution with arbitrary complex coefficients on the rough support. The coefficient choice is kept outside the short-sum supremum.

theorem OAI.TwoPointCorrelations.weighted_rough_shift_convolution line 16

Source documentation

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

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

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

theorem OAI.TwoPointCorrelations.summed_weighted_rough_shift_convolution line 54

Source documentation

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

theorem summed_weighted_rough_shift_convolution (f g : ℕ → ℂ) (Z : Finset ℕ) (c : ℕ → ℂ)
    (D h Y : ℕ) (hZ : ∀ z ∈ Z, z ≤ 2 * D) :
    (∑ v ∈ range Y, ∫ θ,
      weightedRoughFourier Z c 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,
        (c z / (z : ℂ)) * (f (v + 1 + m) * g (v + 1 + m + h * z)) := by
…

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