OAI/Geometry/TamingCompatibility/HeatFlow/HodgeClosedResolvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_power_closed_iff line 23
2. def OAI.TamingCompatibility.GeometricHilbert.hodgeIsExact line 32
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeIsExact_closed line 36
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_exact_iff line 42
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_power_exact_iff line 59
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_smooth_inverse line 70
7. theorem OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_smooth_closed_exact line 79