OAI/Combinatorics/Progressions/Estimates/ExtractedInitialState.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fastCoefficient_rational_removal_grid line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_initial_remainder line 101
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_mem_second line 122
  4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fastCoefficient_slow_removal_bound line 140
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realFast_derivative_removal_controlled line 237
  6. def OAI.Erdos3.NilpotentLieFiltration.nativeInitialFormalState line 306
  7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_of_quotient_section line 433
  8. theorem OAI.Erdos3.NilpotentLieFiltration.fastCoefficientSection_budget line 520
  9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_of_normalized_quotient line 551
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_after_removal line 654
  11. def OAI.Erdos3.NilpotentLieFiltration.ControlledInitialRemovalSpec line 745
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_initialFormalState_after_removal line 806
  13. def OAI.Erdos3.NilpotentLieFiltration.HorizontalInitialStateSpec line 891
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_of_horizontal_data line 936
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_horizontal_initialState_bound line 1002
  16. def OAI.Erdos3.NilpotentLieFiltration.AbsorbedInitialStateSpec line 1051
  17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_after_absorption line 1102
  18. theorem OAI.Erdos3.NilpotentLieFiltration.exists_absorbed_initialState_bound line 1174
  19. def OAI.Erdos3.NilpotentLieFiltration.ExtractedInitialStateSpec line 1222
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_from_extraction line 1269
  21. theorem OAI.Erdos3.NilpotentLieFiltration.exists_extracted_initialState_bound line 1337