OAI/Analysis/CircleDomains/Sobolev/StaircaseGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual differential of the cutoff staircase

This identifies the random covectors used in the wedge-cost selection with derivatives of the modified scalar coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_cutoffStaircase line 19
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_cutoff_shiftedStaircase line 29