OAI/Analysis/CircleDomains/Rigidity/ScalarModelConductivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual conductivity postcomposition stays in the retained model class. Near maximality therefore bounds its first coefficient and both terms of its proved global energy identity.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.complement_compact line 23
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.conductivity_conformal line 37
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.conductivity_coefficient_le line 66
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.near_extremal_conductivity_energy line 84
  5. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_near_extremal_conductivity_family line 108