OAI/Combinatorics/Progressions/Polynomial/RefilteredPolynomialProjection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.mem_native_refiltration_layer line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_native_refiltered_orbit line 26
  3. theorem OAI.Erdos3.NilpotentLieFiltration.native_refiltered_orbit_real_value line 64
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realificationLieHom_mem_layer line 96
  5. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap line 101
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_log line 109
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_value line 115
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_constant line 124
  9. theorem OAI.Erdos3.NilpotentLieFiltration.refiltration_coefficients_mem_first_of_constant line 149
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_native_refiltered_orbit_of_constant line 161
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_native_refiltered_orbit_real_values_of_constant line 205
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_native_pointwise_refiltered_orbit_of_constant line 222
  13. theorem OAI.Erdos3.realificationLieHom_repr_of_coordinate line 259
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_slow line 271
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_rational line 285
  16. def OAI.Erdos3.NilpotentLieFiltration.filteredRealPolynomialSection line 317
  17. theorem OAI.Erdos3.NilpotentLieFiltration.filteredRealPolynomialSection_value line 328
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialGroupMap_filteredSection line 338
  19. theorem OAI.Erdos3.NilpotentLieFiltration.coefficient_mem_kernel_of_realPolynomialGroupMap_eq_one line 357
  20. theorem OAI.Erdos3.NilpotentLieFiltration.marked_kernel_polynomial_factors line 372
  21. theorem OAI.Erdos3.NilpotentLieFiltration.exists_model_refiltered_polynomial line 420
  22. theorem OAI.Erdos3.NilpotentLieFiltration.refiltered_polynomial_projection line 439