OAI/Analysis/CircleDomains/Topology/RoundCollarLifts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual zero-period real lift on a target collar is the source branch composed with the inverse finite model. Its oscillation follows from the terminal assignment, not from a boundary extension.

  1. theorem OAI.CircleDomainRigidity.unitCircleParam_one_eq_zero line 17
  2. theorem OAI.CircleDomainRigidity.unitCircleParam_mem_round_exterior line 21
  3. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.round_collar_mapsTo line 38
  4. def OAI.CircleDomainRigidity.roundCollarRealLift line 54
  5. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.exists_round_collar_lifts line 57