OAI/Analysis/RieszRectifiability/Kernel/ApproximationComparison.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RieszRectifiability.integral_sq_four_step_boundline 14 - theorem
OAI.RieszRectifiability.fixed_pair_bound_of_approximationsline 40 - theorem
OAI.RieszRectifiability.exists_L2_limit_of_sq_distance_boundline 70