OAI/Analysis/CircleDomains/Probability/SliceDensityNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The slice density used by the smoothed mean has a quantitative L² bound in the same Euclidean chart as its partial derivatives.

  1. theorem OAI.CircleDomainRigidity.eLpNorm_toReal_le_square_integral line 17
  2. theorem OAI.CircleDomainRigidity.sliceChartDensity_complex_eLpNorm_le line 31
  3. theorem OAI.CircleDomainRigidity.sliceChartDensity_euclidean_eLpNorm_le line 47