OAI/Combinatorics/Progressions/Estimates/CurrentLayerPreservation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.lie_mem_invariant_sup_layer_of_degree line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.correction_adjoint_sub_current_bracket_mem line 28
  3. theorem OAI.Erdos3.NilpotentLieFiltration.correction_inverse_adjoint_sub_current_bracket_mem line 46
  4. theorem OAI.Erdos3.NilpotentLieFiltration.correction_removal_coord_sub_mem_layer line 56
  5. theorem OAI.Erdos3.NilpotentLieFiltration.correction_removal_preserves_lower_layers line 77
  6. theorem OAI.Erdos3.NilpotentLieFiltration.correction_removal_preserves_mod_invariant line 86
  7. theorem OAI.Erdos3.NilpotentLieFiltration.removal_adjoint_relation line 109
  8. theorem OAI.Erdos3.NilpotentLieFiltration.current_layer_normalization line 114
  9. theorem OAI.Erdos3.NilpotentLieFiltration.logDerivative_current_layer_of_lower_brackets line 183
  10. theorem OAI.Erdos3.NilpotentLieFiltration.adjoint_sub_mem_invariant_next_layer line 195
  11. theorem OAI.Erdos3.NilpotentLieFiltration.current_layer_derivative_system line 206
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_mem_layer line 239
  13. theorem OAI.Erdos3.NilpotentLieFiltration.real_corrected_middle_mem_next_layer line 250
  14. theorem OAI.Erdos3.NilpotentLieFiltration.real_quotient_mem_subgroup_iff line 287
  15. theorem OAI.Erdos3.NilpotentLieFiltration.real_corrected_middle_quotient_mem_next_layer line 303
  16. theorem OAI.Erdos3.NilpotentLieFiltration.simultaneous_real_grade_correction line 328
  17. theorem OAI.Erdos3.NilpotentLieFiltration.real_correction_removal_current_grade line 374
  18. theorem OAI.Erdos3.NilpotentLieFiltration.real_polynomial_correction_removal line 407
  19. theorem OAI.Erdos3.basisBelowProjection_succ line 441
  20. theorem OAI.Erdos3.NilpotentLieFiltration.real_current_bracket_remainder line 458
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_mem_of_mem_sup_next line 479
  22. theorem OAI.Erdos3.NilpotentLieFiltration.real_mem_of_homogeneous_mem_sup_next line 488
  23. theorem OAI.Erdos3.NilpotentLieFiltration.real_correction_preserves_grades_below line 496
  24. theorem OAI.Erdos3.NilpotentLieFiltration.real_correction_current_grade line 510
  25. theorem OAI.Erdos3.NilpotentLieFiltration.adjoint_correction_sub_mem_layer line 539
  26. theorem OAI.Erdos3.NilpotentLieFiltration.current_layer_correction_preserves_lifts line 550
  27. theorem OAI.Erdos3.NilpotentLieFiltration.derivative_removal_preserves_layer_mod_invariant line 569
  28. theorem OAI.Erdos3.NilpotentLieFiltration.real_pure_correction_preserves_log_conditions line 597