OAI/Analysis/LipschitzHilbert/Trees/SourceResidualPolynomial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial good-path thresholds control the actual residual square with an exponent fixed before the path and the mass cutoff are chosen.

  1. theorem OAI.LipschitzHilbert.residual_square_polynomial_bound line 11