OAI/Combinatorics/Progressions/Estimates/FastCoefficientImage.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.NilpotentLieFiltration.FirstCoefficientModule line 15
  2. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientMap line 19
  3. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientMap_eq_zero_iff line 24
  4. abbrev OAI.Erdos3.NilpotentLieFiltration.FirstCoefficientIndex line 30
  5. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientSurvivorEquiv line 33
  6. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientBasis line 50
  7. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientBasis_repr_map line 58
  8. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientMap_surjective line 82
  9. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal line 85
  10. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_map line 97
  11. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientConstant line 101
  12. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_constant line 106
  13. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontalSection line 111
  14. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontalSection_mk line 118
  15. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientHorizontal_section line 121
  16. def OAI.Erdos3.NilpotentLieFiltration.normalizedFirstCoefficientMap line 126
  17. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedFirstCoefficientMap_eq_zero_iff line 132
  18. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedFirstCoefficientMap_range line 136
  19. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientIndex_grade_pos line 155
  20. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientIndex_zero_iff_grade_one line 160
  21. theorem OAI.Erdos3.NilpotentLieFiltration.exists_sorted_firstCoefficient_rows line 176
  22. theorem OAI.Erdos3.NilpotentLieFiltration.sorted_firstCoefficient_scale_bounds line 187
  23. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolKernel_lift line 212
  24. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolKernel_lie_eq_zero line 222
  25. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolKernel_bch line 230
  26. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolHom line 251
  27. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDiagonalSymbolHom line 254
  28. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSndSymbolHom_diagonal line 257
  29. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart line 262
  30. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_projection line 266
  31. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_coord_kernel line 270
  32. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_factorization line 274
  33. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_mul line 278
  34. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_mul_coord line 287
  35. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelative_same_diagonal_mod_kernel line 301
  36. def OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap line 335
  37. theorem OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap_apply line 339
  38. theorem OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap_projection line 343
  39. theorem OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap_range line 348
  40. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_of_factors line 362
  41. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifference line 385
  42. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifference_mk line 393
  43. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifference_mem_layer line 397
  44. theorem OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap_eq_zero_iff line 404
  45. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_reduced_square_relative_coord line 441
  46. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedFirstCoefficientMap_ker line 483
  47. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeRangeEquiv line 490
  48. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeRangeEquiv_apply line 496
  49. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeEquiv line 501
  50. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeEquiv_apply line 508
  51. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeMap line 514
  52. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeMap_injective line 520
  53. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientFastSubmodule line 523
  54. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientFastSubmodule_le_horizontal_ker line 528
  55. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedFirstCoefficientMap_mem_fast_iff line 534
  56. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRelativeGroupPart_triple_coord line 568
  57. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_reduced_square_derivative_factors line 583
  58. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifference_mem_two line 621
  59. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifferenceAdapted line 628
  60. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifferenceRelative line 638
  61. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifferenceRelative_coefficient line 651
  62. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareCoefficientMap line 657
  63. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareCoefficientMap_symbol line 668
  64. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareDifferenceRelative_relative line 673
  65. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareCoefficientMap_relative line 693
  66. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareCoefficientMap_horizontal line 701
  67. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareCoefficientMap_relativeMap line 719
  68. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRelativeMap_coefficientMap line 733
  69. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientFastSubmodule_eq_image line 750