OAI/Analysis/CircleDomains/Sobolev/PairedEnergyCauchy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equality of two-component Dirichlet energies of differences transfers strong Cauchy control. This is the Hilbert-space step in conformal energy transport for nonsmooth functions.

  1. theorem OAI.CircleDomainRigidity.integral_sq_sub_eq_Lp_dist_sq line 13
  2. theorem OAI.CircleDomainRigidity.cauchy_partials_of_paired_energy_isometry line 20