OAI/Analysis/LipschitzHilbert/Trees/SourcePolynomialGoodPathArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial weight scales are admitted before forming the common reference bad set. The weighted bad mass retains its integral bound, and Markov's inequality gives the same area loss for the common good set.

  1. theorem OAI.LipschitzHilbert.eventually_source_polynomial_good_path_area line 13