OAI/Analysis/LipschitzHilbert/Packets/PacketDataModelConfig.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed geometric and selector data for the ordinary model. None of these parameters depends on the input function or the tested set.

  1. structure OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig line 15
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceTreeConstant_nonneg line 88
  3. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.sizeAreaConstant line 98
  4. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.stepConstant line 102
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.sizeAreaConstant_nonneg line 106
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.stepConstant_nonneg line 111