Problem 13 definitions — First-passage time of Brownian motion to an exponentially decaying boundary

ElementaryExpr is a parameter-free inductive type whose elements are finite expression trees. It has a nullary variable expression; a rational-constant expression for every $q∈ℚ$; a real-constant expression for every $x∈ℝ$; binary addition, subtraction, multiplication, and division expressions formed from any two expressions; and unary negation, exponential, logarithm, square-root, sine, cosine, and normal-density expressions formed from any one expression. There are no side conditions on any constructor and no equations identifying distinct constructor trees.

For every elementary expression $E$ and every real input $t$, ElementaryExpr.eval assigns a real value, denoted $⟦E⟧(t)$, recursively as follows: the variable evaluates to $t$; a rational constant $q$ evaluates to its image in $ℝ$, independently of $t$; a real constant $x$ evaluates to $x$, independently of $t$; addition, subtraction, multiplication, and division evaluate to $⟦A⟧(t)+⟦B⟧(t)$, $⟦A⟧(t)-⟦B⟧(t)$, $⟦A⟧(t)⟦B⟧(t)$, and $⟦A⟧(t)/⟦B⟧(t)$, respectively; negation evaluates to $-⟦A⟧(t)$; and the exponential, logarithm, square-root, sine, and cosine constructors evaluate to the corresponding real functions applied to $⟦A⟧(t)$. The normal-density constructor evaluates to $(2π)^{-1/2}e^{-⟦A⟧(t)^2/2}$. All operations are total: division by zero, including $0/0$, evaluates to $0$; the real logarithm evaluates to $0$ at $0$ and to the logarithm of the absolute value at a nonzero negative input; and the real square root evaluates to $0$ on every nonpositive input. Thus every syntactically valid expression has a real value at every real input, with no domain-error condition.

For every $b₀,c,t∈ℝ$, boundary is the real number $b₀e^{-ct}$. No signs or nonzeroness conditions are imposed: $b₀=0$ gives the identically zero function of $t$, $c=0$ gives the constant value $b₀$, negative $c$ is allowed and produces exponential growth in magnitude as $t$ increases when $b₀≠0$, negative $b₀$ is allowed, and negative, zero, and positive values of $t$ are all within the definition. The declaration defines this formula but does not itself assert any decay property.

For every $x∈ℝ$, normalDensity is the real number $(2π)^{-1/2}e^{-x^2/2}$. It is defined for every real $x$; the declaration introduces only this function and does not itself assert that it integrates to one or attach a probability measure to it.

Given arbitrary $b₀,c∈ℝ$ and an arbitrary total function $f:ℝ→ℝ$, SolvesAbelEquation(b₀,c,f) means that for every real $t$, if $t>0$, then, writing $B(u)=b₀e^{-cu}$ and $φ(x)=(2π)^{-1/2}e^{-x^2/2}$, the equality $∫_{(0,t]} [1/√(t-s)]\,φ((B(t)-B(s))/√(t-s))\,f(s)\,ds=[1/√t]\,φ(B(t)/√t)$ holds, where the integral is the real Lebesgue interval integral with its positive orientation from $0$ to $t$. Equivalently, the boundary terms appearing in the equation are exactly $B(t)=b₀e^{-ct}$ and $B(s)=b₀e^{-cs}$. For $t≤0$, the implication is automatically true and imposes no condition; no equation at $t=0$ is required. For $t>0$, $√t>0$, while at the integration endpoint $s=t$ one has $√(t-s)=0$; total real division makes both $1/√(t-s)$ and $(B(t)-B(s))/√(t-s)=0/0$ equal to $0$ there, so the pointwise integrand at that endpoint is $0$, and in any case a single endpoint has Lebesgue measure zero. No continuity, measurability, integrability, sign, normalization, or support condition is assumed directly of $f$. Under the total convention used for the integral, a non-integrable weighted integrand has integral $0$; since the right-hand side is strictly positive for every $t>0$, any $f$ satisfying the predicate must nevertheless make the displayed weighted integrand integrable on $(0,t]$ for every positive $t$. The predicate is insensitive to $f$ on $(-\infty,0]$ and to changes of $f$ on Lebesgue-null subsets of $(0,\infty)$. It includes the degenerate parameter cases $b₀=0$ and $c=0$, permits negative $b₀$ and negative $c$, and asserts neither the existence nor the uniqueness of such an $f$.