OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialTent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A concrete nonnegative radial test supported in [2,4].

  1. def OAI.CubicFirstMoment.cubicThetaRadialTent line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRadialTent_nonneg line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialTent_continuous line 16
  4. lemma OAI.CubicFirstMoment.cubicThetaRadialTent_compact line 20
  5. def OAI.CubicFirstMoment.cubicThetaRadialTestWeight line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialTestWeight_apply line 35
  7. lemma OAI.CubicFirstMoment.cubicThetaPositive_setIntegral line 38