OAI/Combinatorics/Progressions/Nilpotent/BCHSmoothPartitionBudget.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_mfderiv_coordinateLine line 20
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.enorm_mfderiv_coordinateLine line 31
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.pathELength_coordinateLine line 41
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_one_le_coordinateL2Norm line 55
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_le_coordinateL2Norm_mul_inv line 71
  6. def OAI.Erdos3.bchBoxMetricConstant line 89
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_le_bchBoxMetricConstant line 108
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitzOn_basisHomeomorph_symm_box line 126
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_linear_lift_le line 165
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_local_metric_lifts_of_section line 209
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_local_metric_lifts_on_image line 229
  12. theorem OAI.Erdos3.coordinateL2Norm_smul line 265
  13. def OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine line 276
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine_zero line 278
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine_one line 282
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine_add line 286
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine_commute line 292
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.realBCHLine_dist_one_le line 301
  19. theorem OAI.Erdos3.exists_bchBoxMetricConstant_exp_bound line 321
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitzOn_quotient_basisHomeomorph_symm_box line 399
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_coordinateBox_metric_cover line 428
  22. def OAI.Erdos3.bchInjectivityRadius line 471
  23. theorem OAI.Erdos3.bchInjectivityRadius_pos line 474
  24. theorem OAI.Erdos3.bchInjectivityRadius_le_one line 479
  25. theorem OAI.Erdos3.bchInjectivityRadius_separation line 485
  26. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_coordinate_injOn line 505
  27. theorem OAI.Erdos3.exists_bch_partition_input_exp_bound line 534
  28. theorem OAI.Erdos3.inverse_radius_product_exp_bound line 576
  29. theorem OAI.Erdos3.enlarged_power_dominates_twice_add_sixteen line 587
  30. theorem OAI.Erdos3.exists_bchInjectivityRadius_inv_exp_bound line 608
  31. theorem OAI.Erdos3.bchBoxCoordinateBound_le_bchBoxMetricConstant line 647
  32. theorem OAI.Erdos3.exists_bchInverseBoxConstant_exp_bound line 653
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_inverse_chart_lipschitz_exp_bound line 703
  34. theorem OAI.Erdos3.bchLogMetricConstant_le_inverseBoxConstant line 735
  35. theorem OAI.Erdos3.smooth_partition_cost_le_exp line 742
  36. theorem OAI.Erdos3.smooth_partition_power_budget line 770