OAI/Analysis/PathSelection/RootLimits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Clock scalar limits and limits of monic roots.

  1. lemma OAI.DegeneratingTrees.Clock.LogMonomial.trichotomy line 16
  2. lemma OAI.DegeneratingTrees.Clock.ClockGerm.scalar_limits line 37
  3. lemma OAI.DegeneratingTrees.Clock.clockEvaluation_limits line 61
  4. theorem OAI.DegeneratingTrees.Clock.clockField_isAlgClosed line 67
  5. lemma OAI.DegeneratingTrees.Clock.clockEvaluation_reflected line 72
  6. theorem OAI.DegeneratingTrees.Clock.clockRealField_isRealClosed line 80
  7. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_sum line 100
  8. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_add line 105
  9. lemma OAI.DegeneratingTrees.ScalarEvaluation.monic_root_limit line 110
  10. theorem OAI.DegeneratingTrees.Clock.clock_monic_root_limit line 164
  11. theorem OAI.DegeneratingTrees.Clock.clock_exists_monic_root_limit line 173