OAI/Analysis/CircleDomains/Sobolev/StrongWeakPartialLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded pointwise convergence and strong L2 convergence of actual weak partial derivatives identify the derivative of the limit. Only the compact support of the testing function is used for the value limit.

  1. theorem OAI.CircleDomainRigidity.weakPartial_of_bounded_pointwise_strong_limit line 15