OAI/Analysis/LipschitzHilbert/Trees/SourcePolynomialSelectedGoodPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The selected-reference weighted good set follows from original packet spectra and selector hypotheses. The component event estimates are proved internally, including the exact reference/path slope change. No exceptional-set or variation estimate is supplied as source data.

  1. theorem OAI.LipschitzHilbert.eventually_polynomial_uniform_selected_reference_good_path line 16