OAI/Geometry/TamingCompatibility/Hodge/HodgeGraphSmoothing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraphResolvent_raw_H5 line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.exists_hodgeGraphResolvent_lift line 49
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy_prod_norm_sq line 90
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergy_prod_norm_le line 94
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakSolution_derivative_bound line 102
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakSolution_graph_bound line 122
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakSolution_graph_small_bound line 138