OAI/Analysis/LipschitzHilbert/Fourier/GlobalBandLocalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact patching of the local band theorem over disjoint horizontal strips, with a uniform finite-overlap cost.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.bandL2Operator_horizontal_patch line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.bandL2Operator_global_from_local line 50