OAI/Analysis/LipschitzHilbert/Packets/ReferencePacketFamily.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite packet data in one reference box. Coefficients are left arbitrary for the weighted synthesis and subsequent duality argument.

  1. structure OAI.LipschitzHilbert.ReferencePacketFamily line 14
  2. def OAI.LipschitzHilbert.ReferencePacketFamily.packets line 41
  3. def OAI.LipschitzHilbert.ReferencePacketFamily.coefficientEnergy line 45
  4. theorem OAI.LipschitzHilbert.ReferencePacketFamily.coefficientEnergy_nonneg line 49
  5. theorem OAI.LipschitzHilbert.ReferencePacketFamily.horizontal_energy line 55
  6. theorem OAI.LipschitzHilbert.ReferencePacketFamily.weighted_energy line 70