OAI/Analysis/LipschitzHilbert/Trees/SourceDemodulatedCellEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Long-cell energy with constants independent of the carrier locations and of the ratio between spatial and angular widths.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_demodulated_long_cell_energy line 16