CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Heat-semigroup martingales

Statement

Assume the Axiom of Choice. Let $g : R \to R$ be bounded and Borel measurable, let $T > 0$ , and let $p_{t}$ and $P_{t}$ be the Brownian transition kernel and operators The Brownian transition semigroup. Define $M_{t} : = P_{T - t} g (B_{t}) (0 \leq t < T), M_{t} : = g (B_{T}) (t \geq T) .$ Then $M$ is a bounded martingale relative to the Brownian filtration, and for every $0 \leq t < T$ the function $u (t, x) : = P_{T - t} g (x)$ is smooth on $(0, T) \times R$ and solves the backward heat equation $\partial_{t} u + \frac{1}{2} \partial_{x}^{2} u = 0 (0 < t < T, x \in R) .$

Facts & Assumptions

Given: AC, a standard Brownian motion $B$ with its natural filtration and usual augmentation, a bounded Borel $g : R \to R$ , a fixed $T > 0$ , and $0 \leq t < T$ .

[F1]

Transition kernel and its properties. $P_{s} f (x) = \int_{R} f (y) p_{s} (x, y) d y$ for $s > 0$ , $P_{0} f = f$ , $p_{s} (x, y) = (2 π s)^{- 1 / 2} e^{- (y - x)^{2} / (2 s)}$ ; for a standard Brownian motion $P_{s} f (x) = E [f (x + B_{s})]$ , the semigroup identity $P_{r} P_{s} = P_{r + s}$ holds, each $P_{s}$ is a probability kernel with $∥ P_{s} f ∥_{\infty} \leq ∥ f ∥_{\infty}$ , and the kernel identity $\int p_{r} (x, z) p_{s} (z, y) d z = p_{r + s} (x, y)$ holds. The Brownian transition semigroup The Brownian kernels form a semigroup Brownian motion Standard normal and normal laws The standard normal density has total mass one

[F2]

Markov property. For deterministic $s, u \geq 0$ and bounded Borel $f$ , $E [f (B_{s + u}) ∣ F_{s}] = P_{u} f (B_{s})$ almost surely, for both the raw natural filtration and its usual augmentation. Markov property of Brownian motion Natural and usual augmented Brownian filtrations

[F3]

Tower property. For $H \subseteq G$ and integrable $X$ , $E [E [X ∣ G] ∣ H] = E [X ∣ H]$ almost surely. Tower property of conditional expectation Conditional expectation as an ae class Continuous-time adapted processes and martingales

[F4]

Differentiation under the integral sign. If $x \mapsto f (x, s)$ is integrable for each $s$ in an open interval, $s \mapsto f (x, s)$ is differentiable for almost every $x$ , the partial derivative is measurable in $x$ , and $∣ \partial_{s} f (x, s) ∣ \leq G (x)$ with $G$ integrable and independent of $s$ , then $\partial_{s} \int f (x, s) d μ (x) = \int \partial_{s} f (x, s) d μ (x)$ ; the same statement applies to the parameter $x$ of the kernel. Applied to the bounded $g$ and the Gaussian kernel with $s = T - t > 0$ , the derivative bounds of line 1.1 below are integrable majorants. Differentiation under the integral sign Dominated convergence

[F5]

Gaussian derivative bounds of every order. For $s > 0$ and $z = y - x$ one has $p_{s} (x, y) = (2 π s)^{- 1 / 2} e^{- z^{2} / (2 s)}$ . For all integers $a, b \geq 0$ , repeated differentiation gives $\partial_{s}^{a} \partial_{x}^{b} p_{s} (x, y) = s^{- a - b / 2} P_{a, b} (z / \sqrt{s}) p_{s} (x, y)$ for a polynomial $P_{a, b}$ ; this follows inductively because differentiating in $x$ differentiates the scaled variable and differentiating in $s$ differentiates both the power of $s$ and that variable. Since every polynomial times $e^{- r^{2} / 4}$ is bounded, $∣ \partial_{s}^{a} \partial_{x}^{b} p_{s} (x, y) ∣ \leq C_{a, b} s^{- a - b / 2} q_{s} (x, y)$ , where $q_{s} (x, y)$ is the Gaussian density in $y$ of variance $2 s$ . Thus on compact subintervals of $s > 0$ every mixed derivative has an integrable, locally uniform Gaussian majorant. In particular, $\partial_{x} p_{s} = (z / s) p_{s}$ , $\partial_{x x}^{2} p_{s} = ((z^{2} / s^{2}) - (1 / s)) p_{s}$ , and $\partial_{s} p_{s} = \frac{1}{2} \partial_{x x}^{2} p_{s}$ . The Brownian transition semigroup The standard normal density has total mass one Standard normal and normal laws

[F6]

AC bookkeeping. Choice is declared for the conditional-expectation and completeness interfaces. The Axiom of Choice

Proof

technique · direct

1.1

Kernel identities and derivative bounds: for every $a, b \geq 0$ , [F5] bounds $∣ g (y) \partial_{s}^{a} \partial_{x}^{b} p_{s} (x, y) ∣$ by $∥ g ∥_{\infty} C_{a, b} s^{- a - b / 2} q_{s} (x, y)$ . On a neighborhood of any $(s_{0}, x_{0})$ with $s_{0} > 0$ , these bounds admit one integrable Gaussian majorant, so every order of $s$ - and $x$ -differentiation may be passed successively through the integral by [F4]; the resulting derivative integrals are jointly continuous by the same domination argument. The low-order identity $\partial_{s} p_{s} = \frac{1}{2} \partial_{x x}^{2} p_{s}$ is included in [F5].

F4F5given

1.2

Martingale property: for $0 \leq t \leq T$ the Markov property [F2] with $s = t$ , $u = T - t$ and $f = g$ gives $E [g (B_{T}) ∣ F_{t}] = P_{T - t} g (B_{t}) = M_{t}$ almost surely; at $t = T$ this is the identity $M_{T} = g (B_{T})$ and at $t < T$ it is the defining formula. Hence $M$ is adapted on $[0, \infty)$ , because it is a deterministic function of $B_{t}$ before $T$ and the $F_{T}$ -measurable variable $g (B_{T})$ thereafter. For $0 \leq s \leq t \leq T$ , the tower property [F3] gives $E [M_{t} ∣ F_{s}] = M_{s}$ . If $s < T \leq t$ , then $M_{t} = M_{T}$ and the same identity follows from the preceding calculation with terminal time $T$ ; if $T \leq s \leq t$ , then $M_{s} = M_{t} = g (B_{T})$ is $F_{s}$ -measurable. Thus the martingale identity holds for every $0 \leq s \leq t < \infty$ .

F1F2F3

2.1

Boundedness: for $t < T$ , $∣ M_{t} ∣ = ∣ P_{T - t} g (B_{t}) ∣ \leq ∥ g ∥_{\infty}$ by [F1], and for $t \geq T$ , $∣ M_{t} ∣ = ∣ g (B_{T}) ∣ \leq ∥ g ∥_{\infty}$ ; so $M$ is a bounded martingale and in particular uniformly integrable.

F1step 1.2

2.2

Smoothness and the heat equation: fix $0 < t < T$ and put $s = T - t > 0$ ; then $u (t, x) = \int g (y) p_{s} (x, y) d y$ . Step 1.1 gives, for every $a, b \geq 0$ , the continuous mixed derivative $\partial_{t}^{a} \partial_{x}^{b} u (t, x) = (- 1)^{a} \int g (y) \partial_{s}^{a} \partial_{x}^{b} p_{s} (x, y) d y$ , so $u \in C^{\infty} ((0, T) \times R)$ . Taking $(a, b) = (1, 0)$ and $(0, 2)$ and using $\partial_{s} p_{s} = \frac{1}{2} \partial_{x x}^{2} p_{s}$ gives $\partial_{t} u + \frac{1}{2} \partial_{x x}^{2} u = - \int g \partial_{s} p_{s} + \frac{1}{2} \int g \partial_{x x}^{2} p_{s} = 0$ .

F4step 1.1

3.1

Boundary and consistency cases: at $t = 0$ the solution $u (0, \cdot) = P_{T} g$ is the positive-time smoothing of $g$ and the equation holds there; as $t ↑ T$ one has $s ↓ 0$ and the formula $u (t, x) = \int g (y) p_{s} (x, y) d y$ degenerates to the point mass in the limit, so no smoothness or equation is asserted at $t = T$ ; for $g \equiv c$ constant one has $u \equiv c$ and the equation holds with all derivatives zero; for $g$ nonnegative bounded, $u \geq 0$ ; the endpoint definition $M_{T} = g (B_{T})$ is what makes the martingale identity of step 1.2 hold at $t = T$ ; and AC enters only through [F6].

F1F6step 1.2step 2.2∎

Source notes

Lawler, Sections 3.3 and 3.6, computes backward-heat-equation martingales from the Markov property and the smoothness of the heat semigroup. The differentiation under the integral sign in step 3.1 is justified through the explicit Gaussian derivative majorants of [F5], not through an assumption of smoothness of $g$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gregory F. Lawler, Stochastic Calculus: An Introduction with Applications, Sections 3.3 and 3.6 (standard reference, not scraped)