OAI/Analysis/NumericalRange/OptimalExtremal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.pos_trace_zero_mul line 26
  2. lemma OAI.CompleteCrouzeix.pos_trace_zero_mul_reverse line 48
  3. lemma OAI.CompleteCrouzeix.upper_slack_support line 53
  4. lemma OAI.CompleteCrouzeix.lower_slack_support line 61
  5. lemma OAI.CompleteCrouzeix.endpoint_support_factor line 67
  6. lemma OAI.CompleteCrouzeix.sqrt_endpoint_support line 75
  7. lemma OAI.CompleteCrouzeix.separated_endpoint_orthogonal line 88
  8. theorem OAI.CompleteCrouzeix.exists_optimal_metric_and_dual line 107
  9. theorem OAI.CompleteCrouzeix.endpoint_dual_factors line 127
  10. lemma OAI.CompleteCrouzeix.metric_sqrt_isUnit line 171
  11. theorem OAI.CompleteCrouzeix.metric_similarity_contraction line 176
  12. lemma OAI.CompleteCrouzeix.endpoint_congruence line 202
  13. lemma OAI.CompleteCrouzeix.normalized_dual_balance line 211
  14. lemma OAI.CompleteCrouzeix.spectrum_matrix_similarity line 237
  15. lemma OAI.CompleteCrouzeix.vectorize_norm_one_of_trace line 244
  16. theorem OAI.CompleteCrouzeix.exists_optimal_analytic_extremal line 254