OAI/Combinatorics/Progressions/Polynomial/RealCoordinatePolynomialSymbol.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.eval₂_substitute line 14
  2. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitSubstitute_realEval line 32
  3. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitRealEval_constant line 40
  4. theorem OAI.Erdos3.NilpotentLieFiltration.real_adapted_coordinate_degree line 60
  5. theorem OAI.Erdos3.NilpotentLieFiltration.real_scaled_adapted_basis_mem line 92
  6. def OAI.Erdos3.NilpotentLieFiltration.orderedSlotFactor line 98
  7. theorem OAI.Erdos3.NilpotentLieFiltration.orderedSlotFactor_realEval line 112
  8. def OAI.Erdos3.NilpotentLieFiltration.orderedSlotOrbit line 129
  9. theorem OAI.Erdos3.NilpotentLieFiltration.orderedSlotOrbit_realEval line 142
  10. theorem OAI.Erdos3.NilpotentLieFiltration.real_ofCoordinates_adapted line 178
  11. def OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit line 196
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_log line 200
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_coefficients line 204
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_coordinate line 209
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_eval_coordinates line 214
  16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_coordinate_polynomialOrbit line 223
  17. theorem OAI.Erdos3.NilpotentLieFiltration.orderedSlotOrbit_coordinate line 247
  18. def OAI.Erdos3.NilpotentLieFiltration.orderedPolynomialSlots line 274
  19. theorem OAI.Erdos3.NilpotentLieFiltration.orderedPolynomialSlots_slots line 285
  20. def OAI.Erdos3.NilpotentLieFiltration.orderedPolynomialPatch line 302
  21. theorem OAI.Erdos3.NilpotentLieFiltration.orderedPolynomialPatch_value line 313
  22. def OAI.Erdos3.NilpotentLieFiltration.realExtendedSymbolMap line 340
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_realAdaptedPolynomialMap line 344
  24. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap line 359
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap_apply line 372
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap_representative line 375
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap_surjective line 380
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap_eq_zero_iff line 385
  29. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom line 391
  30. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_coord line 395
  31. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolLift line 400
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_lift line 404
  33. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_surjective line 410
  34. theorem OAI.Erdos3.NilpotentLieFiltration.orderedPolynomialPatch_chart_value line 431
  35. theorem OAI.Erdos3.weightedHomogeneousComponent_mem_weightedSupportLE line 457
  36. theorem OAI.Erdos3.NilpotentLieFiltration.repr_coefficients_ofCoordinates line 475
  37. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_ofCoordinates line 481
  38. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_ofCoordinates_top line 504
  39. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_symbol_top line 515
  40. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_symbol_eq_of_top line 529
  41. theorem OAI.Erdos3.NilpotentLieFiltration.realCoordinatePolynomialOrbit_symbol_representative line 544