OAI/Analysis/CircleDomains/Sobolev/CoordinateGradientSize.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The spherical Dirichlet norm is bounded by the two physical partial norms used by the barrier construction, on the same measurable region.

  1. theorem OAI.CircleDomainRigidity.spherical_gradient_norm_le_partial_norms line 20
  2. theorem OAI.CircleDomainRigidity.physical_coordinate_gradient_size_le line 36
  3. theorem OAI.CircleDomainRigidity.coordinate_band_counting_norm_le line 53