OAI/Analysis/CircleDomains/Transfer/RetainedTerminalGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Terminal contours retaining the prescribed core and oscillation bounds

Intersect the prescribed quotient neighborhoods with the complement of the core image before choosing terminal contours. This retains the uniform staircase estimate, confines every terminal to its prescribed neighborhood, and places the whole core in the open finite completion.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.core_subset_openCompletedRegion line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_retained_physical_terminals_with_staircase_bound line 32