OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactBorelRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A bounded compact restriction of the actual global L2 lift. This permits cusp Fourier windows after arbitrary integral coordinate changes.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompact_pull_ae line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaBorelLift_compact_memLp line 21
  3. def OAI.CubicFirstMoment.cubicThetaCompactBorelRestrictionLinear line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaCompactBorelRestrictionLinear_bound line 78
  5. def OAI.CubicFirstMoment.cubicThetaCompactBorelRestriction line 104
  6. lemma OAI.CubicFirstMoment.cubicThetaCompactBorelRestriction_coe line 109
  7. lemma OAI.CubicFirstMoment.cubicThetaCompactBorelRestriction_section line 115