OAI/Combinatorics/Progressions/Estimates/ReducedRelativeCoefficientBounds.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_basis_coordinate line 22
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_matrix_entry line 36
  3. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareRealFastRelative_adjoint_mem line 63
  4. def OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeInFirst line 93
  5. def OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelativeInFirst line 98
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedRelativeInFirst_coe line 103
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_eq line 110
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_adjoint line 118
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_fast_mem line 129
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeSquareSymbolMap_triple_preimage line 161
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realReducedRelativeCoefficient_triple line 183
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_mul line 220
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_cancel_inv line 234
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_fast_map line 245
  15. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAdjoint line 265
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAdjoint_mk line 277
  17. theorem OAI.Erdos3.NilpotentLieFiltration.coefficient_common_derivative_identity line 301
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficient_common_derivative line 328
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficient_common_mod_fast line 344
  20. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientSlowBound_sub line 379
  21. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGrid_sub line 388
  22. theorem OAI.Erdos3.NilpotentLieFiltration.coefficient_common_derivative_difference line 403
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_adjoint line 433
  24. def OAI.Erdos3.NilpotentLieFiltration.coefficientSlowCorrection line 469
  25. def OAI.Erdos3.NilpotentLieFiltration.coefficientGridCorrection line 476
  26. theorem OAI.Erdos3.NilpotentLieFiltration.synchronized_coefficient_common_derivative line 482
  27. abbrev OAI.Erdos3.NilpotentLieFiltration.RealFastCoefficientModule line 525
  28. def OAI.Erdos3.NilpotentLieFiltration.realFastDiagonalSubgroup line 528
  29. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realFastDiagonalSubgroup line 533
  30. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAdjoint_one line 537
  31. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAdjoint_mul line 550
  32. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAction line 570
  33. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAction_mk line 583
  34. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAction_horizontal line 590
  35. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientSlowBound_add line 618
  36. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientSlowBound_mono line 627
  37. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGrid_add line 634
  38. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGrid_mono line 646
  39. theorem OAI.Erdos3.NilpotentLieFiltration.exists_firstCoefficient_direction_bound line 652
  40. def OAI.Erdos3.NilpotentLieFiltration.ReducedRelativeCoefficientSpec line 688
  41. theorem OAI.Erdos3.NilpotentLieFiltration.exists_reducedRelativeCoefficient_bound line 712