OAI/Geometry/TamingCompatibility/DifferentialForms/MetricSquareEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ComplexMatrix.metric_square_uniform_estimate line 18
2. structure OAI.TamingCompatibility.GeometricHilbert.SquareData line 55
3. lemma OAI.TamingCompatibility.GeometricHilbert.exists_geometric_square_data line 73
4. lemma OAI.TamingCompatibility.GeometricHilbert.exists_geometric_square_estimate line 131