OAI/Analysis/LipschitzHilbert/Packets/PacketDataNormalizedRemovalStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual density/size removal at its normalized dyadic threshold. All input-function and tested-set dependence is explicit in the bound.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_normalized_removal_step line 14