OAI/Probability/SpanningForest/FiniteGradientResponse.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem336.FiniteGradientResponse.segmentFieldline 13 - theorem
OAI.Problem336.FiniteGradientResponse.segmentField_zeroline 16 - theorem
OAI.Problem336.FiniteGradientResponse.segmentField_oneline 20 - theorem
OAI.Problem336.FiniteGradientResponse.abs_sum_mul_leline 24 - theorem
OAI.Problem336.FiniteGradientResponse.response_le_of_line_derivativeline 40