OAI/Probability/LatticeSurface/Dynamics/ShiftAsymptotics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FeasibleShift.scaled_radius_tendsto line 9
2. lemma OAI.FeasibleShift.radius_power line 21
3. lemma OAI.FeasibleShift.scaled_radius_sq_tendsto line 25
4. lemma OAI.FeasibleShift.tail_radius_bound_tendsto line 30
5. lemma OAI.FeasibleShift.small_parameter_eventually line 43