OAI/Analysis/CircleDomains/Sobolev/DensityL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The real representative of a finite-energy density is locally L² in the physical planar chart, including densities that are infinite on a null set.

  1. theorem OAI.CircleDomainRigidity.memLp_two_toReal_of_lintegral_sq_ne_top line 16
  2. theorem OAI.CircleDomainRigidity.physical_density_memLp_rectangle line 27