OAI/Analysis/CircleDomains/Modulus/PathCostReference.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite reference measure for modulus: physical area, squared countable-point weights, and the weighted tuple tori. Its square integral is exactly the sum of the three corresponding energies.

  1. def OAI.CircleDomainRigidity.atomicReference line 20
  2. theorem OAI.CircleDomainRigidity.atomicReference_univ line 24
  3. theorem OAI.CircleDomainRigidity.lintegral_atomicReference line 30
  4. def OAI.CircleDomainRigidity.pathCostReference line 35
  5. theorem OAI.CircleDomainRigidity.pathCostReference_univ line 39
  6. theorem OAI.CircleDomainRigidity.finite_pathCostReference line 47
  7. theorem OAI.CircleDomainRigidity.lintegral_pathCostReference line 55
  8. theorem OAI.CircleDomainRigidity.squareIntegral_pathCostReference line 65
  9. theorem OAI.CircleDomainRigidity.null_tupleExclusions_of_reference_energy line 73