OAI/Analysis/PlanarPacking/Dilation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpPlanar.scaleEquiv line 11
2. def OAI.SharpPlanar.dilateSchwartz line 15
3. lemma OAI.SharpPlanar.dilateSchwartz_apply line 17
4. lemma OAI.SharpPlanar.plane_fourier_dilation line 19
5. lemma OAI.SharpPlanar.plane_fourier_real_const line 34
6. def OAI.SharpPlanar.scaleFactor line 41
7. lemma OAI.SharpPlanar.scaleFactor_pos line 42
8. lemma OAI.SharpPlanar.scaleFactor_sq line 43
9. lemma OAI.SharpPlanar.scaled_radius line 44
10. lemma OAI.SharpPlanar.scaleFactor_inv_sq line 47