OAI/Analysis/CircleDomains/Sobolev/CircleStaircaseGradient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual cutoff differential of a periodic coordinate

The same covector formula used by the random-grid estimate is the intrinsic differential of the descended circle cutoff. Its scalar input can be the bounded canonical representative; integer changes of branch do not change either the multiplier or the error term.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_map_add_int_of_add_one line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.staircaseCovector_reciprocal_add_int line 29
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_reciprocal_cutoff line 42