OAI/Analysis/LipschitzHilbert/Packets/PacketDataOriginalIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original finite packet sums and their top-masked versions are integrable on the full plane. No exceptional set or finite-area bound is needed for these qualitative facts.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalMaskedValue_integrable line 22
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalMaskedSum_integrable line 31