OAI/Geometry/TamingCompatibility/Hodge/HodgeApproximateIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_decay line 17
2. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_scale_inverse_sqrt line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_approximate_identity line 35
4. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.adjoint_product_commutes line 70
5. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.fderiv_commutes line 81
6. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.firstMatrix_commutes line 95
7. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.zeroMatrix_commutes line 115
8. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.gauge_commutes line 136