OAI/Analysis/CircleDomains/Sobolev/LipschitzMappedCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted physical cost under a Lipschitz change of ambient metric.

  1. theorem OAI.CircleDomainRigidity.lipschitzMappedPath_cost_le line 17
  2. theorem OAI.CircleDomainRigidity.lipschitzMappedPath_cost_lt_top line 28