OAI/Analysis/CircleDomains/Selection/HorizontalMeanIndexBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On a physical horizontal segment, a local logarithmic lift of the actual mean index is bounded by the original-law intersection count.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_mono_set line 20
  2. theorem OAI.CircleDomainRigidity.meanIndex_horizontal_segment_bound line 30