OAI/Analysis/HilbertCrouzeix/Compression.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HilbertCrouzeix.compression line 19

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:100 (same declaration text).

  2. theorem OAI.HilbertCrouzeix.numericalRange_compression_subset line 22
  3. theorem OAI.HilbertCrouzeix.compression_pow line 28
  4. def OAI.HilbertCrouzeix.iterateSpace line 43
  5. instance OAI.HilbertCrouzeix.iterateSpace_finiteDimensional line 46
  6. theorem OAI.HilbertCrouzeix.pow_mem_iterateSpace line 50
  7. theorem OAI.HilbertCrouzeix.mem_iterateSpace line 55
  8. def OAI.HilbertCrouzeix.completedIsometry line 59

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:102 (same declaration text).

  9. def OAI.HilbertCrouzeix.tensorInclusion line 66

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:109 (same declaration text).

  10. theorem OAI.HilbertCrouzeix.tensorInclusion_tmul line 70
  11. theorem OAI.HilbertCrouzeix.tensorOp_tmul line 78
  12. theorem OAI.HilbertCrouzeix.polynomialEval_compression_tmul line 84
  13. theorem OAI.HilbertCrouzeix.completion_coe_sum line 95
  14. theorem OAI.HilbertCrouzeix.exists_finite_compression line 100

    Distinct definitions of this name: ComparatorChallenges/HilbertCrouzeix.lean:121 (same statement text; different proof or body). Qualify references as OAI.HilbertCrouzeix.exists_finite_compression@path.

  15. theorem OAI.HilbertCrouzeix.exists_finite_compression_norm_bound line 121