OAI/Analysis/CircleDomains/Sobolev/SmoothLineOscillation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The smooth line estimate for a non-unit oscillation. This allows uniform mollifications of a continuous Sobolev barrier to retain a positive crossing cost without assuming an ACL theorem.

  1. theorem OAI.CircleDomainRigidity.smooth_line_oscillation line 13
  2. theorem OAI.CircleDomainRigidity.smooth_line_half_payment line 37