OAI/Analysis/CircleDomains/Rigidity/ConductivityContraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The real-linear conductivity equation is solved in the actual complex L2 space by contraction. The operator parameter is only the contraction property of the Beurling operator; the fixed point and its support are constructed here.

  1. abbrev OAI.CircleDomainRigidity.ComplexPlaneL2 line 18
  2. def OAI.CircleDomainRigidity.conductivityProduct line 20
  3. theorem OAI.CircleDomainRigidity.conductivityProduct_coe line 29
  4. def OAI.CircleDomainRigidity.conductivityConj line 35
  5. theorem OAI.CircleDomainRigidity.conductivityConj_coe line 38
  6. def OAI.CircleDomainRigidity.conductivitySource line 42
  7. theorem OAI.CircleDomainRigidity.conductivitySource_coe line 45
  8. def OAI.CircleDomainRigidity.conductivityIteration line 49
  9. theorem OAI.CircleDomainRigidity.conductivityIteration_coe line 55
  10. theorem OAI.CircleDomainRigidity.conductivityIteration_contracting line 69
  11. theorem OAI.CircleDomainRigidity.exists_conductivity_density line 92
  12. theorem OAI.CircleDomainRigidity.conductivity_density_support line 115