OAI/Analysis/CircleDomains/Topology/SimpleArcToll.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An injective arc pays each boundary weight at most once. The payment is bounded by the actual atomic measure on any set containing the arc.

  1. def OAI.CircleDomainRigidity.atomicBoundaryMeasure line 17
  2. theorem OAI.CircleDomainRigidity.atomicBoundaryMeasure_apply line 20
  3. theorem OAI.CircleDomainRigidity.atomicBoundaryMeasure_null line 30
  4. theorem OAI.CircleDomainRigidity.simple_arc_boundary_toll_le line 40