OAI/Analysis/NumericalRange/MetricFeasibility.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.transfer_meromorphic line 28
  2. lemma OAI.CompleteCrouzeix.transfer_analytic line 44
  3. theorem OAI.CompleteCrouzeix.exists_transfer_extension line 55
  4. theorem OAI.CompleteCrouzeix.exists_analytic_extremal_from_balance line 105
  5. theorem OAI.CompleteCrouzeix.summable_norm_powers_metricSupport line 139
  6. def OAI.CompleteCrouzeix.steinTerm line 165
  7. lemma OAI.CompleteCrouzeix.summable_steinTerm line 168
  8. def OAI.CompleteCrouzeix.steinMetric line 183
  9. lemma OAI.CompleteCrouzeix.steinMetric_nonneg line 185
  10. lemma OAI.CompleteCrouzeix.steinMetric_ge_one line 190
  11. lemma OAI.CompleteCrouzeix.steinMetric_identity line 199
  12. lemma OAI.CompleteCrouzeix.steinMetric_posDef line 215
  13. def OAI.CompleteCrouzeix.MetricFeasible line 226

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

  14. lemma OAI.CompleteCrouzeix.scalarMatrix_le_iff line 229
  15. lemma OAI.CompleteCrouzeix.MetricFeasible.one_le line 243
  16. lemma OAI.CompleteCrouzeix.MetricFeasible.norm_le line 248
  17. lemma OAI.CompleteCrouzeix.steinMetric_feasible line 253
  18. lemma OAI.CompleteCrouzeix.isClosed_metricFeasible line 262
  19. theorem OAI.CompleteCrouzeix.exists_optimal_metric line 270
  20. abbrev OAI.CompleteCrouzeix.HermitianMatrix line 299
  21. def OAI.CompleteCrouzeix.fromHSL line 301
  22. def OAI.CompleteCrouzeix.hermTrace line 306
  23. lemma OAI.CompleteCrouzeix.hermTrace_realPart line 309
  24. theorem OAI.CompleteCrouzeix.exists_hermitian_trace_representative line 325
  25. lemma OAI.CompleteCrouzeix.hermTrace_symm line 347
  26. lemma OAI.CompleteCrouzeix.hermTrace_nonneg_iff line 350