OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialHolder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The one-dimensional H1 modulus of continuity, derived from the fundamental theorem of calculus and Hilbert-space Cauchy--Schwarz.

  1. lemma OAI.CubicFirstMoment.cubicTheta_integral_sq_bound line 12
  2. theorem OAI.CubicFirstMoment.cubicTheta_radial_holder_sq line 47