OAI/Analysis/LipschitzHilbert/Trees/SourceBoundaryErrorDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual dyadic boundary radius beats every fixed polynomial. This pays for the integrated packet error after its entropy bound.

  1. theorem OAI.LipschitzHilbert.eventually_boundary_error_power_budget line 13
  2. theorem OAI.LipschitzHilbert.eventually_boundary_radius_small line 33