OAI/Analysis/LipschitzHilbert/Trees/SourceOriginalIntegrability.lean

GitHub source file

4 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.SourceLabeledLattice.physicalCrossPacketValue_memLp line 22
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCrossSum_memLp line 41
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_integrable line 46
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedSum_integrable line 55