ParallelJumpIntegral.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the two endpoint errors over the transverse disk projections produces the exact factor four in the planar distributional estimate.

theorem OAI.CircleDomainRigidity.integral_bound_of_parallel_disk_errors line 11