OAI/Geometry/TamingCompatibility/Hodge/HodgeCorrectionLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionFamily line 24
2. theorem OAI.TamingCompatibility.GeometricHilbert.exists_convergent_closed_lift line 30
3. lemma OAI.TamingCompatibility.unitMeasureCurrent_taming_normalized line 70
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_eq line 88
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_taming line 114