OAI/Analysis/LipschitzHilbert/Trees/SourceResidualCostBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed polynomial residual losses are absorbed by the source mass cutoff, uniformly for the full permitted range of the phase exponent.

  1. theorem OAI.LipschitzHilbert.source_principal_residual_costs line 11