OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The number of retained vertical bins has the allowed exponential growth.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinKernelCost_nonneg line 10
  2. def OAI.LipschitzHilbert.PacketRepresentation.verticalBinVectorCost line 13
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinVectorCost_nonneg line 16
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinVectorCost_growth line 19