OAI/Analysis/CircleDomains/Reflection/SemidiskBoundaryEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear decay of the imaginary part at a straight boundary. Only the imaginary trace is prescribed; no complex boundary value is assumed.

  1. lemma OAI.CircleDomainRigidity.imaginary_part_le_semidisk_barrier line 12
  2. lemma OAI.CircleDomainRigidity.imaginary_part_linear_boundary_bound line 61