OAI/Analysis/LipschitzHilbert/Phase/SourceAngularFrozenEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The frozen tree estimate at independent angular width, with the narrow vertical bins required by the manuscript. Scalar Lépingle is its only published analytic input.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_angular_frozen_tree_estimate line 16