OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeTraceNormBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite trace has operator norm at most the square root of the covering degree, separately for actual mass and derivative energy.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_norm_sq_le line 16
  2. def OAI.CubicFirstMoment.cubicThetaPrimeTraceMassMajorant line 35
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceMassMajorant_integrable line 40
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceMassMajorant_integral line 48
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeTrace_mass_integral_le line 65
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeTraceFinite_value_norm_sq line 77
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeTraceFinite_gradient_norm_sq line 84