OAI/Analysis/LipschitzHilbert/Trees/SourceOffchildRegroup.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing a child top before grouping packets gives exactly the removed-child top-band family. The masses and transition coefficients continue to use the original full top collection.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_regroup_offchild line 15