OAI/Analysis/CircleDomains/Selection/MappedMeanBands.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The mean-index band bound in the original path law. Injectivity of the actual Jordan coordinate identifies the hit event exactly.

  1. theorem OAI.CircleDomainRigidity.mapped_arc_hit_probability_eq line 18
  2. theorem OAI.CircleDomainRigidity.mapped_meanGeometricIndex_band_width line 39