OAI/Analysis/LipschitzHilbert/Packets/PacketDataHighDensityPopularRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

High ordinary density supplies the actual popular forest. Its retained angular cells put every keeper in the source direction chart, so both the top-direction and root-interval hypotheses of recovery are derived.

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