OAI/Combinatorics/Progressions/Geometry/NativeProductOrbitMetric.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.productMetricBound line 15
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.productInclusionHom_lipschitz line 25
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.productSpaceEquiv_symm_coordinate_lipschitz line 38
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.productSpaceEquiv_symm_lipschitz line 79
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.productSpaceEquiv_lipschitz line 87
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.productMetricBound_le line 118
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.productMetricBound_le_exp line 136
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.realBCHPiEquiv_symm_lipschitz line 163
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.native_product_group_dist_le line 196
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_cyclicOrbitPoint line 233
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.productSpaceEquiv_cyclicOrbitPoint line 243
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.pi_cyclicOrbitPoint_dist_le line 254
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.pi_cyclicOrbitPoint_dist_le_exp line 282