OAI/Geometry/Cannon/Modulus/BinNearCard.lean
14 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CannonCapacity.bin_near_cardline 26 - theorem
OAI.CannonCapacity.exists_radial_binsline 50 - lemma
OAI.CannonCapacity.subexponential_stretchline 101 - lemma
OAI.CannonCapacity.eventually_exp_dominationline 116 - theorem
OAI.CannonCapacity.eventually_capacity_thresholdsline 127 - theorem
OAI.CannonCapacity.uniform_separated_capacityline 187 - lemma
OAI.CannonCapacity.clip_memline 293 - lemma
OAI.CannonCapacity.positive_clip_endpointsline 296 - lemma
OAI.CannonCapacity.exists_wide_active_rangeline 311 - lemma
OAI.CannonCapacity.small_outer_lower_endline 351 - lemma
OAI.CannonCapacity.small_outer_upper_startline 362 - theorem
OAI.CannonCapacity.bad_node_large_rangeline 373 - theorem
OAI.CannonCapacity.node_radial_coverline 415 - theorem
OAI.CannonCapacity.bad_node_many_childrenline 443