OAI/Analysis/CircleDomains/Topology/CollarMeanLowerBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The boundary lower bound on an actual smooth inward collar. The orientation-normalized circuit is used to evaluate the mean, and its absolute integral is then returned to the original positive circuit.

  1. theorem OAI.CircleDomainRigidity.OrderedCollarLift.mean_boundary_lower_bound line 17