OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelTestTransform.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestLinear line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestLinear_measurable line 28
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestLinear_integrable line 44
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestLinear_apply line 65
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelTestLinear_uniform_bound line 75
6. lemma OAI.TamingCompatibility.MetricForms.abs_pairing_le_sqrt line 107
7. def OAI.TamingCompatibility.GeometricHilbert.pointNorm line 123
8. lemma OAI.TamingCompatibility.GeometricHilbert.pointNorm_continuous line 128
9. lemma OAI.TamingCompatibility.GeometricHilbert.pointNorm_sq line 133
10. lemma OAI.TamingCompatibility.GeometricHilbert.pointNorm_integral_sq line 137
11. lemma OAI.TamingCompatibility.GeometricHilbert.pointNorm_product_integral line 142
12. lemma OAI.TamingCompatibility.GeometricHilbert.bounded_pairing_integrable line 157
13. lemma OAI.TamingCompatibility.GeometricHilbert.bounded_pairing_integral_bound line 171