OAI/Analysis/CircleDomains/Sobolev/L2SummableMajorant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The pointwise sum of the cutoff differential norms is itself in L2, with the sum of their L2 norms as a bound.

  1. theorem OAI.CircleDomainRigidity.l2_tsum_of_summable_norms line 12