An elementary expression for a nonnegative exponential-boundary Abel solution

Open

RybinAI2026.P13.exponential_boundary_elementary_abel_solution

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

brownian-motionintegral-equationsprobability

For every $b_0,c>0$ , let $b(t)=b_0e^{-ct}$ and let $\phi$ be the standard Gaussian density. There exists a finite expression in the original mission's specified elementary-expression language whose evaluation $E(t)$ is continuous and nonnegative for $t>0$ and satisfies

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

This is the elementary-representability part of the original mission. Total mass one is supplied separately by the normalization theorem. The expression language is exactly the original finite-tree language, with its listed arithmetic operations, exponential, logarithm, square root, sine, cosine, and Gaussian density.

Preamble

import Definitions.Def_rybin2026_p13_exponential_boundary
open Filter MeasureTheory Set
open scoped Topology

Formal statement

namespace RybinAI2026.P13

theorem exponential_boundary_elementary_abel_solution
    (b₀ c : ℝ) (hb₀ : 0 < b₀) (hc : 0 < c) :
    ∃ expression : ElementaryExpr,
      ContinuousOn expression.eval (Ioi 0) ∧
      (∀ t, 0 < t → 0 ≤ expression.eval t) ∧
      SolvesAbelEquation b₀ c expression.eval := by sorry

end RybinAI2026.P13

Source

Rybin Problem 13, https://rybindmitry.github.io/problems/13.html, requested elementary density and characterizing equation; exact remaining requirement of RybinAI2026.P13.exponential_boundary_elementary_density after normalization.

View graph