OAI/Analysis/Crouzeix/Iteration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Iteration.

  1. lemma OAI.CrouzeixHilbert.Realization.norm_pow_contraction line 21
  2. theorem OAI.CrouzeixHilbert.Realization.summable_two_sided_series line 24
  3. theorem OAI.CrouzeixHilbert.Realization.tendsto_two_sided_remainder line 33
  4. theorem OAI.CrouzeixHilbert.Realization.finite_recurrence line 45
  5. theorem OAI.CrouzeixHilbert.Realization.eq_two_sided_series line 57
  6. theorem OAI.CrouzeixHilbert.Realization.eq_realization_series line 65