Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Problem 13 Milestone — Exponential boundary continuous abel solution

Open
RybinAI2026.P13.exponential_boundary_continuous_abel_solution

by wenxinzhang · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

brownian-motioncomputational-neurosciencefirst-passage-timesstochastic-processesvolterra-integral-equations

For every b0,c∈Rb₀,c\in\mathbb Rb0​,c∈R with b0>0b₀>0b0​>0 and c>0c>0c>0, there exists at least one total function f:R→Rf:\mathbb R\to\mathbb Rf:R→R, possibly depending on both parameters, that is continuous on the open positive half-line and satisfies f(t)≥0f(t)\ge 0f(t)≥0 for every t>0t>0t>0. Writing B(u)=b0exp⁡(−cu)B(u)=b₀\exp(-cu)B(u)=b0​exp(−cu) and φ(x)=(2π)−1/2exp⁡(−x2/2)\varphi(x)=(2\pi)^{-1/2}\exp(-x^2/2)φ(x)=(2π)−1/2exp(−x2/2), this same fff must satisfy, for every real t>0t>0t>0, ∫0t1t−s φ ⁣(B(t)−B(s)t−s)f(s) ds=1t φ ⁣(B(t)t)\displaystyle \int_0^t \frac{1}{\sqrt{t-s}}\,\varphi\!\left(\frac{B(t)-B(s)}{\sqrt{t-s}}\right)f(s)\,ds=\frac{1}{\sqrt t}\,\varphi\!\left(\frac{B(t)}{\sqrt t}\right)∫0t​t−s​1​φ(t−s​B(t)−B(s)​)f(s)ds=t​1​φ(t​B(t)​), where the integral is the Lebesgue interval integral in the variable sss. For positive ttt, its effective integration domain is (0,t](0,t](0,t], equivalently [0,t][0,t][0,t] up to a null endpoint. At s=ts=ts=t, the apparently singular expression is interpreted using total real division: t−s=0\sqrt{t-s}=0t−s​=0, both 1/01/01/0 and 0/00/00/0 are defined as 000, and hence the integrand’s endpoint value is 000; this singleton value does not affect the integral. No separate integrability hypothesis is stated: under the totalized integral convention a nonintegrable integrand has integral 000, while the displayed right-hand side is strictly positive under the stated assumptions, so the required equality can hold only when the integrand is integrable for each positive ttt. The declaration imposes no condition at t=0t=0t=0 or at negative arguments: f(0)f(0)f(0) and all values f(t)f(t)f(t) for t<0t<0t<0 are unrestricted, continuity need not extend to 000, and no boundedness near 000 is asserted. It also asserts neither uniqueness nor strict positivity of fff, and requires no normalization, elementary-expression or closed-form representation, or additional regularity.

Preamble
import Definitions.Def_rybin2026_p13_exponential_boundary

open MeasureTheory Set
Formal statement
namespace RybinAI2026.P13

/-- Analytic existence milestone: construct a continuous nonnegative solution of the Abel
equation before proving normalization and elementary closed-form representability. -/
theorem exponential_boundary_continuous_abel_solution
    (b₀ c : ℝ) (hb₀ : 0 < b₀) (hc : 0 < c) :
    ∃ f : ℝ → ℝ,
      ContinuousOn f (Ioi 0) ∧
      (∀ t, 0 < t → 0 ≤ f t) ∧
      SolvesAbelEquation b₀ c f := by
  sorry

end RybinAI2026.P13
Source
https://rybindmitry.github.io/problems/13.html
Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every b0,c∈Rb₀,c\in\mathbb Rb0​,c∈R with b0>0b₀>0b0​>0 and c>0c>0c>0, there exists at least one total function f:R→Rf:\mathbb R\to\mathbb Rf:R→R, possibly depending on both parameters, that is continuous on the open positive half-line and satisfies f(t)≥0f(t)\ge 0f(t)≥0 for every t>0t>0t>0. Writing B(u)=b0exp⁡(−cu)B(u)=b₀\exp(-cu)B(u)=b0​exp(−cu) and φ(x)=(2π)−1/2exp⁡(−x2/2)\varphi(x)=(2\pi)^{-1/2}\exp(-x^2/2)φ(x)=(2π)−1/2exp(−x2/2), this same fff must satisfy, for every real t>0t>0t>0, ∫0t1t−s φ ⁣(B(t)−B(s)t−s)f(s) ds=1t φ ⁣(B(t)t)\displaystyle \int_0^t \frac{1}{\sqrt{t-s}}\,\varphi\!\left(\frac{B(t)-B(s)}{\sqrt{t-s}}\right)f(s)\,ds=\frac{1}{\sqrt t}\,\varphi\!\left(\frac{B(t)}{\sqrt t}\right)∫0t​t−s​1​φ(t−s​B(t)−B(s)​)f(s)ds=t​1​φ(t​B(t)​), where the integral is the Lebesgue interval integral in the variable sss. For positive ttt, its effective integration domain is (0,t](0,t](0,t], equivalently [0,t][0,t][0,t] up to a null endpoint. At s=ts=ts=t, the apparently singular expression is interpreted using total real division: t−s=0\sqrt{t-s}=0t−s​=0, both 1/01/01/0 and 0/00/00/0 are defined as 000, and hence the integrand’s endpoint value is 000; this singleton value does not affect the integral. No separate integrability hypothesis is stated: under the totalized integral convention a nonintegrable integrand has integral 000, while the displayed right-hand side is strictly positive under the stated assumptions, so the required equality can hold only when the integrand is integrable for each positive ttt. The declaration imposes no condition at t=0t=0t=0 or at negative arguments: f(0)f(0)f(0) and all values f(t)f(t)f(t) for t<0t<0t<0 are unrestricted, continuity need not extend to 000, and no boundedness near 000 is asserted. It also asserts neither uniqueness nor strict positivity of fff, and requires no normalization, elementary-expression or closed-form representation, or additional regularity.

Human review
  • Endorsed by Shuze Chen · Sep 1, 2026

  • Endorsed by wenxinzhang · Sep 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me