OAI/NumberTheory/CubicMoment/Estimates/FarHeightIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The far-cell height identity and its uniformly integrable Fourier kernel. These are identities for the actual height integral, with no arithmetic input.

  1. lemma OAI.CubicFirstMoment.far_height_identity line 14
  2. lemma OAI.CubicFirstMoment.far_dilated_integrable line 33
  3. lemma OAI.CubicFirstMoment.far_dilated_fourier_integrable line 38
  4. lemma OAI.CubicFirstMoment.far_fourier_representation line 57

    Source documentation

    Fourier inversion separates the far-cell product weight, with its frequency shifts independent of the height variable.

    lemma far_fourier_representation {J : ℝ} (hJ : 0 < J) (x : ℝ) :
    farInverseSquare (J*x) =
      ∫ u : ℝ, Complex.exp ((2*Real.pi*u*x:ℝ)*Complex.I) *
        𝓕 (fun y => farInverseSquare (J*y)) u := by
…

    Mentions: OAI.CubicFirstMoment.farInverseSquare