OAI/Combinatorics/Progressions/Estimates/QuotientInducedMark.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.lieQuotientDescend line 11
  2. theorem OAI.Erdos3.lieQuotientDescend_mk line 19
  3. def OAI.Erdos3.NilpotentLieFiltration.quotientLie line 34
  4. theorem OAI.Erdos3.NilpotentLieFiltration.quotientLie_mem line 49
  5. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_quotientLie line 53
  6. def OAI.Erdos3.NilpotentLieFiltration.quotientTop line 60
  7. def OAI.Erdos3.NilpotentLieFiltration.quotientStepHom line 78
  8. theorem OAI.Erdos3.NilpotentLieFiltration.quotientStepHom_coord line 81
  9. theorem OAI.Erdos3.NilpotentLieFiltration.quotientStepHom_surjective line 84
  10. theorem OAI.Erdos3.NilpotentLieFiltration.quotientStepHom_ker line 87
  11. theorem OAI.Erdos3.NilpotentLieFiltration.quotientStepHom_eq_changeStep line 97
  12. def OAI.Erdos3.NilpotentLieFiltration.quotientStepEquiv line 104
  13. def OAI.Erdos3.NilpotentLieFiltration.quotientPolynomialOrbit line 108
  14. theorem OAI.Erdos3.NilpotentLieFiltration.quotientPolynomialOrbit_log line 113
  15. theorem OAI.Erdos3.NilpotentLieFiltration.quotientPolynomialOrbit_eval line 117
  16. def OAI.Erdos3.MultidegreeLieFiltration.quotientMultidegree line 138
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.quotientMultidegree_mem line 158
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.quotientMultidegree_layer_eq_bot line 162
  19. theorem OAI.Erdos3.MultidegreeLieFiltration.quotientMultidegree_adapted line 168
  20. def OAI.Erdos3.NilpotentLieFiltration.realQuotientStepHom line 190
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientStepHom_surjective line 195
  22. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realQuotientStepHom_ker line 200
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientStepHom_lattice line 212
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientStep_mem_layer line 218
  25. def OAI.Erdos3.NilpotentLieFiltration.realQuotientPolynomialOrbit line 232
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientPolynomialOrbit_eval line 239
  27. def OAI.Erdos3.quotientInducedMark line 264
  28. theorem OAI.Erdos3.quotientInducedMark_mk line 267
  29. theorem OAI.Erdos3.quotientInducedMark_comp line 270
  30. theorem OAI.Erdos3.quotientInducedMark_real_mk line 275
  31. theorem OAI.Erdos3.quotientInducedMark_real_comp line 282
  32. theorem OAI.Erdos3.NilpotentLieFiltration.quotientInducedMark_mem_layer line 292
  33. theorem OAI.Erdos3.NilpotentLieFiltration.quotientInducedMark_realQuotientStepHom line 301