OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothSpatial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_encode line 25
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.smoothL2_eq_of_framePairings line 36
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.framePairing_fun_smul line 55
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frame_kernel_pairing_continuous line 68
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frame_kernel_scalar_eq_of_smooth_tests line 78
6. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationTerm line 137
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationTerm_continuous line 143
8. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluation line 164
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluation_continuous line 168
10. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluationTerm_smooth_sum line 176
11. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.pairingEvaluation_smooth line 210