OAI/NumberTheory/CubicMoment/Estimates/RieszIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The trace Fourier Riesz identity at the two exponents needed for cubing.

  1. theorem OAI.CubicFirstMoment.riesz_trace_identity line 13

    Source documentation

    The Riesz identity before dividing by Gamma(2/3).

    theorem riesz_trace_identity (F : š“¢(ā„‚,ā„‚)) :
    (Real.Gamma (2/3:ā„):ā„‚)*
      (āˆ« z : ā„‚, ((ā€–zā€–^(-(4/3:ā„)):ā„):ā„‚)*traceFourier F z) =
      ((Real.pi*(4*Real.pi^2)^(-(1/3:ā„))*Real.Gamma (1/3:ā„):ā„):ā„‚)*
        (āˆ« z : ā„‚, ((ā€–zā€–^(-(2/3:ā„)):ā„):ā„‚)*F z) := by
ā€¦

    Mentions: OAI.CubicFirstMoment.traceFourier