SourceAngularOrdinaryTree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary size-density tree bound with separate angular width and spatial width. Constants are uniform in their ratio and in the number of vertical frequency bins.

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