OAI/Analysis/CircleDomains/Sobolev/SmoothWeakGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identify the weak gradient of an actual local Sobolev witness with its classical differential when the represented scalar is smooth.

  1. def OAI.CircleDomainRigidity.localSobolevChangeDomain line 13
  2. theorem OAI.CircleDomainRigidity.smooth_weak_gradient_ae line 21