OAI/Geometry/TamingCompatibility/Hodge/HodgeCorrectionRegularization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionRegularize line 25
2. theorem OAI.TamingCompatibility.GeometricHilbert.exists_regularizable_closed_lift line 32
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionRegularize_mixing line 50
4. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_star line 84
5. lemma OAI.TamingCompatibility.GeometricHilbert.smoothAntiProjection_star line 92
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_cube_star line 101
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_star line 110
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionRegularize_star line 120
9. def OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectedSource line 151
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectedSource_annihilates line 160
11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrected_regularize_represents line 171
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrected_energy_identity line 184