OAI/Analysis/CircleDomains/Transfer/FilledGapIntegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-gap estimate as an integral of the actual filled function, with its ordinary derivative off the finitely many jumps.

  1. theorem OAI.CircleDomainRigidity.intervalIntegral_congr_Ioo line 12
  2. theorem OAI.CircleDomainRigidity.filled_gap_integration_bound line 18