OAI/Analysis/CoulombIonization/FormDomain/LipschitzWeak.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.mollified_lipschitz_derivative line 26
2. lemma OAI.CoulombAtom.convolution_bounded line 54
3. lemma OAI.CoulombAtom.bounded_lipschitz_smooth_approx line 66
4. lemma OAI.CoulombAtom.integral_real_mul_tendsto line 105
5. lemma OAI.CoulombAtom.smooth_lineDeriv_continuous line 126
6. lemma OAI.CoulombAtom.IsWeakDerivative.mul_lipschitz line 134