OAI/Analysis/JiangSu/Comparison/FamilyDyadicApproximation.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.FamilyComparison.comparison_dyadic_approximationline 21 - theorem
OAI.FamilyComparison.comparison_exact_relative_cutline 90 - theorem
OAI.FamilyComparison.comparison_relative_partitionline 142