OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialConductor.lean
4 declarations, 0 contain sorry, 0 declared as axioms
The Green norm decreases with the actual Fourier potential. This uniform estimate is needed when the cusp modes are assembled.
- lemma
OAI.CubicFirstMoment.cubicThetaRadialJet_mass_boundline 12 - lemma
OAI.CubicFirstMoment.cubicThetaRadial_test_mass_boundline 23 - theorem
OAI.CubicFirstMoment.cubicThetaRadial_mass_boundline 47 - theorem
OAI.CubicFirstMoment.cubicThetaRadialGreen_conductor_boundline 59