OAI/Analysis/CircleDomains/Modulus/WeightedCurveLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The arclength identity as a measure identity and its weighted version.

  1. def OAI.CircleDomainRigidity.curveOnSet line 14
  2. lemma OAI.CircleDomainRigidity.curve_length_map_measure line 18
  3. lemma OAI.CircleDomainRigidity.weighted_curve_length line 46