OAI/Analysis/LipschitzHilbert/Trees/SourceRootIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The root estimates integrate the exact boundary-weighted packet sum. At most two nonempty eligible roots occur in the bounded slope range, so this final spatial sum has only an absolute factor.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundarySum_integral_le line 18