OAI/NumberTheory/CubicMoment/Theta/CubicThetaL2Cutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Restriction to a measurable height region as a contraction on L2.

  1. def OAI.CubicFirstMoment.cubicThetaL2CutoffFun line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaL2CutoffFun_coe line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaL2CutoffFun_bound line 19
  4. def OAI.CubicFirstMoment.cubicThetaL2CutoffLinear line 26
  5. def OAI.CubicFirstMoment.cubicThetaL2Cutoff line 52
  6. lemma OAI.CubicFirstMoment.cubicThetaL2Cutoff_coe line 58
  7. lemma OAI.CubicFirstMoment.cubicThetaL2Cutoff_norm_sq line 61