OAI/Analysis/Crouzeix/FiniteCompression.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact polynomial compression on spans of finitely many operator iterates.

  1. def OAI.CrouzeixHilbert.compression line 20
  2. theorem OAI.CrouzeixHilbert.compression_inner line 23
  3. theorem OAI.CrouzeixHilbert.numericalRange_compression_subset line 28
  4. theorem OAI.CrouzeixHilbert.coe_compression_apply line 33
  5. theorem OAI.CrouzeixHilbert.coe_compression_pow line 39
  6. def OAI.CrouzeixHilbert.iterateSpan line 53
  7. instance OAI.CrouzeixHilbert.iterateSpanFiniteDimensional line 56
  8. theorem OAI.CrouzeixHilbert.iterate_mem_iterateSpan line 60
  9. theorem OAI.CrouzeixHilbert.mem_iterateSpan line 65
  10. def OAI.CrouzeixHilbert.amplificationInclusion line 69
  11. theorem OAI.CrouzeixHilbert.norm_amplificationInclusion line 73
  12. theorem OAI.CrouzeixHilbert.amplificationInclusion_tmul line 87
  13. theorem OAI.CrouzeixHilbert.polynomialEval_tmul line 93
  14. theorem OAI.CrouzeixHilbert.polynomial_compression_tmul line 101
  15. theorem OAI.CrouzeixHilbert.completion_coe_finsetSum line 112
  16. theorem OAI.CrouzeixHilbert.polynomial_bound_of_finite_compressions line 118
  17. theorem OAI.CrouzeixHilbert.polynomial_inequality_of_finite_compressions line 154