OAI/NumberTheory/CubicMoment/Estimates/IntervalTransform.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The interval Fourier multiplier

Evaluation of the interval transform gives the two endpoint terms divided by frequency. The value at zero is the interval length, so there is no singularity in the original multiplier.

  1. theorem OAI.CubicFirstMoment.fourier_intervalStep_eq_integral line 19
  2. theorem OAI.CubicFirstMoment.fourier_intervalStep_zero line 33
  3. theorem OAI.CubicFirstMoment.fourier_intervalStep_nonzero line 38
  4. theorem OAI.CubicFirstMoment.dyadic_interval_multiplier line 57

    Source documentation

    The multiplier for the dyadic interval [1,2], at every nonzero frequency.

    theorem dyadic_interval_multiplier {ξ : ℝ} (hξ : ξ ≠ 0) :
    𝓕 (fun x => (intervalStep 0 (Real.log 2) x : ℂ)) ξ =
      (1 - Complex.exp ((-2 * Real.pi * Real.log 2 * ξ : ℝ) * Complex.I)) /
        ((2 * Real.pi * ξ : ℝ) * Complex.I) := by
…

    Mentions: OAI.CubicFirstMoment.intervalStep