OAI/Analysis/NumericalRange/CompleteResolvent.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.fourier_nat_pow line 22
  2. lemma OAI.CompleteCrouzeix.integrable_polynomial_diskDensity line 30
  3. lemma OAI.CompleteCrouzeix.polynomial_diskDensity line 37
  4. lemma OAI.CompleteCrouzeix.stable_spectrum_norm_lt_one line 59
  5. lemma OAI.CompleteCrouzeix.analytic_diskDensity line 67
  6. def OAI.CompleteCrouzeix.completeAnalyticEval line 119

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:116 (same declaration text).

  7. lemma OAI.CompleteCrouzeix.continuous_analytic_circle line 123
  8. theorem OAI.CompleteCrouzeix.complete_analytic_disk_representation line 132
  9. theorem OAI.CompleteCrouzeix.stable_complete_analytic_disk_bound line 152
  10. lemma OAI.CompleteCrouzeix.primaryEval_add line 174
  11. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_const line 187
  12. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_id line 192
  13. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_add line 196
  14. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_mul line 205
  15. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_sum line 214
  16. lemma OAI.CompleteCrouzeix.completeAnalyticEval_const line 226
  17. lemma OAI.CompleteCrouzeix.completeAnalyticEval_add line 235
  18. lemma OAI.CompleteCrouzeix.completeAnalyticEval_mul line 247
  19. lemma OAI.CompleteCrouzeix.completeAnalyticEval_zsmul line 262
  20. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_eventuallyEq line 279
  21. lemma OAI.CompleteCrouzeix.completeAnalyticEval_eqOn line 286
  22. lemma OAI.CompleteCrouzeix.matrixAnalyticEval_sub line 299
  23. lemma OAI.CompleteCrouzeix.completeAnalyticEval_sub line 308
  24. lemma OAI.CompleteCrouzeix.matrix_entry_analytic line 320
  25. lemma OAI.CompleteCrouzeix.scalar_matrix_inverse_analytic line 326
  26. lemma OAI.CompleteCrouzeix.resolvent_disk_analytic line 335
  27. lemma OAI.CompleteCrouzeix.complete_resolvent_inverse line 344
  28. lemma OAI.CompleteCrouzeix.complete_resolvent_inverse_of_isUnit line 371