OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedWeightedMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Product-weighted maximal control only needs tree geometry and separation on packets with nonzero coefficients.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_supported_weighted_tree_maximal line 16