OAI/Analysis/LipschitzHilbert/Packets/SourcePacketPathProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The path-product theorem applied to original packet amplitudes. The remaining analytic inputs are explicit square sums and propagated residual bounds; no path-product estimate is assumed.

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