OAI/Geometry/TamingCompatibility/Elliptic/MemSobolevSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_sum line 15
2. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_of_laplacian line 24
3. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_succ_of_derivatives line 29
4. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.schwartz_derivative_product line 41
5. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.distribution_derivative_product line 57
6. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_zero_product line 67
7. theorem OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_nat_product line 78