OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialEquicontinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Unit-energy cusp test functions have a common square-root modulus of continuity and locally precompact restrictions.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadial_derivative_energy_le line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaRadial_unit_holder line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaRadial_unit_value line 41
  4. abbrev OAI.CubicFirstMoment.CubicThetaRadialUnitTests line 47
  5. def OAI.CubicFirstMoment.cubicThetaRadialCompactRestriction line 49
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialRestriction_equicontinuous line 54
  7. theorem OAI.CubicFirstMoment.cubicThetaRadialRestriction_precompact line 68