OAI/Analysis/KadisonKastler/ContinuousMapHolomorphic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic continuous spectral functions

On a compact spectrum, a continuous family of continuous functions is holomorphic once each scalar evaluation is holomorphic. The Cauchy integral formula proves the required uniform derivative without enlarging Lean limits.

  1. theorem OAI.KadisonKastler.circleIntegral_evaluation line 23
  2. theorem OAI.KadisonKastler.continuousMap_differentiableOn_of_evaluations line 30