OAI/Analysis/LipschitzHilbert/Estimates/OrdinaryModelConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Construct the ordinary model from its geometric data. The numerical parameters are fixed before the finite packet collection is chosen. The auxiliary positive cutoff is chosen below every packet's angular scale.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.length_le_topLength line 14
  2. def OAI.LipschitzHilbert.PacketLatticeData.ordinaryModelOfGeometry line 20