OAI/Geometry/TamingCompatibility/Elliptic/InteriorRegularity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.exists_outer_cutoff line 21
2. def OAI.TamingCompatibility.HilbertSobolev.MemSobolevLoc line 43
3. lemma OAI.TamingCompatibility.HilbertSobolev.MemSobolevLoc.mono line 47
4. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_H1_interior_bootstrap line 51
5. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_H1_interior_smooth line 91
6. def OAI.TamingCompatibility.EuclideanSobolevOperators.linearDistribution line 124
7. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.linearDistribution_apply line 128
8. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.linearSchwartz_derivative line 132
9. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.linearDistribution_derivative line 144
10. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memLp_comp_linearEquiv line 151
11. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.linearDistribution_lp line 160
12. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_zero_linear line 188
13. theorem OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_nat_linear line 196