ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

The heat flow of an interval indicator is a difference of Gaussian tails

Example

Assume Countable Choice. Let $n = 1$ and let $f = 1_{(a, b)}$ for real $a < b$ . Then $f \in L^{p} (R)$ for every $1 \leq p \leq \infty$ and, for every $t > 0$ and $x \in R$ , $H_{t} f (x) = Φ ⁣ (\frac{b - x}{\sqrt{2 t}}) - Φ ⁣ (\frac{a - x}{\sqrt{2 t}}),$ where $Φ (u) = (2 π)^{- 1 / 2} \int_{- \infty}^{u} e^{- s^{2} / 2} d s$ is the standard normal distribution function. In particular $H_{t} f$ is $C^{\infty}$ on $R$ and strictly positive at every point for every $t > 0$ , while $f$ is discontinuous.

Facts & Assumptions

Given: Countable Choice, real $a < b$ , $t > 0$ and $x \in R$ .

[A1]

Countable Choice is the hypothesis carried by the evolution and change-of-variables suppliers below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For $t > 0$ the heat kernel is $Γ (z, t) = (4 π t)^{- 1 / 2} e^{- z^{2} / (4 t)} > 0$ , with unit mass (The heat kernel on $R^{n}$ and its causal extension, Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel).

[F2]

The indicator of a measurable set is measurable (An indicator function is measurable exactly when its set is measurable), so $f = 1_{(a, b)}$ is bounded and measurable, and for bounded measurable data $H_{t} f$ is the everywhere-defined absolutely convergent convolution $x \mapsto \int_{R} Γ (x - y, t) f (y) d y$ (The heat evolution $H_{t}$ of initial data); for $1 \leq p < \infty$ the class $H_{t} f$ also obeys the finite- $p$ theory (The heat Cauchy problem for $L^{p}$ data).

[F3]

For a $C^{1}$ diffeomorphism $T : U \to V$ of open sets and nonnegative measurable $ψ$ , $\int_{V} ψ (y) d y = \int_{U} ψ (T (s)) ∣ \det D T (s) ∣ d s$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F4]

$\int_{- \infty}^{\infty} e^{- u^{2}} d u = \sqrt{π}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ ).

[F5]

The standard normal density $φ (s) = (2 π)^{- 1 / 2} e^{- s^{2} / 2}$ is $C^{\infty}$ on $R$ : it is a scalar multiple of the composite of the quadratic map with the exponential, which is $C^{\infty}$ by The exponential function is smooth and $(\exp)^{'} = \exp$ and $C^{k}$ Euclidean maps are closed under componentwise algebra and composition.

[F6]

For continuous real $ψ$ on an interval $I$ with at least two elements and $0 \in I$ , the function $G (u) = \int_{0}^{u} ψ (s) d s$ is differentiable with $G^{'} = ψ$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ , existence clause).

Verification

technique · direct

1.1A1F2givenalgebra

Membership and setup: by [F2] the class $f = 1_{(a, b)}$ is bounded and measurable with $\int_{R} ∣ f ∣^{p} = b - a$ for every $1 \leq p < \infty$ and $∥ f ∥_{\infty} = 1$ , so $f$ lies in every $L^{p} (R)$ , $1 \leq p \leq \infty$ ; $H_{t} f$ is the everywhere-defined representative $H_{t} f (x) = (4 π t)^{- 1 / 2} \int_{a}^{b} e^{- (x - y)^{2} / (4 t)} d y$ of [F2].

1.2F4F5F6givenalgebra

Smoothness and strict positivity of $Φ$ : for every real $u$ the identity $Φ (u) = \frac{1}{2} + \int_{0}^{u} φ (s) d s$ holds with $φ$ as in [F5], because $φ$ is even and has total mass $\sqrt{2 π} (2 π)^{- 1 / 2} = 1$ by [F4]; the fundamental theorem [F6] gives $Φ^{'} = φ > 0$ for every real $u$ , while [F5] and induction give $Φ^{(m)} = φ^{(m - 1)}$ for every $m \geq 1$ , so $Φ$ is $C^{\infty}$ and strictly increasing on $R$ .

2.1step 1.1F1F3givenalgebra

Substitution: the map $s \mapsto y = x + \sqrt{2 t} s$ is a $C^{1}$ diffeomorphism of $R$ onto itself with $d y = \sqrt{2 t} d s$ and $(x - y)^{2} / (4 t) = s^{2} / 2$ , so the nonnegative-function substitution [F3] turns the interval $a < y < b$ into $(a - x) / \sqrt{2 t} < s < (b - x) / \sqrt{2 t}$ and gives $H_{t} f (x) = (4 π t)^{- 1 / 2} \sqrt{2 t} \int_{(a - x) / \sqrt{2 t}}^{(b - x) / \sqrt{2 t}} e^{- s^{2} / 2} d s = Φ ((b - x) / \sqrt{2 t}) - Φ ((a - x) / \sqrt{2 t})$ , since $(4 π t)^{- 1 / 2} \sqrt{2 t} = (2 π)^{- 1 / 2}$ .

2.2step 1.2F5givenalgebra

Consequences: since $a < b$ implies $(a - x) / \sqrt{2 t} < (b - x) / \sqrt{2 t}$ , strict monotonicity of $Φ$ in step 1.2 gives $H_{t} f (x) = Φ (\cdot) - Φ (\cdot) > 0$ at every $x$ , and the affine maps $x \mapsto (a - x) / \sqrt{2 t}$ and $x \mapsto (b - x) / \sqrt{2 t}$ are $C^{\infty}$ , so the composite $H_{t} f$ is $C^{\infty}$ on $R$ by the closure of smooth maps under composition in [F5]; the indicator $f$ is discontinuous at $a$ and $b$ .

3.1step 1.1step 2.1step 2.2given∎

Steps 1.1, 2.1 and 2.2 give the membership $f \in L^{p}$ for all $1 \leq p \leq \infty$ , the displayed difference-of-Gaussian-tails formula, strict positivity of $H_{t} f$ at every point of every positive time, and smoothness of $H_{t} f$ despite the discontinuity of $f$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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

Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #5: The Fundamental Solution for the Heat Equation (Fall 2011) (standard reference, not scraped)