OAI/Analysis/CircleDomains/Sobolev/WeakBarrierMeasurability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the actual barrier differential follows from the two scalar Sobolev witnesses and the reference differential.

  1. theorem OAI.CircleDomainRigidity.continuous_plane_covector_comp line 13
  2. theorem OAI.CircleDomainRigidity.joint_barrier_differential_measurable line 18