OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedMaskRemoval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mask removal for the literal assigned original packet sum. The per-top raw concentration bound is used with the unchanged original analyzing coefficients, after exact finite regrouping.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_assigned_mask_removal line 16