OAI/Geometry/TamingCompatibility/Charts/AffineBase.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.EuclideanSobolevOperators.affineSchwartz line 19
2. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineSchwartz_apply line 25
3. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineSchwartz_derivative line 30
4. def OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution line 43
5. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_apply line 47
6. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_derivative line 52
7. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memLp_comp_affine line 62
8. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_lp line 71
9. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_zero_affine line 106
10. theorem OAI.TamingCompatibility.EuclideanSobolevOperators.memSobolev_nat_affine line 116
11. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affine_inverse_point line 155
12. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_product line 160
13. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_fiberMap line 176
14. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.affineDistribution_inverse line 182
15. def OAI.TamingCompatibility.EuclideanSobolevOperators.zoomDistribution line 190
16. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.zoomDistribution_product line 194
17. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.zoomDistribution_second line 205
18. lemma OAI.TamingCompatibility.EuclideanSobolevOperators.zoomDistribution_memSobolev line 211