CenteredPacketGain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual coarse-cell projections yield the product gain for the original packet. The projected rows are constructed in the proof; neither product structure nor a separated output pencil family is assumed.

theorem OAI.Falconer.centered_packet_gain_of_local_energy line 13