OAI/Analysis/CircleDomains/Reflection/PrincipalReflectionDefect.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual mollified coefficients' reflection defects are uniformly bounded and tend almost everywhere to zero. The smooth conjugate's exact antiholomorphic derivative is expressed using this defect.

  1. def OAI.CircleDomainRigidity.AnalyticReflectionData.reflectionDefect line 19
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectionDefect_measurable line 25
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectionDefect_bound line 33
  4. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectionDefect_tendsto line 41
  5. def OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedApproximation line 55
  6. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedApproximation_error line 60