OAI/Geometry/TamingCompatibility/DifferentialForms/SecondVariationIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.PlaneVariation.continuousOn_secondVariation line 12
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationRaw line 34
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationDensity_eq_indicator line 44
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationVector line 63
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationVector_continuousOn line 69
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationRaw_continuousOn line 78
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.secondVariationDensity_integrable line 94