OAI/NumberTheory/CubicMoment/Estimates/FourierTwoDerivatives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Two integrable derivatives give the Fourier L1 bound needed for the fixed inverse-square extension in the far-cell argument.

  1. lemma OAI.CubicFirstMoment.norm_fourier_le_l1 line 14
  2. lemma OAI.CubicFirstMoment.fourier_second_deriv line 20
  3. lemma OAI.CubicFirstMoment.fourier_two_derivative_bound line 28
  4. theorem OAI.CubicFirstMoment.integrable_fourier_of_two_derivatives line 47
  5. theorem OAI.CubicFirstMoment.fourier_dilation_l1 line 61

    Source documentation

    Dilation costs no Fourier L1 mass, including the exact Jacobian.

    theorem fourier_dilation_l1 (f : ℝ → ℂ) {J : ℝ} (hJ : 0 < J) :
    (∫ t : ℝ, ‖𝓕 (fun x => f (J*x)) t‖) = ∫ t : ℝ, ‖𝓕 f t‖ := by
…