OAI/Analysis/LipschitzHilbert/Packets/PacketDataUniversalNormalizedStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The removal constants are chosen before the packet lattice, its size, and its scale-dependent geometric parameters.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_universal_normalized_removal_step line 12