OAI/Combinatorics/Progressions/Estimates/ComparisonAmbient.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeLayerMap line 16
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeLayerMap_tmul line 21
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeLayerMap_zero line 29
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeLayerMap_mem line 39
  5. def OAI.Erdos3.MultidegreeLieFiltration.realBlockCoefficient line 66
  6. def OAI.Erdos3.MultidegreeLieFiltration.realPolarizedCoefficient line 70
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.realPolarizedCoefficient_zero line 75
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.realPolarizedCoefficient_mem line 79
  9. def OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeInclusion line 99
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeInclusion_injective line 103
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeInclusion_layerMap line 106
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.realSquarefreeInclusion_permute line 118
  13. theorem OAI.Erdos3.realSquarefreePermute_monomial line 139
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.realPolarizedCoefficient_inclusion line 153
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.realPolarizedCoefficient_permute line 162
  16. def OAI.Erdos3.MultidegreeLieFiltration.comparisonSubalgebra line 190
  17. def OAI.Erdos3.MultidegreeLieFiltration.comparisonFiltration line 195
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_comparisonFiltration_layer line 213
  19. def OAI.Erdos3.MultidegreeLieFiltration.comparisonFirst line 216
  20. def OAI.Erdos3.MultidegreeLieFiltration.comparisonSecond line 219
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonFirst_mem_layer line 222
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonSecond_mem_layer line 226
  23. def OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLift line 244
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLift_first line 256
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLift_second line 259
  26. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLift_mem_degree line 262
  27. def OAI.Erdos3.MultidegreeLieFiltration.comparisonFiltrationLayerEquiv line 277
  28. def OAI.Erdos3.MultidegreeLieFiltration.realComparisonGraphLift line 299
  29. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonGraphLift_tmul line 304
  30. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonGraphLift_first line 310
  31. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonGraphLift_second line 320
  32. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonGraphLift_mem_degree line 333
  33. def OAI.Erdos3.MultidegreeLieFiltration.realComparisonCoefficient line 359
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonCoefficient_zero_index line 367
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonCoefficient_zero_value line 371
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonCoefficient_mem line 381
  37. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionProductMap_point_logHeight line 411
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonFirst_real_mem_layer line 439
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonSecond_real_mem_layer line 445
  40. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonAmbient line 464
  41. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonToAmbient line 470
  42. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonToAmbient_injective line 474
  43. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonAmbient_geometry line 479
  44. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonAmbient_point_logHeight line 496