OAI/Analysis/CircleDomains/Sobolev/LocallyFiniteL2Sum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

L² control of a pointwise finite sum by the sum of its local error norms. This applies to the countable partition-of-unity error terms.

  1. theorem OAI.CircleDomainRigidity.finiteSupport_hasSum_finsum line 16
  2. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_finsum_of_pointFinite line 21
  3. theorem OAI.CircleDomainRigidity.eLpNorm_finsum_le_tsum_of_pointFinite line 32