OAI/Analysis/LipschitzHilbert/Geometry/SourceTreeFarEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The analytic distant-scale bound for a selected long tree and a packed short family, conditional only on the published Lépingle input.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_tree_far_gram_bound line 15