OAI/Analysis/LipschitzHilbert/Estimates/OrdinaryModelNumerics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed choices of the separation gaps in the ordinary packet model. They depend only on the spectral and selector constants, never on the number of scales, sites, carriers, or the input functions.

  1. structure OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelNumerics line 12
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_ordinary_model_numerics line 20