OAI/Analysis/CircleDomains/Sobolev/BoundedEnergyWeakClosure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Almost everywhere convergence of bounded continuous scalars and a uniform global Dirichlet budget produce a global weak gradient. Compact support is needed only for the test functions, not for a common support of the approximating scalars.

  1. theorem OAI.CircleDomainRigidity.weakPartial_of_bounded_ae_pointwise_weak_limit line 18
  2. theorem OAI.CircleDomainRigidity.exists_bounded_energy_weak_gradient line 49
  3. theorem OAI.CircleDomainRigidity.exists_bounded_energy_weak_closure line 108