OAI/Analysis/CoulombRadii/FormDomain/SchwartzFourierDerivativeNorm.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Coulomb.schwartz_fourier_derivative_normline 81 - lemma
OAI.Coulomb.schwartz_fourier_weighted_integrableline 91 - lemma
OAI.Coulomb.schwartz_fourier_weighted_integralline 96 - lemma
OAI.Coulomb.packetState_fourier_applyline 103 - lemma
OAI.Coulomb.packetState_fourier_joint_continuousline 118