OAI/Analysis/CircleDomains/Transfer/ScalarHoleFillings.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Constant values for the actual finite target holes. Every finite cluster value differs from the chosen fill by at most the original terminal oscillation.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.exists_scalar_fill_values line 14
  2. structure OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling line 55
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.exists_hole_filling line 72
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.radius_sq_bound line 82
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_hole_cost_bound line 97