OAI/Analysis/RieszRectifiability/Kernel/OrderedSpanConditioning.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.RieszRectifiability.OrderedSpanSeparatedline 13 - def
OAI.RieszRectifiability.spanConditionConstantline 18 - theorem
OAI.RieszRectifiability.spanConditionConstant_nonnegline 22 - theorem
OAI.RieszRectifiability.ordered_span_coefficient_boundline 30 - theorem
OAI.RieszRectifiability.linearIndependent_of_coordinate_boundline 45 - theorem
OAI.RieszRectifiability.ordered_span_linearIndependentline 57