OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeTraceNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite trace has its Cauchy--Schwarz mass bound with the exact covering index. The integrability assertion is proved from this bound, so it will pass to the completed operator.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeTrace_norm_sq_le line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeSection_sheet_integrable line 36
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeTrace_majorant_integrable line 48
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeTrace_integrable line 60
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeTrace_mass_integral_le line 71