OAI/Analysis/LipschitzHilbert/Trees/SourceBoundaryIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every fixed-translation boundary sum is integrable whenever its original finite packet values are integrable. This supplies all sections needed for recovery, in addition to the averaged Fubini estimate.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_sum_integrable line 16