OAI/Combinatorics/Progressions/Dynamics/UniformFormalInductionIteration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.formalIterationBudget line 9
  2. theorem OAI.Erdos3.formalIterationBudget_zero line 13
  3. theorem OAI.Erdos3.formalIterationBudget_succ line 15
  4. theorem OAI.Erdos3.formalIterationBudget_nonneg line 18
  5. theorem OAI.Erdos3.formalIterationBudget_monotone line 24
  6. theorem OAI.Erdos3.formalIterationBudget_ge line 36
  7. def OAI.Erdos3.formalIterationPolynomial line 39
  8. theorem OAI.Erdos3.formalIterationPolynomial_eval line 43
  9. theorem OAI.Erdos3.exists_formal_iteration_uniform_budget line 49
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_formal_induction_iteration line 71
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_uniform_formal_induction_iteration line 161