OAI/Analysis/CircleDomains/Sobolev/LocalWeakBarrierBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local three-term barrier bound from four actual scalar Sobolev witnesses. Measurability and joint differential integrability are derived.

  1. theorem OAI.CircleDomainRigidity.local_weak_barrier_bound line 12