OAI/Analysis/CircleDomains/Rigidity/RealBeltramiL2Reduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A measurable standard coefficient built from the actual conductivity L2 density. The zero-derivative set requires no division hypothesis.

  1. lemma OAI.CircleDomainRigidity.exists_real_beltrami_l2_reduction line 13
  2. lemma OAI.CircleDomainRigidity.real_beltrami_memLp_of_compact_support line 36
  3. lemma OAI.CircleDomainRigidity.exists_compact_real_beltrami_l2_reduction line 49
  4. lemma OAI.CircleDomainRigidity.exists_bounded_compact_real_beltrami_l2_reduction line 62
  5. lemma OAI.CircleDomainRigidity.exists_complex_real_beltrami_l2_reduction line 78