OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedSelectorPlaneIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-selector marked bounds pass from each terminal line window to the plane. The measurable integrand is the original active path; the locally chosen marked factors need no joint measurability.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_supported_selector_plane_integral line 19