Every nonnegative continuous exponential-boundary Abel solution has total mass one

Proved

RybinAI2026.P13.exponential_boundary_abel_solution_mass_one

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

brownian-motionintegral-equationsprobability

Let $b_0,c>0$ , put $b(t)=b_0e^{-ct}$ , and let $\phi$ be the standard Gaussian density. Let $f:\mathbb R\to\mathbb R$ be continuous and nonnegative for $t>0$ and satisfy, for every $t>0$ ,

\int_0^t \frac{1}{\sqrt{t-s}}\phi\!\left(\frac{b(t)-b(s)}{\sqrt{t-s}}\right)f(s)\,ds =\frac{1}{\sqrt t}\phi\!\left(\frac{b(t)}{\sqrt t}\right).

Then $f$ is integrable on every finite positive interval, and

\int_0^T f(s)\,ds\le1\quad(T>0),\qquad \lim_{T\to\infty}\int_0^T f(s)\,ds=1.

This supplies the normalization required by the mission. Integrability near zero and unit mass are conclusions, with no extra regularity assumption at zero and no assumption of elementary expressibility.

Preamble

import Definitions.Def_rybin2026_p13_exponential_boundary
open Filter MeasureTheory Set
open scoped Topology

Formal statement

namespace RybinAI2026.P13

theorem exponential_boundary_abel_solution_mass_one (b₀ c : ℝ) (hb₀ : 0 < b₀) (hc : 0 < c)
    (f : ℝ → ℝ) (hfc : ContinuousOn f (Ioi 0))
    (hfn : ∀ t, 0 < t → 0 ≤ f t)
    (habel : RybinAI2026.P13.SolvesAbelEquation b₀ c f) :
    (∀ T, 0 < T → IntervalIntegrable f volume 0 T ∧ (∫ s in (0:ℝ)..T, f s) ≤ 1) ∧
    Tendsto (fun T : ℝ => ∫ s in (0:ℝ)..T, f s) atTop (nhds 1)  := by sorry

end RybinAI2026.P13

Source

Normalization lemma for Rybin Problem 13, https://rybindmitry.github.io/problems/13.html, displayed characterizing Abel equation (condition 3). The argument applies more generally to a bounded nonnegative measurable boundary. In the proof, the triangular Fubini and inverse-square-root integral helpers are adapted with credit from ryanshin, Prove2Me submission 80cd703c-5b47-463e-9982-3e2df931d0de, BrownianComponent13–14.

View graph