OAI/Analysis/CircleDomains/Sobolev/ScalarWeakEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The combined energy of the weak derivative limit is bounded by the original source energy, without the finite-stage error.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.filled_weak_energy_le line 20