OAI/Analysis/CircleDomains/Sobolev/SphericalGradientEnergyNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Express the actual spherical Dirichlet energy through its two L² partial-derivative norms.

  1. theorem OAI.CircleDomainRigidity.integral_sq_eq_eLpNorm_toReal_sq line 14
  2. theorem OAI.CircleDomainRigidity.spherical_gradient_energy_eq_norms line 26