OAI/Analysis/RieszRectifiability/Nets/RegularLatticeScales.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.latticeRadius line 13
2. theorem OAI.RieszRectifiability.latticeRadius_zero line 15
3. theorem OAI.RieszRectifiability.latticeRadius_pos line 17
4. theorem OAI.RieszRectifiability.latticeRadius_succ line 21
5. theorem OAI.RieszRectifiability.latticeRadius_add line 26
6. theorem OAI.RieszRectifiability.latticeRadius_antitone line 30
7. theorem OAI.RieszRectifiability.latticeRadius_tendsto_zero line 35
8. theorem OAI.RieszRectifiability.latticeRadius_binary_levels line 40
9. theorem OAI.RieszRectifiability.latticeRadius_sum_le line 46
10. theorem OAI.RieszRectifiability.netAncestor_dist_le_latticeRadius line 56