OAI/Geometry/TamingCompatibility/Hodge/HodgeRawRegular.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.TamingCompatibility.GeometricHilbert.hodge_resolvent_raw_gainline 23 - def
OAI.TamingCompatibility.GeometricHilbert.hodgeRegularizedGraphline 87 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodgeRegularizedGraph_inclusionline 92 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_raw_H5line 101