OAI/Analysis/StructuralCrouzeix/SharedMaximum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.CompleteCrouzeix.AdmissibleDomain.analyticRangeMaximum line 16
  2. lemma OAI.CompleteCrouzeix.AdmissibleDomain.analyticRangeMaximum_bddAbove line 20
  3. theorem OAI.CompleteCrouzeix.AdmissibleDomain.analyticRangeMaximum_attained line 25
  4. lemma OAI.CompleteCrouzeix.AdmissibleDomain.analyticRangeMaximum_nonneg line 38
  5. lemma OAI.CompleteCrouzeix.AdmissibleDomain.norm_le_analyticRangeMaximum line 45
  6. theorem OAI.CompleteCrouzeix.AdmissibleDomain.common_positiveDensity_maximum_for_metric line 50