OAI/Geometry/PolarProducts/Nonsqueezing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderParameters.weights line 16
2. theorem OAI.CylinderParameters.energy_weights line 18
3. theorem OAI.CylinderParameters.energy_weights_upper line 27
4. theorem OAI.CylinderParameters.gap_first line 35
5. theorem OAI.CylinderParameters.gap_small line 44
6. theorem OAI.CylinderParameters.weights_bounds line 55
7. theorem OAI.CylinderParameters.exists_parameters line 75
8. theorem OAI.CylinderNonsqueezing.radius_le_of_embedding line 112