OAI/NumberTheory/CubicMoment/Estimates/CubicBesselContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local dominated continuity of the fixed positive Bessel integral.

  1. lemma OAI.CubicFirstMoment.cubicBesselHeat_local_bound line 11
  2. lemma OAI.CubicFirstMoment.cubicBessel_integral_continuousAt line 23
  3. theorem OAI.CubicFirstMoment.cubicBesselKernel_continuousOn line 42

    Source documentation

    The fixed kernel is continuous on its positive domain.

    theorem cubicBesselKernel_continuousOn : ContinuousOn cubicBesselKernel (Ioi 0) := by
…

    Mentions: OAI.CubicFirstMoment.cubicBesselKernel