OAI/Combinatorics/Progressions/Estimates/ReindexedFastCoefficientSection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_grid line 18
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_bound line 31
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realHorizontalSection_constant_coordinate line 42
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realHorizontalSection_nonconstant_coordinate line 52
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realHorizontalSection_slow_bound line 60
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realHorizontalSection_grid line 74
  7. theorem OAI.Erdos3.NilpotentLieFiltration.FirstCoefficientSlowBound.mono line 107
  8. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientRepresentative line 123
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientRepresentative_mk line 127
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientRepresentative_horizontal line 134
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientRepresentative_bound line 143
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientRepresentative_grid line 154
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal_section_norm_bound line 184
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientHorizontal_section_grid line 209
  15. def OAI.Erdos3.reindexCoordinateSection line 232
  16. theorem OAI.Erdos3.reindexCoordinateSection_right_inverse line 238
  17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_reindexed_fast_coefficient_section line 252