OAI/Geometry/NodalSets/Coefficients/IntrinsicCoefficientIncrementBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Target.intrinsicChartCoefficient_increment line 15
2. lemma OAI.Yau.Target.seed_scalar_pullback_smooth line 24
3. lemma OAI.Yau.Target.round_increment_entry_smooth line 32
4. lemma OAI.Yau.Target.intrinsic_seed_increment_pullback_smooth line 41
5. lemma OAI.Yau.Target.intrinsic_seed_increment_smooth line 54
6. theorem OAI.Yau.Target.intrinsic_coefficient_increment_derivative_bound line 63