OAI/Analysis/KLS/Sobolev/WeakDerivatives.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DeGiorgi.HasWeakPartialDeriv line 23
2. abbrev OAI.DeGiorgi.HasWeakPartialDeriv' line 31
3. def OAI.DeGiorgi.HasWeakGrad line 34
4. def OAI.DeGiorgi.HasWeakDiv line 37
5. theorem OAI.DeGiorgi.HasWeakPartialDeriv.ae_eq line 47
6. theorem OAI.DeGiorgi.HasWeakPartialDeriv.of_contDiff line 87
7. theorem OAI.DeGiorgi.HasWeakPartialDeriv.mul_smooth line 129
8. theorem OAI.DeGiorgi.HasWeakPartialDeriv.restrict line 200
9. lemma OAI.DeGiorgi.tendsto_integral_mul_of_eLpNorm_tendsto_zero_p line 231
10. theorem OAI.DeGiorgi.HasWeakPartialDeriv.of_eLpNormApprox_p line 299