OAI/Analysis/LipschitzHilbert/Packets/PacketDataDensityGoodRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The common concentration set gives popular recovery. The deleted-area and mask losses, global weight budget and numerical parameters follow from the common-set estimates and the density forest.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_density_recovery_of_good_set line 17