OAI/Analysis/CircleDomains/Sobolev/TrackedGlobalWeakLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual continued tracked test converges off the removable dust, and hence almost everywhere, to its continuous source limit. Its exact model energy and the recursive budget give a global weak gradient.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.exists_tracked_global_weak_limit line 30