OAI/Analysis/CircleDomains/Sobolev/CircleGradientSize.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full spherical energy of a circle coordinate is controlled by its two real partial derivatives, with no choice of global real lift.

  1. theorem OAI.CircleDomainRigidity.circle_gradient_energy_eq_norms line 15
  2. theorem OAI.CircleDomainRigidity.circle_gradient_norm_le_partial_norms line 32