OAI/Combinatorics/Progressions/Estimates/RefilteredPointwiseSplitting.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationLayer line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationLayer_antitone line 20
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationLayer_le line 23
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationLayer_lie_mem line 27
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationLayer_terminal line 32
  6. def OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltrationSubalgebra line 35
  7. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realGradedRefiltrationSubalgebra line 38
  8. def OAI.Erdos3.NilpotentLieFiltration.realGradedRefiltration line 41
  9. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realGradedRefiltration_layer line 58
  10. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realGradedRefiltrationLayer_iff line 63
  11. theorem OAI.Erdos3.NilpotentLieFiltration.real_symbol_values_iff_refiltration_coefficients line 88
  12. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_refiltration_coefficients_mem_first line 101
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_refiltered_polynomial_of_coefficients line 112
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_pointwise_refiltered_polynomial line 135
  15. theorem OAI.Erdos3.NilpotentLieFiltration.pointwise_refiltered_values_mem line 147
  16. theorem OAI.Erdos3.NilpotentLieFiltration.normalized_symbol_polynomial_values_mem_subgroup line 175
  17. theorem OAI.Erdos3.NilpotentLieFiltration.pointwise_factor_middle_refiltration line 186
  18. theorem OAI.Erdos3.NilpotentLieFiltration.exists_pointwise_polynomial_symbol_splitting line 218
  19. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_polynomial_step_drop_factors line 317
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_pointwise_refiltered_splitting line 408