OAI/Analysis/Crouzeix/ExteriorKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exterior Kernel.

  1. abbrev OAI.CrouzeixHilbert.Conformal.ExteriorCollar.reciprocalDisk line 19
  2. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.inverse_mem_reciprocalDisk line 21
  3. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.inverse_mem_parameter line 26
  4. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.deriv_laurent line 31
  5. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.dividedDenominator line 44
  6. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.continuousOn_dividedDenominator line 47
  7. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_dividedDenominator_left line 54
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_dividedDenominator_right line 60
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.dividedDenominator_eq line 67
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.dividedDenominator_diag line 75
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.dividedDenominator_ne_zero line 81
  12. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correction line 98
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.continuousOn_correction line 101
  14. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_correction_left line 110
  15. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_correction_right line 116
  16. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correction_zero_left line 127
  17. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correction_zero_right line 130
  18. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correction_eq line 134