CorrelationWeightVariation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform variation of the two transform factors in a correlation

theorem OAI.Ostmann.discreteVariation_conj line 11
theorem OAI.Ostmann.discreteVariation_mul_le line 15

theorem OAI.Ostmann.schwartz_correlation_variation line 46

Source documentation

The two smooth Fourier-transform weights have uniform variation on any interval whose length is bounded by both scaling lengths.

theorem schwartz_correlation_variation (Φ Ψ : 𝓢(ℝ, ℂ))
    (ξ η Y Z C D : ℝ) (N : ℕ) (hY : 0 < Y) (hZ : 0 < Z)
    (hNY : (N : ℝ) ≤ C * Y) (hNZ : (N : ℝ) ≤ D * Z) :
    discreteVariation (fun n => Φ (((n : ℝ) + ξ) / Y) *
      conj (Ψ (((n : ℝ) + η) / Z))) N ≤
      SchwartzMap.seminorm ℝ 0 0 Φ *
        (SchwartzMap.seminorm ℝ 0 0 Ψ + SchwartzMap.seminorm ℝ 0 1 Ψ * D) +
      SchwartzMap.seminorm ℝ 0 0 Ψ *
        (SchwartzMap.seminorm ℝ 0 0 Φ + SchwartzMap.seminorm ℝ 0 1 Φ * C) := by
…

Mentions: OAI.Ostmann.discreteVariation