OAI/Analysis/LipschitzHilbert/Fourier/AnnularSlopePartition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On an annular multiplier, bounded output directions imply a finite range of frequency slopes. The constructed arithmetic partition covers that entire range, with no remaining partition-of-unity premise.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.annular_normalized_slope_bound line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteSlopePartition_annular line 35