OAI/Analysis/CircleDomains/Topology/ReparametrizedBoundaryPairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The positive boundary identity in a physical boundary parameter. The increasing angle change is only a homeomorphism; it is not differentiated.

  1. theorem OAI.CircleDomainRigidity.integral_single_reparametrized_boundary_index line 15
  2. theorem OAI.CircleDomainRigidity.integrable_weighted_reparametrized_boundary_index line 65
  3. theorem OAI.CircleDomainRigidity.liftedBoundaryPairing_reparametrized_boundaryIndexMean line 96