OAI/Analysis/CircleDomains/Sobolev/SmoothLocalWeakDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A global distributional derivative agrees with the ordinary derivative on any open set where its scalar has a smooth representative.

  1. theorem OAI.CircleDomainRigidity.integrable_mul_of_continuousOn_tsupport line 13
  2. theorem OAI.CircleDomainRigidity.integral_mul_fderiv_of_contDiffOn line 20
  3. theorem OAI.CircleDomainRigidity.weak_field_eq_smooth_derivative line 37