OAI/Analysis/CircleDomains/Sobolev/LocalWeakGradientEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Locality identifies the actual Sobolev gradient and its energy. A zero exterior contributes no energy; the intervening circle is null.

  1. theorem OAI.CircleDomainRigidity.weakGradient_eq_on_subset line 13
  2. theorem OAI.CircleDomainRigidity.weakGradient_zero_on_subset line 29
  3. theorem OAI.CircleDomainRigidity.localized_weakGradient_energy line 42