OAI/Analysis/CircleDomains/Sobolev/ExteriorDerivativeMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact angular mean of the derivative of a principal exterior map. Inversion turns the derivative into a holomorphic disk function with value one at its center. No area inequality is used.

  1. lemma OAI.CircleDomainRigidity.circleAverage_comp_inv line 14
  2. lemma OAI.CircleDomainRigidity.invertedPrincipalRemainder_analyticOnNhd line 28
  3. def OAI.CircleDomainRigidity.invertedPrincipalDerivative line 50
  4. lemma OAI.CircleDomainRigidity.invertedPrincipalDerivative_zero line 53
  5. lemma OAI.CircleDomainRigidity.invertedPrincipalDerivative_eq line 56
  6. lemma OAI.CircleDomainRigidity.exterior_derivative_circleAverage line 71