OAI/Combinatorics/Progressions/Polynomial/PositivePolynomialVectorOrbit.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMonomial line 17
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMonomial_coe line 31
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMonomial_mem_layer line 34
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMonomial_evaluation line 41
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMap_monomial line 60
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialMonomial_mem_layer line 80
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_realPositivePolynomial_component line 90
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialTensor_mem_layer line 127
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_realPositivePolynomial_preimage_layer line 152
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialTensor_surjective line 172
  11. def OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialEquiv line 179
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialEquiv_apply line 184
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialEquiv_mem_layer line 187
  14. def OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialOrbitTransport line 211
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialOrbitTransport_eval line 225
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.realPositivePolynomialOrbitTransport_zero line 238
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_realPositivePolynomial_orbit line 258
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownset_projection_height line 300
  19. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialQuotientProductModel line 327
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialQuotientProductModel_geometry line 332
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialQuotientProductModel_map_height line 341
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialQuotientProductModel_lattice_cover line 349
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialQuotientProductModel_map_injective line 361
  24. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetOrbit line 380
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetOrbit_eval line 386
  26. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetOrbit_zero line 395
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialProductProjection_mk line 413
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialProductProjection_orbit line 426
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_positivePolynomial_product_reconstruction line 449
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomial_factor_error_of_lift line 532
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomial_vector_error_of_lift line 575