OAI/Analysis/CircleDomains/Modulus/SphericalWeightedLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The spherical metric contributes its decay factor to weighted level length. No pointwise finiteness of the nonnegative density is required.

  1. theorem OAI.CircleDomainRigidity.finite_sphere_chart_weighted_length_le line 19
  2. theorem OAI.CircleDomainRigidity.spherical_weighted_density_sq_finite line 55
  3. theorem OAI.CircleDomainRigidity.spherical_weighted_length_le_chart line 64
  4. theorem OAI.CircleDomainRigidity.scaled_spherical_weighted_density_sq_finite line 94