OAI/Analysis/LipschitzHilbert/Trees/SourceCentralPathGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual common good-path bounds give the central negative-power estimate. The finite phase count is the manuscript's blockCount(L), and all integrations are over the same good set.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_central_from_paths line 19