OAI/Analysis/CircleDomains/Transfer/ShrinkingRealModels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Vanishing transfer errors and shrinking physical marked neighborhoods.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.modelError line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.modelError_pos line 18
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.modelError_tendsto line 22
  4. def OAI.CircleDomainRigidity.FiniteTransfer.markedNeighborhoods line 27
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.markedNeighborhoods_nhds line 30
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.markedNeighborhoods_shrink line 34
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_shrinking_real_model_exhaustion line 41
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_marked_cap_in_nhds line 55