TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Quantitative residual error under strong monotonicity

Statement

Assume the Axiom of Choice.

Let $(V, H, J)$ be the evolution triple of Banach evolution triples and weak time derivatives, $1 < p < \infty$ , and assume $A : V \to V^{*}$ is strongly monotone with constant $μ > 0$ and exponent $p$ : $⟨ A (x) - A (y), x - y ⟩ \geq μ ∥ x - y ∥_{V}^{p} (x, y \in V) .$ Suppose $u, v \in L^{p} (0, T; V)$ have derivatives in $L^{p^{'}} (0, T; V^{*})$ and residual difference $R = (u^{'} + A (u)) - (v^{'} + A (v)) \in L^{p^{'}} (0, T; V^{*})$ . Then for every $t \in [0, T]$ , $∥ u (t) - v (t) ∥_{H}^{2} + μ \int_{0}^{t} ∥ u - v ∥_{V}^{p} \leq ∥ u (0) - v (0) ∥_{H}^{2} + 2 C_{μ, p} ∥ R ∥_{L^{p^{'}} (0, t; V^{*})}^{p^{'}},$ where both functions use their continuous $H$ representatives and $C_{μ, p} = \frac{1}{p^{'}} (2 / (μ p))^{1 / (p - 1)}$ . In particular, equal initial data and zero residual imply $u = v$ .

Facts & Assumptions

Given: The Axiom of Choice, the evolution triple, $1 < p < \infty$ , strong monotonicity with constant $μ$ , two functions in the stated evolution space, and their residual difference $R$ .

[F1]

Functions in $L^{p} (V)$ with derivative in $L^{p^{'}} (V^{*})$ have continuous $H$ representatives and satisfy the integrated Hilbert norm chain rule (The Banach evolution-space energy identity and H trace).

[F2]

Hölder's inequality applies to the dual pairing of $L^{p^{'}} (V^{*})$ and $L^{p} (V)$ (Holder's inequality for integrals, including the endpoint cases).

[F3]

For conjugate exponents $p, p^{'} > 1$ , Young's inequality is $a b \leq a^{p} / p + b^{p^{'}} / p^{'}$ for $a, b \geq 0$ (Young's inequality for conjugate real exponents).

[A1]

Strong monotonicity with exponent $p$ and constant $μ$ is the additional hypothesis of this theorem; it is not part of ordinary monotonicity in Coercive monotone p-growth diffusion fluxes.

[A2]

The Axiom of Choice licenses the energy chain rule through its absolutely continuous representative prerequisite (The Axiom of Choice).

Proof

1.1A1A2F1F2givenalgebra

Set $e = u - v$ . Subtracting the residual definitions gives $e^{'} + A (u) - A (v) = R$ in $L^{p^{'}} (0, T; V^{*})$ . By [F1], testing this identity against $e \in L^{p} (0, T; V)$ is integrable by [F2], and for every $t$ , $\frac{1}{2} ∥ e (t) ∥_{H}^{2} - \frac{1}{2} ∥ e (0) ∥_{H}^{2} + \int_{0}^{t} ⟨ A (u) - A (v), e ⟩ = \int_{0}^{t} ⟨ R, e ⟩ .$

2.1A1A2F1F2F3step 1.1givenalgebra∎

Strong monotonicity bounds the left integral below by $μ \int_{0}^{t} ∥ e ∥_{V}^{p}$ . Young's inequality [F3], applied to $(μ p / 2)^{1 / p} a$ and $(μ p / 2)^{- 1 / p} b$ , gives the scaled form $a b \leq \frac{μ}{2} a^{p} + \frac{1}{p^{'}} {(\frac{2}{μ p})}^{1 / (p - 1)} b^{p^{'}}$ gives $∣ ⟨ R, e ⟩ ∣ \leq \frac{μ}{2} ∥ e ∥_{V}^{p} + C_{μ, p} ∥ R ∥_{V^{*}}^{p^{'}}$ . Integrating and absorbing the first term yields $\frac{1}{2} ∥ e (t) ∥_{H}^{2} + \frac{μ}{2} \int_{0}^{t} ∥ e ∥_{V}^{p} \leq \frac{1}{2} ∥ e (0) ∥_{H}^{2} + C_{μ, p} ∥ R ∥_{L^{p^{'}} (0, t; V^{*})}^{p^{'}} .$ Multiplying by two proves the estimate. If $e (0) = 0$ and $R = 0$ , the nonnegative left side vanishes for every $t$ , hence $e (t) = 0$ in $H$ and $e = 0$ in $L^{p} (V)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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

Tomáš Roubíček, Nonlinear Partial Differential Equations with Applications, 2nd ed., Birkhäuser, 2005 (standard reference, not scraped)
Marvin Fritz, Monotone Operators in Nonlinear PDEs, JKU lecture notes, WS 2023/2024 (standard reference, not scraped)