OAI/Analysis/CircleDomains/Sobolev/SmoothScalarCutoffWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth value cutoffs and spatial cutoffs of an actual compact Sobolev function, retaining the exact product/chain-rule gradient.

  1. def OAI.CircleDomainRigidity.smoothScalarCutoffWitness line 13
  2. lemma OAI.CircleDomainRigidity.smoothScalarCutoffWitness_gradient line 44