LocalizedStopped.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

High-height localization for the actual stopped coefficients. The outer and inner energies are derived from their divisor definitions.

theorem OAI.CubicFirstMoment.localized_stopped_bilinear_log_saving line 13