OAI/Combinatorics/Progressions/Estimates/ImageRepresentatives.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.basis_repr_height_one line 17
  2. theorem OAI.Erdos3.lie_basis_bracket_height line 25
  3. theorem OAI.Erdos3.span_basis_brackets_layer line 37
  4. theorem OAI.Erdos3.exists_small_bounded_spanning_family line 66
  5. theorem OAI.Erdos3.exists_bounded_layer_spanning line 83
  6. def OAI.Erdos3.layerRoundingBound line 113
  7. theorem OAI.Erdos3.layerRoundingBound_mono_layer line 116
  8. theorem OAI.Erdos3.layerRoundingBound_le_exp line 120
  9. theorem OAI.Erdos3.exists_bounded_realification_layer_reduction line 170
  10. theorem OAI.Erdos3.exists_bounded_realification_factors line 227
  11. def OAI.Erdos3.lieTreeHeight line 265
  12. theorem OAI.Erdos3.lieTreeHeight_ge_input line 267
  13. theorem OAI.Erdos3.lieTreeHeight_mono line 275
  14. theorem OAI.Erdos3.lieTreeHeight_step line 280
  15. theorem OAI.Erdos3.lieTreeHeight_le_coordinateHeight line 303
  16. theorem OAI.Erdos3.lieTreeHeight_le_exp line 311
  17. theorem OAI.Erdos3.finiteLieTrees_coordinate_height line 319
  18. theorem OAI.Erdos3.exists_realification_representatives_exp_bound line 348
  19. theorem OAI.Erdos3.exists_compact_realification_representatives_exp_bound line 377
  20. theorem OAI.Erdos3.exists_rational_representatives_exp_bound line 410
  21. theorem OAI.Erdos3.exists_subgroup_index_exp_bound line 453
  22. theorem OAI.Erdos3.exists_controlled_normal_cover line 488
  23. theorem OAI.Erdos3.product_grid_allowance_le_exp line 535
  24. theorem OAI.Erdos3.exists_common_controlled_normal_cover line 547
  25. theorem OAI.Erdos3.matrixDenominator_allowance_le_exp line 599
  26. theorem OAI.Erdos3.bch_comap_inner_grid line 625
  27. theorem OAI.Erdos3.exists_bounded_image_representatives line 639