OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledUniformGoodTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform local tails for the actual physical reference bad set. All three component tails follow from original packet spectra, selector bounds and slope multiplicity. No tail or active-cardinality premise is retained, and the threshold is selected before the packet family.

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