OAI/Analysis/Crouzeix/MetricBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Metric Boundary.

  1. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.spectralRadius_coordinate_lt_one line 22
  2. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.minimizing_metric_sqrt_le_two line 42
  3. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.exists_conformal_contraction line 114