OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactCuspCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite disjoint cusp cover gives smooth compact cutoffs on the actual quotient by subtracting its scalar incoming cusp cutoffs.

  1. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_mono line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaDisjointCuspCover line 19
  3. def OAI.CubicFirstMoment.cubicThetaCompactCuspCutoff line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaCompactCuspCutoff_continuous line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaCompactCuspCutoff_smooth line 43
  6. lemma OAI.CubicFirstMoment.cubicThetaCompactCuspCutoff_high line 49
  7. lemma OAI.CubicFirstMoment.cubicThetaCompactCuspCutoff_compact line 65