OAI/Analysis/Crouzeix/DiskHolomorphic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Disk Holomorphic.

  1. def OAI.CrouzeixHilbert.densityIntegralCLM line 30
  2. theorem OAI.CrouzeixHilbert.densityIntegralCLM_apply line 57
  3. theorem OAI.CrouzeixHilbert.Disk.integral_matrixHolomorphic line 67
  4. theorem OAI.CrouzeixHilbert.Disk.holomorphic_bound_spectralRadius_lt_one line 135