OAI/Geometry/TamingCompatibility/Hodge/HodgeH1.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraph_norm_sq line 25
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmooth_dense line 49
3. def OAI.TamingCompatibility.GeometricHilbert.hodgeToH1 line 52
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeToH1_bound line 56
5. def OAI.TamingCompatibility.GeometricHilbert.hodgeEnergyToH1 line 87
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergyToH1_smooth line 91
7. lemma OAI.TamingCompatibility.ComplexMatrix.full_metric_square_regular line 107
8. lemma OAI.TamingCompatibility.ComplexMatrix.full_metric_square_uniform_regular line 148
9. lemma OAI.TamingCompatibility.ComplexMatrix.full_metric_square_uniform_estimate line 191