OAI/Geometry/TamingCompatibility/Hodge/HodgeHarmonicSmooth.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.GeometricHilbert.hodge_harmonic_smooth line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_dense line 56
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_fixed_of_weak_harmonic line 68
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_weak_harmonic_graph line 89
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmooth_closed_of_weakDerivative_zero line 104
6. theorem OAI.TamingCompatibility.GeometricHilbert.hodge_weak_harmonic_smooth line 113
7. def OAI.TamingCompatibility.GeometricHilbert.hodgePreClosed line 140
8. def OAI.TamingCompatibility.GeometricHilbert.hodgeClosedL2 line 146
9. def OAI.TamingCompatibility.GeometricHilbert.hodgeWeakClosedL2 line 149
10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakClosedL2_isClosed line 156
11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmooth_mem_weakClosed line 163
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmooth_mem_closedL2 line 171
13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeClosedL2_le_weakClosed line 176
14. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_closed_orthogonal_zero line 182
15. theorem OAI.TamingCompatibility.GeometricHilbert.hodgeClosedL2_eq_weakClosed line 200
16. theorem OAI.TamingCompatibility.GeometricHilbert.hodge_pair_weakClosed_eq_zero line 216