OAI/Analysis/LipschitzHilbert/Packets/SourceFrozenTreeEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The frozen long-tree estimate with the actual density masks and reproducing kernels constructed. Its only published analytic input is scalar Lépingle; the coefficient-size hypothesis is the ordinary tree size.

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