OAI/Analysis/LipschitzHilbert/Packets/PacketDataCrossValue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual distinct-profile, masked analyzing packet sum. No auxiliary jet is needed for the physical bilinear operator.

  1. def OAI.LipschitzHilbert.PacketLatticeData.crossPacketValue line 18
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.crossPacketValue_memLp line 24
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.crossSum_memLp line 32