OAI/MeasureTheory/Falconer/Radial/RadialCollisionMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-pin radial collision means on a profile interval

The comparison source is the full conditional source law. The reverse pin law remains a restriction of the original pin measure; no fiber is normalized.

  1. theorem OAI.Falconer.radial_collision_mean_bound line 18