OAI/Analysis/CircleDomains/Topology/BoundaryIndexPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The boundary pairing of the actual averaged index is integration against the starting-angle law. This proves the weak boundary identity used when a smooth inner contour approaches the original boundary.

  1. theorem OAI.CircleDomainRigidity.integral_single_boundary_index line 17
  2. theorem OAI.CircleDomainRigidity.integrable_weighted_boundary_index line 56
  3. theorem OAI.CircleDomainRigidity.integral_weighted_boundaryIndexMean line 81
  4. theorem OAI.CircleDomainRigidity.liftedBoundaryPairing_boundaryIndexMean line 106