OAI/Analysis/LipschitzHilbert/Geometry/PacketDataFarGram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The distant-scale Gram contribution of an actual selected tree is bounded by the short-packet envelope paired with its interval maximum.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.packetVector_memLp line 16
  2. def OAI.LipschitzHilbert.PacketLatticeData.longPacketSum line 23
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.longPacketSum_memLp line 28
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.far_gram_le_maximal_pairing line 34