OAI/Combinatorics/Progressions/Estimates/SymbolCommonCorrections.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.bracket_mem_subalgebra_sup_layer_succ line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.bch_triple_remainder_mem_subalgebra_sup_layer line 38
  3. theorem OAI.Erdos3.NilpotentLieFiltration.outer_sum_mem_subalgebra_sup_layer line 48
  4. theorem OAI.Erdos3.NilpotentLieFiltration.outer_factors_mem_of_separation line 76
  5. theorem OAI.Erdos3.NilpotentLieFiltration.comparison_middle_identity line 103
  6. theorem OAI.Erdos3.NilpotentLieFiltration.compatible_factors_mem_of_separation line 109
  7. theorem OAI.Erdos3.NilpotentLieFiltration.outer_sum_mem_of_identity_mod_layer line 131
  8. theorem OAI.Erdos3.NilpotentLieFiltration.outer_factors_mem_mod_layer_of_separation line 147
  9. theorem OAI.Erdos3.NilpotentLieFiltration.compatible_factors_mem_mod_layer_of_separation line 181
  10. theorem OAI.Erdos3.NilpotentLieFiltration.controlled_outer_factors_mem line 210
  11. theorem OAI.Erdos3.NilpotentLieFiltration.controlled_compatible_factors_mem line 248
  12. theorem OAI.Erdos3.NilpotentLieFiltration.controlled_separation_at_layer line 284
  13. theorem OAI.Erdos3.NilpotentLieFiltration.controlled_compatible_factors_mod_layer line 315
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_comparison line 351
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotient_mem_iff line 441
  16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_comparison_mod_layer line 453
  17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_symbol_comparison line 555
  18. theorem OAI.Erdos3.NilpotentLieFiltration.symbol_current_grade_residual_mem line 638
  19. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_grade_step line 660
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_symbol_grade_corrections line 749