OAI/Analysis/CircleDomains/Sobolev/ExtendedDensityL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite-energy extended density has a Borel real L² representative. Its infinite values are retained separately as a reference-null Borel set.

  1. lemma OAI.CircleDomainRigidity.lintegral_ofReal_toReal_eq_away_infinity line 15
  2. lemma OAI.CircleDomainRigidity.extended_density_L2 line 24