OAI/Analysis/CoulombRadii/FormDomain/L2MultiplierDistribution.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Coulomb.l2_multiplier_distributionline 81 - lemma
OAI.Coulomb.l2_fourier_weakDeriv_distributionline 97 - lemma
OAI.Coulomb.l2_fourier_weakDerivline 108 - lemma
OAI.Coulomb.fourierMultiplier_norm_sqline 133 - lemma
OAI.Coulomb.l2_norm_sq_fourierline 140 - lemma
OAI.Coulomb.l2_fourier_weighted_derivativeline 147