OAI/Combinatorics/Progressions/Estimates/ReducedSquareSymbol.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.quotientLie_mem_iff line 12
  2. def OAI.Erdos3.NilpotentLieFiltration.quotientGradedMap line 18
  3. theorem OAI.Erdos3.NilpotentLieFiltration.quotientGradedMap_piece line 23
  4. theorem OAI.Erdos3.NilpotentLieFiltration.quotientGradedMap_piece_eq_zero_iff line 30
  5. def OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedMap line 39
  6. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedMap_piece_eq_zero_iff line 42
  7. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedMap_top line 51
  8. theorem OAI.Erdos3.NilpotentLieFiltration.mem_normalizedRelative_iff_firstJet line 70
  9. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelative_mem_of_firstJet_eq line 82
  10. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeLog_shifted line 93
  11. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeLog_horizontal line 109
  12. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeLog_mem line 123
  13. def OAI.Erdos3.NilpotentLieFiltration.differentiatedRelativeLog line 130
  14. theorem OAI.Erdos3.NilpotentLieFiltration.differentiatedRelativeLog_mem line 135
  15. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelative_square_symbol line 141
  16. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDiagonalPiece line 161
  17. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelativePiece line 165
  18. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDiagonalPiece_eq_zero_iff line 169
  19. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelativePiece_eq_zero_iff line 177
  20. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelative_top_injective line 186
  21. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDiagonal_top line 196
  22. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDiagonal_lie line 200
  23. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDiagonal_relative_lie line 207
  24. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelative_lie line 215
  25. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelativeSubalgebra line 223
  26. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedRelativeSubalgebra_lie_eq_zero line 227
  27. theorem OAI.Erdos3.NilpotentLieFiltration.square_relative_diagonal_factorization line 250
  28. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_square_symbol_factorization line 266
  29. theorem OAI.Erdos3.NilpotentLieFiltration.exists_normalized_square_symbol_factorization line 286
  30. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_sub_mem line 318
  31. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedAdjointConstant_sub_mem line 342
  32. theorem OAI.Erdos3.NilpotentLieFiltration.filteredFirstJet_logDerivative_eq line 363
  33. def OAI.Erdos3.NilpotentLieFiltration.symbolLogDerivative line 370
  34. theorem OAI.Erdos3.NilpotentLieFiltration.symbolLogDerivative_map line 375
  35. def OAI.Erdos3.NilpotentLieFiltration.symbolAdjointConstant line 381
  36. theorem OAI.Erdos3.NilpotentLieFiltration.symbolAdjointConstant_map line 388
  37. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeLog_symbol_formula line 399
  38. theorem OAI.Erdos3.NilpotentLieFiltration.differentiatedRelativeLog_firstJet_eq line 408
  39. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelative_square_symbol_congr line 422
  40. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_square_symbol_congr line 437
  41. def OAI.Erdos3.NilpotentLieFiltration.reducedSquarePolynomialMap line 470
  42. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolMap line 477
  43. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolMap_symbol line 483
  44. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolMap_lieBCH line 487
  45. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_reduced_square_symbol_factorization line 497