OAI/Analysis/CircleDomains/Modulus/MeanIndexOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local oscillation of the averaged index is bounded by the probability that the sampled arc hits the projected point.

  1. theorem OAI.CircleDomainRigidity.meanGeometricIndex_oscillation_le_hit line 15