OAI/Analysis/LipschitzHilbert/Packets/ShortPacketBoxes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact finite decomposition of the short-scale synthesis into its actual center boxes. Empty fibers are retained and contribute zero.

  1. def OAI.LipschitzHilbert.centerBoxIndex line 16
  2. def OAI.LipschitzHilbert.allPacketBoxes line 20
  3. theorem OAI.LipschitzHilbert.mem_allPacketBoxes line 24
  4. abbrev OAI.LipschitzHilbert.ShortBoxFiber line 28
  5. def OAI.LipschitzHilbert.shortBoxSynthesis line 32
  6. theorem OAI.LipschitzHilbert.shortBoxSynthesis_eq line 39
  7. theorem OAI.LipschitzHilbert.shortSynthesis_eq_sum_boxes line 54
  8. theorem OAI.LipschitzHilbert.component_coefficient_energy line 67