OAI/Geometry/TamingCompatibility/DifferentialForms/PhysicalSchur.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalProfileMass_quadratic line 22
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalGradientMass line 32
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalGradientMass_integrable line 35
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalGradientMass_schur line 41
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalGradientMass_L2_limit line 62
6. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError line 105
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_nonneg line 109
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_integrand_integrable line 116
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_product_integrable line 128
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_integrable line 147
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_integral line 155
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.physicalQError_limit line 171