OAI/Analysis/CircleDomains/Selection/MeanIndexBands.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Boundary band widths of the actual mean are bounded by point hit probabilities. This applies after any continuous local lift, including limits along the physical domain at a collapsed complementary component.

  1. theorem OAI.CircleDomainRigidity.limsup_sub_liminf_le_of_pair_oscillation line 16
  2. theorem OAI.CircleDomainRigidity.meanGeometricIndex_band_width line 38