WeightedFourierIntegration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-sum interchange and the two L¹ costs in the cutoff Fourier inversion step. The uniform estimate is used after summing in the integer variable, so no frequency supremum enters the short sum.

theorem OAI.TwoPointCorrelations.finite_two_integrals line 15

theorem OAI.TwoPointCorrelations.norm_two_weighted_integrals line 40

Source documentation

A bound uniform in both Fourier parameters incurs exactly the product of the two L¹ coefficient masses.

theorem norm_two_weighted_integrals (w₁ w₂ : ℝ → ℂ)
    (hw₁ : Integrable w₁) (hw₂ : Integrable w₂)
    (F : ℝ → ℝ → ℂ) (E : ℝ)
    (hF : ∀ t s, ‖F t s‖ ≤ E) :
    ‖∫ t, ∫ s, w₁ t * w₂ s * F t s‖ ≤
      E * (∫ t, ‖w₁ t‖) * (∫ s, ‖w₂ s‖) := by
…