OAI/Analysis/StructuralCrouzeix/SimilarityMinimum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic domains, optimal similarities and matrix-valued boundary representations.

  1. lemma OAI.CompleteCrouzeix.metric_congruence_mono line 14
  2. lemma OAI.CompleteCrouzeix.metric_gram_le_norm_sq line 24
  3. theorem OAI.CompleteCrouzeix.similarity_normalized_metric_feasible line 29
  4. theorem OAI.CompleteCrouzeix.optimal_metric_sqrt_le_similarity line 72
  5. theorem OAI.CompleteCrouzeix.optimal_metric_similarity_minimal line 83
  6. theorem OAI.CompleteCrouzeix.optimal_metric_condition_eq_from_minimality line 94
  7. theorem OAI.CompleteCrouzeix.optimal_metric_similarity_exact line 103
  8. theorem OAI.CompleteCrouzeix.optimal_metric_similarity_isLeast line 115