OAI/Geometry/TamingCompatibility/Hodge/HodgeCutoffSquare.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.scalar_second line 20
2. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.secondOrder_scalar_product line 41
3. def OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.cutoffFirst line 66
4. def OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.cutoffZero line 70
5. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.secondOrder_cutoff line 75
6. def OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.cutoffPrincipal line 103
7. lemma OAI.TamingCompatibility.GeometricHilbert.NormalHeatResidual.cutoff_gaussian_residual line 107
8. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.linear_bound_on_tube line 155
9. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.quadratic_bound_on_tube line 175
10. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.normal_bounds_on_tube line 201