OAI/Analysis/CircleDomains/Modulus/FiniteCostChartPaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An actual interval in a chart with a Lipschitz inverse coordinate has finite weighted path cost whenever its image has finite weighted Hausdorff length.

  1. theorem OAI.CircleDomainRigidity.intervalChartPath_antilipschitz line 18
  2. theorem OAI.CircleDomainRigidity.intervalChartPath_range line 41
  3. theorem OAI.CircleDomainRigidity.intervalChartPath_cost_lt_top line 49