OAI/Analysis/CircleDomains/Sobolev/WeakPartialPairingLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak L2 pairings identify derivatives of bounded pointwise limits. The same pairings retain localized energy estimates on measurable sets.

  1. lemma OAI.CircleDomainRigidity.weakPartial_of_bounded_pointwise_weak_limit line 14
  2. lemma OAI.CircleDomainRigidity.weak_pairings_restrict line 37
  3. lemma OAI.CircleDomainRigidity.weak_pair_energy_restrict_le line 53