OAI/Analysis/Crouzeix/SeparateHolomorphic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separate Holomorphic.

  1. lemma OAI.CrouzeixHilbert.differentiableOn_parameter_intervalIntegral_pos line 16
  2. lemma OAI.CrouzeixHilbert.deriv_eq_circle_parameter line 35
  3. theorem OAI.CrouzeixHilbert.continuousOn_first_derivative line 59
  4. theorem OAI.CrouzeixHilbert.differentiableOn_second_first_derivative line 118