OAI/Analysis/CircleDomains/Reflection/SemidiskDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The boundary barrier and Schwarz estimate give a uniform derivative bound on a smaller half disk, hence a genuine Lipschitz extension route.

  1. lemma OAI.CircleDomainRigidity.semidisk_derivative_bound line 14
  2. lemma OAI.CircleDomainRigidity.semidisk_lipschitz line 45