OAI/Analysis/CircleDomains/Modulus/IntervalChartCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted cost of a chart interval, bounded by the ordinary line integral of the pulled-back density. Parameter speed cancels exactly.

  1. def OAI.CircleDomainRigidity.realRectifiableInterval line 16
  2. theorem OAI.CircleDomainRigidity.realRectifiableInterval_occupation_le line 19
  3. theorem OAI.CircleDomainRigidity.intervalChartPath_cost_le line 34