OAI/Analysis/LipschitzHilbert/Trees/SourceDemodulatedLong.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Narrow-bin reproduction for actual long intervals. The transverse weight and all physical cells retain their original spatial width.

  1. theorem OAI.LipschitzHilbert.packetNormSup_verticalDemodulation line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLongIntervalSchwartz_demodulated_bands line 26