OAI/Analysis/CircleDomains/Sobolev/SliceDensityLp.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-chart slice density has finite L² norm in complex, Cartesian and Euclidean coordinates.

  1. theorem OAI.CircleDomainRigidity.sliceChartDensity_complex_memLp line 18
  2. theorem OAI.CircleDomainRigidity.sliceChartDensity_realProd_memLp line 25
  3. theorem OAI.CircleDomainRigidity.sliceChartDensity_euclidean_memLp line 32