OAI/Geometry/NodalSets/Coefficients/ResidualProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Jets.DerivativeBound.enlarge line 10
2. lemma OAI.Yau.Jets.DerivativeBound.const_mul line 14
3. lemma OAI.Yau.Jets.DerivativeBound.scale_power line 23
4. lemma OAI.Yau.Jets.DerivativeBound.exponent_mono line 33
5. lemma OAI.Yau.Jets.norm_complex_inv_pow line 39
6. theorem OAI.Yau.Jets.residual_times_exponential_bound line 44