OAI/Geometry/TamingCompatibility/DifferentialForms/End.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.End line 25
2. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.Principal line 26
3. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.First line 27
4. def OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.euclideanPrincipal line 28
5. def OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.residual line 30
6. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.residual_bound line 38
7. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.exists_residual_bound line 95
8. def OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.applyOperator line 119
9. def OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.modelSection line 125
10. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.modelSection_fderiv line 127
11. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.modelSection_hessian line 134
12. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.modelSection_time line 143
13. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.residual_apply line 149