OAI/Analysis/CircleDomains/Topology/ReparametrizedBoundaryLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A positive starting-point law gives the lower bound on any sufficiently close smooth inward circuit. The boundary angle parameter need not be smooth.

  1. theorem OAI.CircleDomainRigidity.smooth_reparametrized_boundary_integral_lower_bound line 16
  2. theorem OAI.CircleDomainRigidity.exists_mean_collar_boundary_lower_bound line 64