Stopped scale identity implies the scale-function ratio

Proved

AvramDividend.Classical.stopped_scale_identity_to_ratio

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

optimal-dividendsscale-functionsource-faithful-child

If an extended-nonnegative-real L satisfies L times ENNReal.ofReal va equals ENNReal.ofReal vx with 0 < va, then L equals ENNReal.ofReal (vx / va).

Preamble

import Mathlib

open scoped ENNReal

Formal statement

namespace AvramDividend.Classical

theorem stopped_scale_identity_to_ratio
    (L : ℝ≥0∞) (vx va : ℝ)
    (hL : L * ENNReal.ofReal va = ENNReal.ofReal vx)
    (hva : 0 < va) :
    L = ENNReal.ofReal (vx / va) := by sorry

end AvramDividend.Classical

Source

Algebraic bridge isolating the final division step of the Proposition 1 two-sided-exit reduction: the stopped-scale identity (lintegral times ofReal (W a) equals ofReal (W x)) implies the ratio form once W a > 0. Pure ENNReal algebra, no stochastic content; reusable by the corrected two-sided-exit target.

View graph