OAI/Analysis/CircleDomains/Sobolev/ScalarCutoffEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise energy control for the actual product-and-chain-rule field. Constants depend only on the fixed smooth cutoffs.

  1. lemma OAI.CircleDomainRigidity.scalar_cutoff_energy_algebra line 11
  2. lemma OAI.CircleDomainRigidity.smoothScalarCutoffWitness_energy line 38