OAI/Analysis/CircleDomains/Transfer/BoundedScalarFillings.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable fillings on the whole plane, equal to the clipped transferred scalar in the domain and constant on each actual round hole.

  1. def OAI.CircleDomainRigidity.clipScalar line 13
  2. theorem OAI.CircleDomainRigidity.clipScalar_lipschitz line 15
  3. theorem OAI.CircleDomainRigidity.clipScalar_mem line 18
  4. theorem OAI.CircleDomainRigidity.clipScalar_eq line 21
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.transferred_continuousOn line 31
  6. def OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled line 41
  7. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_on_domain line 46
  8. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_on_hole line 58
  9. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_mem line 69
  10. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_measurable line 81
  11. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_memLp line 98