OAI/Analysis/LipschitzHilbert/Estimates/NormalizedProfileBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Choose the finite derivative order and Fourier-decay exponent before any packet lattice. Their fixed profile cost fits the model's logarithmic budget once the disparity parameter is large enough.

  1. def OAI.LipschitzHilbert.PacketRepresentation.requiredPacketOrder line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.requiredPacketOrder_basic line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_normalized_profile_budget line 18