OAI/Combinatorics/IndependentSets/Geometry/CoordinateDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LargeIndependentSets.CubeGradient.coordinateDerivative line 10
2. lemma OAI.LargeIndependentSets.CubeGradient.coordinateDerivative_eq line 13
3. lemma OAI.LargeIndependentSets.CubeGradient.fderiv_coordinate_integrable line 20
4. theorem OAI.LargeIndependentSets.CubeGradient.integral_total_coordinate_variation line 30