OAI/Geometry/NodalSets/Elliptic/RealDerivativeErrorBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Geometry.realGradientSquare_nonneg line 10
2. lemma OAI.Yau.Geometry.real_partial_sq_le_gradient line 13
3. lemma OAI.Yau.Geometry.real_matrix_flux_square_bound line 17
4. lemma OAI.Yau.Geometry.realDerivativeErrorFlux_square_bound line 32
5. lemma OAI.Yau.Geometry.real_coordDiv_neg line 38
6. lemma OAI.Yau.Geometry.real_differentiated_density_signed line 48