OAI/Analysis/StructuralCrouzeix/SharedDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.CompleteCrouzeix.AdmissibleDomain.positiveDensity_analytic_bound_unit line 16
  2. theorem OAI.CompleteCrouzeix.AdmissibleDomain.positiveDensity_analytic_bound line 38
  3. theorem OAI.CompleteCrouzeix.AdmissibleDomain.complete_analytic_similarity_bound_nonneg line 81
  4. theorem OAI.CompleteCrouzeix.AdmissibleDomain.common_positiveDensity_for_metric line 110