OAI/Analysis/LipschitzHilbert/Packets/PacketDataWeightedMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted maximal estimates for actual selected trees of unrestricted packet data. The bounded reference lattice is constructed from the tree's own angular cone.

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