OAI/Combinatorics/Progressions/Estimates/PolarizedCoefficientPermutation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.polynomialOrbitOfLog line 18
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.polynomialOrbitOfLog_eval line 21
  3. def OAI.Erdos3.MultidegreeLieFiltration.constantMultidegreeOrbit line 38
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.constantMultidegreeOrbit_eval line 44
  5. def OAI.Erdos3.MultidegreeLieFiltration.normalizeMultidegreeOrbit line 50
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.normalizeMultidegreeOrbit_eval line 53
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.normalizeMultidegreeOrbit_zero line 58
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.adapted_rationalDilation line 77
  9. def OAI.Erdos3.MultidegreeLieFiltration.rationalDilationOrbit line 83
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.rationalDilationOrbit_eval line 87
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.rationalDilationOrbit_rescaled line 94
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_zero line 115
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_zero line 134
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPair_degree_comap line 141
  15. def OAI.Erdos3.MultidegreeLieFiltration.dilationPairMultidegree line 172
  16. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPair_top_group_relation line 202
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPair_projections_mem line 222
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPair_top_group_relation line 229
  19. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_splitTriple_orbit line 255
  20. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_coordinateAddition_orbit line 274
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_normalizedCoordinateAddition_orbit line 305
  22. def OAI.Erdos3.MultidegreeLieFiltration.dilationPairLog line 336
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairMultidegree_mem_layer line 344
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLog_adapted line 348
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLog_eval line 361
  26. def OAI.Erdos3.MultidegreeLieFiltration.dilationPairPolynomialOrbit line 369
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairPolynomialOrbit_eval line 375
  28. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairPolynomialOrbit_zero line 382
  29. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_integer_dilationPair_orbit line 394
  30. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_normalized_dilationPair_orbit line 410
  31. def OAI.Erdos3.MultidegreeLieFiltration.blockCoefficient line 435
  32. def OAI.Erdos3.MultidegreeLieFiltration.polarizedCoefficient line 439
  33. theorem OAI.Erdos3.MultidegreeLieFiltration.polarizedCoefficient_zero line 444
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.polarizedCoefficient_coe line 448
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.polarizedCoefficient_mem line 458
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.polarizedCoefficient_permute line 473