SourceOrdinaryTreeEstimate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The ordinary size-density tree estimate for the actual selected packet sum. Scalar Lépingle is the sole published analytic premise here.

def OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryTreeConstant line 15
def OAI.LipschitzHilbert.SourceLabeledLattice.separatedTreeEnergy line 24
Source documentation
The separated portion of the original coefficient family, as in Eq. (size) of the manuscript.
```
def separatedTreeEnergy (P : SourceLabeledLattice N κ Label Item) (cb : ℝ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ) : ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice
theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_ordinary_tree_estimate line 30