OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.KernelL2.action line 18
2. lemma OAI.TamingCompatibility.GeometricHilbert.KernelL2.applied_measurable line 21
3. lemma OAI.TamingCompatibility.GeometricHilbert.KernelL2.action_measurable line 28
4. lemma OAI.TamingCompatibility.GeometricHilbert.KernelL2.action_integrable line 33
5. lemma OAI.TamingCompatibility.GeometricHilbert.KernelL2.action_norm line 43
6. lemma OAI.TamingCompatibility.GeometricHilbert.KernelL2.action_test_swap line 54
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameNormConstant line 101
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameNormConstant_nonneg line 104
9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelSectionL2 line 108
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelSectionL2_norm line 122
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelSectionL2_pairing line 134