OAI/Geometry/TamingCompatibility/Hodge/HodgeInputInitial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernel_pairing_integral_bound line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernel_leading_pairing_initial line 41
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelWeakAction_leading_initial line 55
4. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestSlice line 101
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestSlice_continuousOn line 107
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestSlice_uniform_bound line 119
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leading_time_primitive line 139