OAI/Analysis/LipschitzHilbert/Trees/SourceOriginalRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recover the original adjoint sum with the manuscript's fixed and moving exceptional-area budgets. The common good set precedes all translations, and only the boundary error is averaged.

  1. theorem OAI.LipschitzHilbert.eventually_original_recovery line 16