OAI/Analysis/CircleDomains/Sobolev/ExactSobolevLinePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous compact W1,2 function satisfies the coordinate-line fundamental inequality with its actual distributional gradient.

  1. lemma OAI.CircleDomainRigidity.exact_sobolev_line_payment line 13