OAI/Geometry/TamingCompatibility/Currents/PlaneMeasure.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeAreaCut line 19
2. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeBaseCut line 22
3. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeBaseCut_measurable line 26
4. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeAreaCut_measurable line 33
5. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeAreaCut_nonneg line 40
6. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeAreaCut_integrable line 46
7. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeMeasure line 60
8. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeMeasure_finite line 65
9. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.planeMeasure_integral line 78
10. lemma OAI.TamingCompatibility.ManifoldForms.pullback_exteriorDerivative_chartLift line 114
11. def OAI.TamingCompatibility.Concentration.testOne line 134
12. lemma OAI.TamingCompatibility.Concentration.testOne_smooth line 137
13. lemma OAI.TamingCompatibility.Concentration.testOne_compact line 140
14. lemma OAI.TamingCompatibility.Concentration.testOne_support line 143
15. lemma OAI.TamingCompatibility.Concentration.testOne_deriv line 146
16. lemma OAI.TamingCompatibility.Concentration.testOne_skew line 158