OAI/Analysis/LipschitzHilbert/Packets/PacketDataPathRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original selected coefficients are fixed integrals. Spatial regularity of the masked packets therefore requires no regularity of the selecting direction field beyond that used to define them.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalMaskedValue_continuous line 15
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.physicalMaskedPath_measurable line 29