OAI/Geometry/TamingCompatibility/DifferentialForms/RawTest.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricChart.rawPair_manifoldTest line 20
2. lemma OAI.TamingCompatibility.GeometricChart.rawPair_manifoldTest_eventually line 33
3. lemma OAI.TamingCompatibility.GeometricChart.normalOperator_test line 39
4. def OAI.TamingCompatibility.GeometricChart.coordinateWeight line 62
5. lemma OAI.TamingCompatibility.GeometricChart.coordinateWeight_smooth line 66
6. lemma OAI.TamingCompatibility.GeometricChart.scalar_eq_weight line 72
7. def OAI.TamingCompatibility.GeometricChart.realPairSchwartz line 79
8. lemma OAI.TamingCompatibility.GeometricChart.realPairSchwartz_apply line 82
9. lemma OAI.TamingCompatibility.GeometricChart.realPairSchwartz_embed line 88
10. lemma OAI.TamingCompatibility.GeometricChart.realPairSchwartz_raw line 94
11. lemma OAI.TamingCompatibility.GeometricChart.cutoff_realPair_raw line 103
12. lemma OAI.TamingCompatibility.GeometricHilbert.scalarDistribution_smooth line 122
13. def OAI.TamingCompatibility.GeometricHilbert.rawDistribution line 130
14. lemma OAI.TamingCompatibility.GeometricHilbert.rawDistribution_H1 line 135
15. lemma OAI.TamingCompatibility.GeometricHilbert.rawDistribution_smooth line 145