OAI/Analysis/CircleDomains/Topology/BoundedCompactCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact smooth cutoff of a bounded weakly differentiable scalar, with its actual product-rule gradient retained.

  1. theorem OAI.CircleDomainRigidity.locallyIntegrable_of_unit_bound line 12
  2. def OAI.CircleDomainRigidity.boundedCompactCutoffWitness line 23