OAI/Analysis/CircleDomains/Topology/PeriodicBoundaryPairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A boundary pairing defined for continuous lifts is stable under uniform perturbations of the same period. For smooth lifts it is the ordinary boundary integral, by integration by parts.

  1. def OAI.CircleDomainRigidity.liftedBoundaryPairing line 15
  2. theorem OAI.CircleDomainRigidity.liftedBoundaryPairing_eq_integral line 18
  3. theorem OAI.CircleDomainRigidity.liftedBoundaryPairing_stability line 27