OAI/Combinatorics/Progressions/Polynomial/ShiftedPolynomialBasis.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.normalizedShiftLog line 13
  2. theorem OAI.Erdos3.VectorPolynomial.eval_normalizedShiftLog line 17
  3. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedShiftLog_adapted line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedShiftLog_sub_coefficient_mem line 38
  5. theorem OAI.Erdos3.NilpotentLieFiltration.positive_weight_of_ne_zero line 82
  6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_square_polynomial line 87
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_normalized_shift_square line 124
  8. theorem OAI.Erdos3.NilpotentLieFiltration.square_polynomial_quotient_adapted line 134
  9. abbrev OAI.Erdos3.NilpotentLieFiltration.PolynomialSymbol line 154
  10. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap line 157
  11. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_surjective line 161
  12. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_eq_zero_iff line 165
  13. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_eq_iff line 170
  14. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_lieBCH line 177
  15. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbol_lowerCentralSeries_eq_bot line 182
  16. abbrev OAI.Erdos3.NilpotentLieFiltration.PolynomialSymbolGroup line 187
  17. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolHom line 190
  18. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolHom_coord line 194
  19. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolHom_surjective line 198
  20. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_constant line 204
  21. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_translate line 209
  22. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_normalizedShift line 219
  23. theorem OAI.Erdos3.VectorPolynomial.exponent_of_weight_le_one line 240
  24. theorem OAI.Erdos3.VectorPolynomial.eq_affine_of_degreeLE_one line 251
  25. theorem OAI.Erdos3.VectorPolynomial.eval₂_affine_of_degreeLE_one line 276
  26. def OAI.Erdos3.NilpotentLieFiltration.adaptedCoefficientMap line 297
  27. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedCoefficientMap_apply line 302
  28. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolCoefficient line 306
  29. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolCoefficient_map line 313
  30. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolCoefficient_mem_layer_image line 318
  31. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbol_ext line 325
  32. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolCoefficient_eq_zero_of_weight_gt line 339
  33. theorem OAI.Erdos3.NilpotentLieFiltration.mem_layer_iff_basis_coordinates line 365
  34. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedSubmodule_eq_span_tensorBasis line 370
  35. def OAI.Erdos3.NilpotentLieFiltration.adaptedMonomialBasis line 386
  36. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedMonomialBasis_coe line 391
  37. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedMonomialBasis_repr line 400
  38. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedAdaptedIdeal_eq_span_monomialBasis line 409
  39. def OAI.Erdos3.NilpotentLieFiltration.adaptedWeightedDilation line 441
  40. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedWeightedDilation_mem_shiftedIdeal line 454
  41. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolDilation line 462
  42. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolDilation_map line 478
  43. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolCoefficient_dilation line 483
  44. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolDilation_one line 494
  45. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolDilation_mul line 500
  46. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolHom_dilation line 507
  47. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialFiltration_layer line 528
  48. abbrev OAI.Erdos3.NilpotentLieFiltration.SymbolBasisIndex line 557
  49. def OAI.Erdos3.NilpotentLieFiltration.symbolSurvivorEquiv line 560
  50. def OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis line 578
  51. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_apply line 585
  52. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_repr_map line 591
  53. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedPolynomialIdeal_eq_span_monomialBasis line 615
  54. abbrev OAI.Erdos3.NilpotentLieFiltration.ShiftedMonomialIndex line 634
  55. def OAI.Erdos3.NilpotentLieFiltration.shiftedMonomialBasis line 638
  56. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedMonomialBasis_coe line 645
  57. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedMonomialBasis_repr line 650
  58. theorem OAI.Erdos3.NilpotentLieFiltration.shiftedPolynomial_next_eq_span line 656