OAI/Analysis/CircleDomains/Sobolev/SmoothPlaneLinePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrate the positive oscillation cost over an arbitrary finite measurable set of horizontal lines. No choice of crossing points needs to be measurable.

  1. theorem OAI.CircleDomainRigidity.smooth_plane_half_payment line 13