OAI/Analysis/CircleDomains/Transfer/ModelFixedWorkingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Common source and image radii for the appending construction. The estimates are independent of the finite test family.

  1. theorem OAI.CircleDomainRigidity.exterior_source_mono line 11
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.fixed_working_image_bound line 19