OAI/Analysis/CircleDomains/Reflection/ReflectionWeightedL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The antiholomorphic Jacobian of circular reflection gives an exact L2 isometry for its weighted pullback. The one pole is a null set.

  1. def OAI.CircleDomainRigidity.roundReflectionWeight line 14
  2. lemma OAI.CircleDomainRigidity.roundReflectionWeight_measurable line 17
  3. lemma OAI.CircleDomainRigidity.roundReflection_abs_det line 21
  4. lemma OAI.CircleDomainRigidity.roundReflectionWeighted_memLp line 27
  5. lemma OAI.CircleDomainRigidity.exists_strong_reflection_pullback line 70