OAI/Analysis/LipschitzHilbert/Trees/SourcePolynomialReferenceArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The reference-event construction with a polynomially growing top-weight scale. The same finite union controls the original selected prefixes and retains its weighted integral, not only the area of the removed set.

  1. theorem OAI.LipschitzHilbert.eventually_polynomial_selected_reference_prefix_area line 14