OAI/Analysis/LipschitzHilbert/Packets/PlanarPacketFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The planar dyadic packet family and its restriction to an actual short-packet center box. This restriction carries no coefficient budget.

  1. structure OAI.LipschitzHilbert.PlanarPacketFamily line 15
  2. def OAI.LipschitzHilbert.PlanarPacketFamily.length line 38
  3. def OAI.LipschitzHilbert.PlanarPacketFamily.centerX line 40
  4. def OAI.LipschitzHilbert.PlanarPacketFamily.centerZ line 43
  5. theorem OAI.LipschitzHilbert.PlanarPacketFamily.length_pos line 46
  6. def OAI.LipschitzHilbert.PlanarPacketFamily.boxIndex line 49
  7. abbrev OAI.LipschitzHilbert.PlanarPacketFamily.BoxFiber line 52
  8. def OAI.LipschitzHilbert.PlanarPacketFamily.referenceBox line 55
  9. def OAI.LipschitzHilbert.PlanarPacketFamily.selectedWave line 88
  10. def OAI.LipschitzHilbert.PlanarPacketFamily.mainCoefficient line 92
  11. theorem OAI.LipschitzHilbert.PlanarPacketFamily.referenceBox_coefficient line 98