OAI/Analysis/CircleDomains/Topology/IndicatorPathPenalty.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A constant density on an open region pays the length of a rectifiable passage that lies in that region apart from its last endpoint.

  1. theorem OAI.CircleDomainRigidity.indicator_occupation_of_interior_passage line 17
  2. theorem OAI.CircleDomainRigidity.indicator_occupation_pays_endpoint_distance line 30