OAI/Geometry/TamingCompatibility/Hodge/HodgeGlobalKernelContinuity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalLeading_continuousAt line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalResidual_continuousAt line 30
3. lemma OAI.TamingCompatibility.GeometricHilbert.smooth_energy_laplacian line 51
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSliceForm_weak_laplacian line 68
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingSliceForm_weak_laplacian_all line 102
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairing_zero_form line 140
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pairing_sum_form line 144
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.integral_pairing_sum line 153
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingFiberForm_weak_laplacian line 165
10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingKernelForm_weak_laplacian line 181