OAI/Combinatorics/Progressions/Estimates/ReducedNativeFactorization.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeSubmodule_lie_mem line 17
  2. def OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeIdeal line 30
  3. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeSubmodule_adjoint_mem line 34
  4. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquareLift_lie line 39
  5. def OAI.Erdos3.NilpotentLieBCHGroup.realLinearCoordinateLift line 64
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.realLinearCoordinateLift_coord line 69
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_controlled_fast_lift line 73
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.synchronize_with_linear_fast_lift line 115
  9. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealSymbolHom line 151
  10. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealLinearLift line 158
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_reduced_fast_lift line 167
  12. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealSymbolKernel_eq line 228
  13. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealSymbolKernel_lie_eq_zero line 233
  14. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealSymbolKernel_bch line 250
  15. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealDiagonalHom line 274
  16. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealSymbolHom_diagonal line 282
  17. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart line 294
  18. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_projection line 299
  19. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_coord_kernel line 304
  20. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_factorization line 310
  21. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_mul line 316
  22. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_mul_coord line 324
  23. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelative_same_diagonal_mod_kernel line 341
  24. def OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap line 384
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_range line 389
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_projection line 398
  27. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_exists_preimage line 407
  28. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_of_factors line 416
  29. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelativePart_triple_coord line 428
  30. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_ker line 454
  31. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientRelativeRangeEquiv line 466
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientRelativeRangeEquiv_apply line 471
  33. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientRelativeEquiv line 478
  34. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientRelativeEquiv_apply line 489
  35. def OAI.Erdos3.NilpotentLieFiltration.adaptedReducedSymbolMap line 511
  36. def OAI.Erdos3.NilpotentLieFiltration.adaptedReducedRealSymbolHom line 515
  37. def OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelativeAdjoint line 522
  38. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelativeAdjoint_inclusion line 528
  39. theorem OAI.Erdos3.NilpotentLieFiltration.reducedRelativeSquareSymbolMap_lie line 535
  40. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_adjoint line 548
  41. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientFastSubmodule line 585
  42. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientFastSubmodule_le_horizontal_ker line 588
  43. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_mem_fast_iff line 598
  44. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_sub_mem_fast_iff line 619
  45. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal line 628
  46. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontalSection line 634
  47. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal_section line 639
  48. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealRelative_conjugation line 658
  49. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_conjugation line 669
  50. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_conjugation_of_eq line 680
  51. def OAI.Erdos3.NilpotentLieFiltration.reducedNativeIndex line 702
  52. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeIndex_injective line 707
  53. def OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection line 725
  54. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_basis line 728
  55. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedReducedSymbolMap_native_basis line 732
  56. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_rightInverse line 752
  57. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_coordinate line 762
  58. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_coordinate_zero line 776
  59. def OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient line 802
  60. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient_horizontal line 808
  61. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient_of_preimage line 814
  62. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient_same_diagonal line 828
  63. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_real_coordinate line 864
  64. theorem OAI.Erdos3.NilpotentLieFiltration.reducedNativeSection_real_coordinate_zero line 874
  65. def OAI.Erdos3.NilpotentLieFiltration.realReducedNativeLift line 884
  66. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedReducedRealSymbolHom_lift line 888
  67. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedNativeLift_slow line 904
  68. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedNativeLift_grid line 919
  69. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedNativeLift_constant line 938
  70. theorem OAI.Erdos3.NilpotentLieFiltration.exists_reduced_native_factorization line 972