OAI/Analysis/LipschitzHilbert/Estimates/BoxSynthesisEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed-box energy step in the reference-line concentration proof. The assumed coefficient budget is the finite local Carleson sum appearing in equation (src-10); the synthesis estimate is derived from envelopes.

  1. theorem OAI.LipschitzHilbert.box_synthesis_energy line 15