OAI/Analysis/CircleDomains/Selection/MeanSlicePointwise.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact transverse tests turn the integrated coarea estimate into an almost-everywhere bound on each physical horizontal slice.

  1. theorem OAI.CircleDomainRigidity.meanSliceCount_restrict line 19
  2. theorem OAI.CircleDomainRigidity.ae_meanSliceCount_le line 43