OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootTranslationL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fractional translations extend isometrically to the actual completed space of root-cover sections.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootResidueSection_memLp line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteResidue line 30
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteResidue_norm line 38
  4. def OAI.CubicFirstMoment.cubicThetaPrimeRootResidueL2 line 58
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootResidueL2_finite line 63