OAI/Analysis/LipschitzHilbert/Trees/SourceTreeMomentBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite source tree, with polynomial node and path costs, provides the small-imaginary vertex moment in §11. Constants are fixed before the finite packet family or the spatial good set is chosen.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_tree_vertex_moment line 17