OAI/Analysis/CircleDomains/Probability/SphericalSliceDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The physical occupation density gives a square-integrable planar slice density in every finite inverse-chart neighborhood.

  1. theorem OAI.CircleDomainRigidity.sphericalArea_setLIntegral_coe line 18
  2. def OAI.CircleDomainRigidity.sliceChartDensity line 30
  3. theorem OAI.CircleDomainRigidity.measurable_sliceChartDensity line 33
  4. theorem OAI.CircleDomainRigidity.sliceChartDensity_sq_integral_le line 38
  5. theorem OAI.CircleDomainRigidity.sliceChartDensity_sq_integral_finite line 63
  6. theorem OAI.CircleDomainRigidity.mean_sphericalSliceCount_le_density line 71