OAI/Combinatorics/Progressions/Nilpotent/BCHUniformQuotientCharts.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.bchProductCoefficientBase line 13
  2. def OAI.Erdos3.bchProductCoefficientHeight line 17
  3. theorem OAI.Erdos3.bchProductCoefficientBase_pos line 20
  4. theorem OAI.Erdos3.bchProductDenominator_le_height line 24
  5. theorem OAI.Erdos3.bchProductNumeratorBound_le_height line 36
  6. theorem OAI.Erdos3.bchProductWordCoefficient_height line 66
  7. theorem OAI.Erdos3.bchProductBracketCoefficient_height line 74
  8. theorem OAI.Erdos3.bchProductCoordinatePolynomial_height line 92
  9. theorem OAI.Erdos3.bchProductCoefficientHeight_le_exp line 112
  10. theorem OAI.Erdos3.exists_bchProductCoordinatePolynomial_exp_budget line 145
  11. theorem OAI.Erdos3.exists_bch_product_coordinate_polynomials_exp_height line 226
  12. theorem OAI.Erdos3.exists_bch_product_box_bound line 263
  13. theorem OAI.Erdos3.bch_box_expression_le_exp line 303
  14. theorem OAI.Erdos3.exists_bch_group_product_exp_bound line 372
  15. theorem OAI.Erdos3.bch_bounded_product_box_expression_le_exp line 418
  16. theorem OAI.Erdos3.exists_bch_fixed_product_exp_bound line 436
  17. theorem OAI.Erdos3.bch_triple_box_expression_le_exp line 481
  18. theorem OAI.Erdos3.exists_bch_triple_product_exp_bound line 499
  19. theorem OAI.Erdos3.coordinateLipschitzBound_power_budget line 547
  20. theorem OAI.Erdos3.exists_bch_conjugation_basis_exp_bound line 568
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_left_lipschitz_exp_bound line 597
  22. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_lipschitz_left line 645
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_lipschitz_orbit line 654
  24. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_dist_action_le line 663
  25. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_quotient_left_lipschitz_exp_bound line 677
  26. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_coordinate_chart_metric_bounds line 717
  27. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHFlow_period line 811
  28. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHFlow_isometry line 818
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHFlow_displacement line 826
  30. def OAI.Erdos3.NilpotentLieBCHGroup.centralBCHCircleAction line 836
  31. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHCircleAction_act_coe line 849
  32. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHCircleAction_displacement line 859
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.centralBCHCircleAction_commutes line 871
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_quotient_isometric_radius_exp_bound line 895
  35. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_quotient_chart_metric_exp_bound line 944