OAI/Analysis/CircleDomains/Reflection/PrincipalReflectionSourceError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reflection invariance and strong principal-derivative convergence give an actual globally L2-small source error, with the exact conjugacy formula on any prescribed finite-measure reflected source set.

  1. lemma OAI.CircleDomainRigidity.planeL2_norm_star line 16
  2. lemma OAI.CircleDomainRigidity.planeL2_star_tendsto_zero line 21
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflection_source_error line 30