OAI/Geometry/TamingCompatibility/Hodge/HodgeL2.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.GeometricHilbert.l2CurrentSourceline 19 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_l2_representsline 25 - lemma
OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_anti_sourceline 33 - def
OAI.TamingCompatibility.GeometricHilbert.positiveL2Sourceline 59 - lemma
OAI.TamingCompatibility.GeometricHilbert.positiveL2Source_representsline 62