OAI/Analysis/CircleDomains/Sobolev/RectangularL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite rectangle integration is continuous for the actual strong L2 residuals. The coordinate and almost-everywhere bridges retain the full closed rectangle required by Morera.

  1. lemma OAI.CircleDomainRigidity.tendsto_complex_setIntegral_L2 line 17
  2. lemma OAI.CircleDomainRigidity.doubleSetIntegral_eq_complex_integral line 25
  3. lemma OAI.CircleDomainRigidity.tendsto_doubleSetIntegral_L2 line 48
  4. lemma OAI.CircleDomainRigidity.tendsto_doubleIntervalIntegral_L2 line 63
  5. lemma OAI.CircleDomainRigidity.doubleIntervalIntegral_congr_ae line 77