OAI/Analysis/LipschitzHilbert/Trees/UnaryRunResidual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cubic residual cost over all constructed unary runs.

  1. theorem OAI.LipschitzHilbert.unary_runs_residual_sum line 14