OAI/Geometry/TamingCompatibility/Hodge/HodgeManifoldPairingInitial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSliceForm_initial line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingFiberForm_initial line 45
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm_initial line 82
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.chart_density_compact_bound line 115
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.integral_chart_bound line 123