OAI/Analysis/CircleDomains/Sobolev/WeightedSobolevTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Preserve a common pointwise derivative bound when transporting rectangle weak derivatives into the Euclidean Sobolev witness.

  1. theorem OAI.CircleDomainRigidity.exists_bounded_rectangle_sobolev_witness line 13