OAI/Geometry/Cannon/Modulus/SqDiffNormDiff.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonRadialWitness.sq_diff_le_of_norm_diff line 12
2. lemma OAI.CannonRadialWitness.norm_one_sq line 23
3. theorem OAI.CannonRadialWitness.two_center_small line 28
4. theorem OAI.CannonRadialWitness.two_center_band line 105
5. lemma OAI.CannonRadialWitness.normalized_dist line 135
6. theorem OAI.CannonRadialWitness.two_center_band_scaled line 141