OAI/Analysis/CircleDomains/Selection/ScalarBoundedRepresentative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A pointwise unit-bounded representative of the actual weak scalar, with the same global planar weak gradient.

  1. def OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.boundedRepresentative line 22
  2. def OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.planarWeakGradient line 25
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.boundedRepresentative_unit line 29
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.boundedRepresentative_ae line 32
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.boundedRepresentative_measurable line 38
  6. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.planarWeakGradient_memLp line 43
  7. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.boundedRepresentative_weak line 51
  8. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.planarWeakGradient_zero_off_image line 76