OAI/NumberTheory/CubicMoment/Theta/CubicThetaSobolevEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual real and imaginary Sobolev vectors are bounded by the complex Euclidean energy integral. This is the norm comparison needed to apply the local compact inclusion to the automorphic energy.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.l2_norm_sq line 16
  2. lemma OAI.CubicFirstMoment.LocalSobolev.value_norm_sq line 26
  3. lemma OAI.CubicFirstMoment.LocalSobolev.gradientL2_norm_sq line 34
  4. lemma OAI.CubicFirstMoment.LocalSobolev.four_norms_eq line 42
  5. lemma OAI.CubicFirstMoment.LocalSobolev.prod_norm_sq_le line 76
  6. lemma OAI.CubicFirstMoment.LocalSobolev.sobolev_pair_norm_sq_le line 85