OAI/Geometry/TamingCompatibility/Hodge/HodgeKernelWeakAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelWeakAction line 21
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernel_pairing_integral_continuousOn line 26
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernel_leading_pairing_hasDerivAt line 47
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.kernelWeakAction_leading_hasDerivAt line 63
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.actual_cutoff_initial_local line 118
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.cutoff_form_initial line 163