OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedTree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ordinary tree estimates for selected packets of an unrestricted slope family. The only published input is scalar Lépingle variation. Small shear is proved for the selected reference family, not assumed globally.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_recentered_selected_tree_estimate line 13