OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.unitIntegral line 23
2. def OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily line 37
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily_pair line 42
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily_tendsto line 55
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily_twice_pair_tendsto line 66
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily_anti_cross_tendsto line 80
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePositiveCurrentFamily_anti_wedge_tendsto line 94
8. lemma OAI.TamingCompatibility.GeometricHilbert.l2AntiProjection_idempotent line 119
9. lemma OAI.TamingCompatibility.GeometricHilbert.smoothAntiProjection_dense line 125
10. lemma OAI.TamingCompatibility.GeometricHilbert.smoothAntiProjection_closure line 136