OAI/Analysis/CircleDomains/Sobolev/PotentialWeightedSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded first-arrival potential has a local L² weak gradient on each physical rectangle. No Sobolev regularity is added as an input.

  1. theorem OAI.CircleDomainRigidity.potential_rectangle_weighted_weak_gradient line 23