OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinPlateau.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed enlarged vertical cutoff equals one on every bin profile. The finite bin partition is exact throughout the prescribed annulus.

  1. def OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal_zero line 15
  3. def OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateau line 20
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateau_one line 36
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateau_support line 42
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateau_mul_profile line 53
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.positiveBand_bin_partition line 59