OAI/Analysis/CircleDomains/Probability/LocalizedDensityNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Outside the permitted perturbation region, the smoothed barrier is controlled by the original spherical density, with one fixed chart constant.

  1. theorem OAI.CircleDomainRigidity.spherical_weighted_density_eLpNorm_euclidean_le line 18
  2. theorem OAI.CircleDomainRigidity.localized_perturbed_density_eLpNorm_le line 35