OAI/Combinatorics/Progressions/Estimates/ReplicatedLieAction.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.ReplicatedIndex line 19
  2. theorem OAI.Erdos3.replicatedIndex_card line 21
  3. def OAI.Erdos3.replicatedPermutation line 25
  4. theorem OAI.Erdos3.replicatedPermutation_block line 28
  5. theorem OAI.Erdos3.replicated_blockDegree_apply line 31
  6. theorem OAI.Erdos3.replicated_blockDegree_le line 42
  7. abbrev OAI.Erdos3.ReplicatedPermutation line 63
  8. instance OAI.Erdos3.replicatedPermutationFintype line 65
  9. theorem OAI.Erdos3.replicatedPermutation_one line 68
  10. theorem OAI.Erdos3.replicatedPermutation_mul line 75
  11. theorem OAI.Erdos3.replicatedPermutation_injective line 82
  12. theorem OAI.Erdos3.replicatedPermutation_card_le line 91
  13. theorem OAI.Erdos3.replicated_blockDegree_full line 105
  14. def OAI.Erdos3.MultidegreeLieFiltration.replicatedTopCoefficient line 118
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedTopCoefficient_apply line 130
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedTopCoefficient_permute line 135
  17. structure OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure line 162
  18. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.ComplexityLE line 174
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.ComplexityLE.mono line 177
  20. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup line 180
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup_eq_realificationSubgroup line 182
  22. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.orbitToOrdinary line 188
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.orbitToOrdinary_eval line 196
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup_closed line 211
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup_lattice_closed_discrete line 215
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup_lattice_cocompact line 223
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.ordinary_top_eq line 243
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.realSubgroup_top line 267
  29. def OAI.Erdos3.MultidegreeLieFiltration.restrictBound line 291
  30. def OAI.Erdos3.MultidegreeLieFiltration.restrictBoundRealOrbit line 302
  31. theorem OAI.Erdos3.MultidegreeLieFiltration.restrictBoundRealOrbit_eval line 307
  32. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.restrictBound line 322
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.restrictBound_complexity line 329
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.restrictBound_orbitToOrdinary line 336
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_eq_finite line 355
  36. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.weightedLayer_span line 386
  37. structure OAI.Erdos3.NativeTwoVariableSplit line 416
  38. def OAI.Erdos3.MultidegreeLieFiltration.replicatedLiePermute line 452
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedLiePermute_one line 457
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedLiePermute_mul line 463
  41. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedLiePermute_top line 472
  42. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedLiePermute_ordinary_top line 478