OAI/Geometry/TamingCompatibility/Functional/PhysicalProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_continuous line 27
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_nonneg line 35
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_le_one line 40
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_symm line 47
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_volume_growth line 53
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfile_unit_integrable line 68
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfileMass line 81
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfileMass_integrable line 84
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfileMass_nonneg line 91
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfileMass_volume_growth line 96
12. lemma OAI.TamingCompatibility.compact_physical_chart_near line 122