OAI/Analysis/Crouzeix/BoundaryKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Boundary Kernel.

  1. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.closed_unit_subset_reciprocalDisk line 21
  2. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.circle_inverse_mem line 27
  3. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCorrection line 30
  4. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel line 39
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.circle_real_quotient line 44
  6. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_off_diagonal line 56
  7. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_nonnegative line 73
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCorrection_integral_right line 85
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCorrection_integral_left line 92
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_integral_right line 99
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_integral_left line 111
  12. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryOperator line 123
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.norm_boundaryOperator_le line 127