OAI/Combinatorics/Progressions/Estimates/NativeProductCoefficient.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap line 16
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap_baseChange line 21
  3. theorem OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates_map line 27
  4. theorem OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates_mem line 37
  5. theorem OAI.Erdos3.DegreeRankLieFiltration.exists_controlled_horizontal_lifts line 47
  6. theorem OAI.Erdos3.real_firstProjection_mem line 99
  7. def OAI.Erdos3.DegreeRankLieFiltration.realFourLayerComponent line 111
  8. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourLayerComponent_coe line 118
  9. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourLayerComponent_horizontal line 121
  10. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourLayerComponent_norm_bound line 138
  11. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourLayerComponent_grid line 148
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap_surjective line 172
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap_ambient line 179
  14. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap_eq line 189
  15. def OAI.Erdos3.DegreeRankLieFiltration.realHorizontalRepresentative line 200
  16. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalRepresentative_zero line 205
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalMap_representative line 210
  18. def OAI.Erdos3.DegreeRankLieFiltration.realHorizontalTreeValue line 218
  19. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalTreeValue_map line 222
  20. theorem OAI.Erdos3.DegreeRankLieFiltration.realHorizontalTreeValue_zero_of_leaf line 233
  21. theorem OAI.Erdos3.DegreeRankLieFiltration.rankLayerCoefficient_tensor_coe line 253
  22. theorem OAI.Erdos3.DegreeRankLieFiltration.rankLayerCoefficient_tensor_horizontal line 264
  23. theorem OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom_eq_realHorizontalMap line 273
  24. def OAI.Erdos3.DegreeRankLieFiltration.horizontalPreimage line 307
  25. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalPreimage_le line 310
  26. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalPreimage_mono line 315
  27. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_horizontalPreimage line 319
  28. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalPreimage_coordinates line 329
  29. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_real_horizontalPreimage line 345
  30. theorem OAI.Erdos3.DegreeRankLieFiltration.native_coefficient_mem_horizontalPreimage line 359
  31. theorem OAI.Erdos3.DegreeRankLieFiltration.polynomialOrbit_coefficient_mem_rank_one line 394
  32. theorem OAI.Erdos3.DegreeRankLieFiltration.polynomialOrbit_log_mul_mod_rank_two line 401
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.orbit_log_mul_mod_rank_two line 436