TheoremStatement: Literature-sourcedProof: 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.

Energy continuous dependence for the forced wave equation

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ , $T > 0$ and let $u \in C^{2}$ solve the forced equation $□_{c} u = f$ either on $R^{n} \times [0, T)$ or on $U \times [0, T)$ with $U$ a bounded $C^{1}$ domain and homogeneous Dirichlet boundary data; assume the total energy $E (t) = \int_{Ω} e (x, t) d x$ (with $Ω = R^{n}$ , respectively $Ω = U$ ) is finite and continuous on $[0, T)$ , differentiable on $(0, T)$ with the energy identity

$E^{'} (t) = (f (t), u_{t} (t)) : = \int_{Ω} f (x, t) u_{t} (x, t) d x,$

which is what differentiating the energy and inserting The local wave-energy conservation law with vanishing boundary flux gives, and assume that $t \mapsto ∥ f (t) ∥_{2}$ is continuous on $[0, T)$ (Cauchy-Schwarz inequality for $L^{2}$ ). Then for every $t \in [0, T)$

$\sqrt{2 E (t)} \leq \sqrt{2 E (0)} + \int_{0}^{t} ∥ f (s) ∥_{2} d s, hence E (t)^{1 / 2} \leq E (0)^{1 / 2} + \int_{0}^{t} ∥ f (s) ∥_{2} d s .$

This is stability of the classical solution with the sharp $L_{t}^{1} L_{x}^{2}$ forcing constant, not only conservation; the second display uses $1 / \sqrt{2} \leq 1$ .

Facts & Assumptions

Given: ${A C}_{ω}$ ; a finite continuous energy $E : [0, T) \to [0, \infty)$ with $E^{'} (t) = (f (t), u_{t} (t))$ on $(0, T)$ and $E (t) = \frac{1}{2} ∥ u_{t} (t) ∥_{2}^{2} + \frac{c^{2}}{2} ∥ D u (t) ∥_{2}^{2}$ ; a continuous map $t \mapsto ∥ f (t) ∥_{2}$ . Write $w (t) : = ∥ f (t) ∥_{2}$ .

[F1]

Cauchy–Schwarz in $L^{2}$ : $∣ \int g h d μ ∣ \leq ∥ g ∥_{2} ∥ h ∥_{2}$ for $g, h \in L^{2} (μ)$ . (Cauchy-Schwarz inequality for $L^{2}$ )

[F2]

Monotonicity from the derivative: a function continuous on an interval that is differentiable at every interior point with derivative $\leq 0$ there is nonincreasing. (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed)

[F3]

Chain rule for composites of totally differentiable maps. (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ )

[F4]

For every real $α$ , $s \mapsto s^{α}$ is continuous on $(0, \infty)$ and differentiable there with derivative $α s^{α - 1}$ . (Continuity and derivatives of positive-base real powers)

[F5]

First fundamental theorem: the integral function of a function continuous at a point has derivative equal to the integrand there. (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive)

[F6]

Continuous functions on a closed bounded interval are integrable, and on such an interval Darboux, Riemann and Lebesgue integrals of a continuous function agree. (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ , A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral)

Proof

1.1givenF3F4algebra

The regularised energy: for $ε > 0$ define $φ_{ε} (t) : = \sqrt{2 E (t) + ε^{2}}$ on $[0, T)$ . The radicand is positive, so by the chain rule [F3] and the power rule [F4] with $α = \frac{1}{2}$ , the function $φ_{ε}$ is continuous on $[0, T)$ and differentiable on $(0, T)$ with $φ_{ε}^{'} (t) = \frac{2 E^{'} (t)}{2 \sqrt{2 E (t) + ε^{2}}} = \frac{(f (t), u_{t} (t))}{φ_{ε} (t)}$ .

2.1givenstep 1.1F1algebra

An upper bound for the derivative: by Cauchy–Schwarz [F1], $(f (t), u_{t} (t)) \leq ∣ (f (t), u_{t} (t)) ∣ \leq ∥ f (t) ∥_{2} ∥ u_{t} (t) ∥_{2}$ , and since $2 E (t) = ∥ u_{t} (t) ∥_{2}^{2} + c^{2} ∥ D u (t) ∥_{2}^{2} \geq ∥ u_{t} (t) ∥_{2}^{2}$ we have $∥ u_{t} (t) ∥_{2} \leq \sqrt{2 E (t)} \leq φ_{ε} (t)$ ; hence $φ_{ε}^{'} (t) \leq ∥ f (t) ∥_{2} = w (t)$ for every $t \in (0, T)$ .

3.1givenstep 2.1F2F5F6algebra

Monotonicity of the defect: the function $W (t) : = \int_{0}^{t} w (s) d s$ is, by the continuity of $w$ and [F6], the integral function of a continuous integrand, so by [F5] it is differentiable with $W^{'} = w$ ; hence $ψ : = φ_{ε} - W$ is continuous on $[0, T)$ , differentiable on $(0, T)$ , and $ψ^{'} = φ_{ε}^{'} - w \leq 0$ there by step 2.1; [F2] makes $ψ$ nonincreasing, so for every $t \in [0, T)$ one has $φ_{ε} (t) \leq φ_{ε} (0) + \int_{0}^{t} w (s) d s = \sqrt{2 E (0) + ε^{2}} + \int_{0}^{t} ∥ f (s) ∥_{2} d s$ .

4.1givenstep 3.1F4algebra∎

Letting $ε ↓ 0$ : by the continuity of the square root [F4] and $0 \leq E (t) < \infty$ , $φ_{ε} (t) \to \sqrt{2 E (t)}$ and $φ_{ε} (0) \to \sqrt{2 E (0)}$ , so the inequality of step 3.1 passes to the limit and gives $\sqrt{2 E (t)} \leq \sqrt{2 E (0)} + \int_{0}^{t} ∥ f (s) ∥_{2} d s$ ; dividing by $\sqrt{2} \geq 1$ gives $E (t)^{1 / 2} \leq E (0)^{1 / 2} + \int_{0}^{t} ∥ f (s) ∥_{2} d s$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

102 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)