OAI/Geometry/NodalSets/Elliptic/CommutatorBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Jets.DerivativeBound.sub line 10
2. lemma OAI.Yau.Jets.secondOrder_derivative_bound line 20
3. lemma OAI.Yau.Jets.real_smul_derivative_bound line 44
4. def OAI.Yau.Jets.cutoffCommutator line 59
5. lemma OAI.Yau.Jets.cutoffCommutator_contDiff line 64
6. theorem OAI.Yau.Jets.cutoffCommutator_polynomial_bound line 72
7. lemma OAI.Yau.Jets.coordPartial_eventuallyEq line 111
8. lemma OAI.Yau.Jets.smoothSecondOrder_eventuallyEq line 115
9. theorem OAI.Yau.Jets.cutoffCommutator_derivative_zero_near line 126
10. theorem OAI.Yau.Jets.cutoffCommutator_gaussian_bound line 143