OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledSpectralGoodTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original packet spectra and the fixed active-label count discharge the main-square and masked-variation tails in the physical reference event. The only remaining component premise is the independently constructed positive angular-error tail.

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