OAI/Analysis/LipschitzHilbert/Fourier/AnnularPartitionIdentities.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The positive and negative annular cutoffs reconstruct the actual low-pass difference, whose finite geometric sums telescope exactly.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_halfsum_nonneg line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_halfsum line 25
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_reflected_sum line 32
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_step line 38
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_telescope line 47
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.reassembly_signed_telescope line 56