OAI/Analysis/LipschitzHilbert/Packets/PacketDataModelCostPolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial dependence of the explicit model cost on the two packet adaptation bounds. All remaining factors involve fixed geometric data.

  1. def OAI.LipschitzHilbert.PacketLatticeData.ordinaryTreeUnitCost line 10
  2. def OAI.LipschitzHilbert.PacketLatticeData.selectedNearUnitCost line 16
  3. def OAI.LipschitzHilbert.PacketLatticeData.selectedFarUnitCost line 19
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceTreeConstant_le_unit line 26
  5. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitSizeAreaCost line 42
  6. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitStepCost line 46
  7. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitModelCost line 50
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.sizeAreaConstant_le_unit line 53
  9. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitStepCost_nonneg line 86
  10. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.modelCost_le_cubic line 93
  11. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.modelCost_le_rpow line 137