Theorem 5.3, p. 21 — the dominating ODE with cubic F has a bounded solution for every T iff (i), (ii) or (iii)

Proved

UnifiedFBSDE.Cubic.theorem_5_3

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

blow-updominating-odefbsdeglobal-existencep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Consider the linear FBSDE (4.1) with constant coefficients and $\sigma_3=0$ , terminal coefficient $h\in\mathbb R$ , and its dominating ODE

y_t=h+\int_t^T F(y_s)\,ds,\qquad F(y)=f_1+[f_2+b_1+\sigma_1f_3]y+[b_2+f_3\sigma_2+b_3\sigma_1]y^2+\sigma_2b_3y^3. \tag{5.3–5.4}

Then (5.3) has a bounded solution on $[0,T]$ for every $T>0$ if and only if one of the following holds:

$F(h)\ge0$ and $F$ has a zero in $[h,\infty)$ ;
$F(h)\le0$ and $F$ has a zero in $(-\infty,h]$ ;
$\sigma_2b_3=0$ and $b_2+f_3\sigma_2+b_3\sigma_1=0$ .

This is a sharp, checkable criterion for the existence of a bounded solution of the dominating ODE on an arbitrarily long horizon. In the paper's framework that solution yields a regular decoupling field, and with it well-posedness of the linear FBSDE. In this sense the result marks the limits of solvability for general FBSDEs.

Formalization Note. "For arbitrary $T$ " is a universal quantifier over $T>0$ placed outside the existential over $y$ . A solution requires the integrand to be integrable on every $[t,T]$ (see the definition file). The page's "zero point in $[h,\infty)$ " is $\exists\,l\ge h$ with $F(l)=0$ , and similarly for $(-\infty,h]$ .

Preamble

import Mathlib
import Definitions.Def_UnifiedFBSDE_Cubic_Setting

Formal statement

namespace UnifiedFBSDE.Cubic

/-- Theorem 5.3, p. 21. -/
theorem theorem_5_3 (c : Coeffs) (h : ℝ) :
    (∀ T : ℝ, 0 < T → ∃ y : ℝ → ℝ, IsBoundedSolution (fun _ y => c.F y) h T y) ↔
      ((0 ≤ c.F h ∧ ∃ l : ℝ, h ≤ l ∧ c.F l = 0) ∨
        (c.F h ≤ 0 ∧ ∃ l : ℝ, l ≤ h ∧ c.F l = 0) ∨
        (c.σ₂ * c.b₃ = 0 ∧ c.b₂ + c.f₃ * c.σ₂ + c.b₃ * c.σ₁ = 0)) := by sorry

end UnifiedFBSDE.Cubic

Source

Ma, Wu, Zhang and Zhang, On well-posedness of forward–backward SDEs—a unified approach, arXiv:1110.4658v2, p. 21, Theorem 5.3

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph