OAI/NumberTheory/CubicMoment/Theta/CubicThetaCutoffEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Quantitative product estimates for the compact core cutoffs. The coefficient is compactly supported, so its supremum is finite.

  1. lemma OAI.CubicFirstMoment.cubicThetaTangentEnergy_nonneg line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaTangentEnergy_add_le line 15
  3. def OAI.CubicFirstMoment.cubicThetaFunctionEnergy line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaFunctionEnergy_mul line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_density line 45
  6. def OAI.CubicFirstMoment.cubicThetaCutoffEnergyCoefficient line 53
  7. lemma OAI.CubicFirstMoment.cubicThetaCutoffEnergyCoefficient_nonneg line 56
  8. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_cutoff_le line 61
  9. lemma OAI.CubicFirstMoment.cubicThetaFunctionEnergy_continuous line 81
  10. lemma OAI.CubicFirstMoment.cubicThetaFunctionEnergy_compact line 88
  11. lemma OAI.CubicFirstMoment.cubicThetaCutoffEnergyCoefficient_bounded line 99