OAI/Analysis/LipschitzHilbert/Trees/SourceLongCellEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted disjoint-cell estimate specialized to the manuscript's actual long packet intervals. All Fourier and geometric premises of the reproduction estimate are discharged here.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_long_cell_energy line 20