OAI/Analysis/CircleDomains/Rigidity/ConjugateBeltramiL2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual Beurling operator in the physical plane. Its exact L2 isometry supplies the operator previously parameterized in conductivity contraction; no second fixed-point argument is needed.

  1. def OAI.CircleDomainRigidity.complexLpToPhysical line 16
  2. def OAI.CircleDomainRigidity.physicalLpToComplex line 19
  3. def OAI.CircleDomainRigidity.physicalBeurling line 24
  4. lemma OAI.CircleDomainRigidity.physicalBeurling_norm line 28
  5. lemma OAI.CircleDomainRigidity.complexLpToPhysical_coe line 32
  6. lemma OAI.CircleDomainRigidity.physicalLpToComplex_coe line 36
  7. lemma OAI.CircleDomainRigidity.physicalLpToComplex_complexLpToPhysical line 42
  8. lemma OAI.CircleDomainRigidity.physicalLpToComplex_beurling line 51
  9. lemma OAI.CircleDomainRigidity.physicalBeurling_complex_coe line 55
  10. lemma OAI.CircleDomainRigidity.exists_actual_conductivity_density line 61