OAI/Analysis/LipschitzHilbert/Trees/SourceFiniteLongTree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite frozen long-tree estimate. The transversely weighted tree energy is the only analytic estimate remaining at this interface; all maximal, spectral, partition, mass and summation steps are proved.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_frozen_long_tree_bound line 18