OAI/Analysis/LipschitzHilbert/Estimates/OrdinaryModelConstructionCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cost of the constructed ordinary models is a fixed number. In particular it has no dependence on the finite lattice or translation.

  1. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelNumerics.modelUnitCost line 12
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitModelCost_of_numeric_fields line 20
  3. def OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelNumerics.reverseUnitCost line 34
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.OrdinaryModelConfig.unitReverseModelCost_of_numeric_fields line 43