OAI/Analysis/Crouzeix/CircleCoordinate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Circle Coordinate.

  1. def OAI.CrouzeixHilbert.Boundary.circleCoordinate line 16
  2. lemma OAI.CrouzeixHilbert.Boundary.norm_circleCoordinate line 18
  3. lemma OAI.CrouzeixHilbert.Boundary.circleCoordinate_ne_zero line 21
  4. lemma OAI.CrouzeixHilbert.Boundary.circleCoordinate_injective line 24
  5. lemma OAI.CrouzeixHilbert.Boundary.circleCoordinate_neg line 30
  6. lemma OAI.CrouzeixHilbert.Boundary.circleCoordinate_coe line 34
  7. lemma OAI.CrouzeixHilbert.Boundary.integral_circleCoordinate_eq_circleAverage line 42
  8. lemma OAI.CrouzeixHilbert.Boundary.integral_inverse_circleCoordinate line 50
  9. lemma OAI.CrouzeixHilbert.Boundary.integral_holomorphic_circleCoordinate line 56
  10. lemma OAI.CrouzeixHilbert.Boundary.integral_holomorphic_inverse_circleCoordinate line 65