OAI/Analysis/CircleDomains/Reflection/SemidiskBarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The explicit positive harmonic barrier in an upper half disk. Its poles lie at the two endpoints of the diameter.

  1. def OAI.CircleDomainRigidity.semidiskBarrier line 12
  2. lemma OAI.CircleDomainRigidity.semidiskBarrier_den_ne_zero line 14
  3. lemma OAI.CircleDomainRigidity.differentiableAt_semidiskBarrier line 24
  4. lemma OAI.CircleDomainRigidity.semidiskBarrier_im line 30
  5. lemma OAI.CircleDomainRigidity.semidiskBarrier_im_nonneg line 36
  6. lemma OAI.CircleDomainRigidity.semidiskBarrier_im_on_arc line 42
  7. lemma OAI.CircleDomainRigidity.semidiskBarrier_im_ge_one_on_arc line 67
  8. lemma OAI.CircleDomainRigidity.semidiskBarrier_im_le line 73