OAI/Analysis/LipschitzHilbert/Trees/SourceFixedException.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed concentration/count exception is charged to the original L2 packet sum with the prescribed polynomial area budget.

  1. theorem OAI.LipschitzHilbert.original_fixed_exception_cost line 14