OAI/Analysis/LipschitzHilbert/Trees/SourceRadialTelescoping.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite sum of literal radial log ratios is bounded by geometric boundary depth, including the terminal eligibility cutoff.

  1. theorem OAI.LipschitzHilbert.AngularGrid.radial_log_ratio_sum_le_depth line 15