Existence for linear parabolic equations #
Let ι : V →L[ℝ] H be a continuous linear map from a real Hilbert space V into a real inner
product space H, inducing H → V* (ContinuousLinearMap.gelfandDual). No injectivity or dense
range is assumed; with both, V ↪ H ↪ V* is a Gelfand triple. Consider on a time interval
(a, b) the abstract linear parabolic problem
u' + A(t) u = f, u(a) = u₀,
with A(t) : V →L[ℝ] V* bounded and satisfying Gårding's inequality
α ‖v‖² - β ‖ι v‖² ≤ A(t) v v, f ∈ L²(a, b; V*) and u₀ ∈ H. Testing the equation against a
C¹ function φ : ℝ → V with φ(b) = 0 and integrating the time derivative by parts turns it
into the variational formulation
∫ₐᵇ (A(t) u(t) φ(t) - ⟪ι u(t), ι φ'(t)⟫) dt = ∫ₐᵇ f(t) φ(t) dt + ⟪u₀, ι φ(a)⟫,
in which neither the time derivative of u nor its value at t = a appears: the initial
condition is carried by the boundary term ⟪u₀, ι φ(a)⟫. This term does not change when u₀ is
modified by an element of (range ι)ᗮ, so the formulation determines the initial value only
modulo (range ι)ᗮ; it encodes u(a) = u₀ itself only when ι has dense range, as it does for a
genuine Gelfand triple. This file proves that the variational formulation has a
solution u ∈ L²(a, b; V) (TauCeti.exists_memLp_forall_setIntegral_eq_add_inner).
When V is moreover separable, every solution u of the variational formulation is a weak
solution in the sense of TauCeti.HasWeakLineDerivOn.ae_eq_of_gelfandDual: its weak time
derivative is u' = f - A u ∈ L²(a, b; V*)
(TauCeti.hasWeakLineDerivOn_gelfandDual_of_forall_setIntegral_eq_add_inner), and the value at
t = a of a continuous representative of ι ∘ u agrees with u₀ modulo (range ι)ᗮ
(TauCeti.gelfandDual_eq_of_forall_setIntegral_eq_add_inner). For a Gelfand triple this gives
existence of a weak solution of u' + A(t) u = f, u(a) = u₀
(TauCeti.exists_hasWeakLineDerivOn_gelfandDual), which the energy estimate in
TauCeti.Analysis.PDE.Parabolic.EnergyEstimate shows to be unique when β ≥ 0. Separability
makes t ↦ A(t) u(t) strongly measurable as a function into V*
(MeasureTheory.MemLp.clm_apply_of_forall_aestronglyMeasurable, a consequence of Pettis'
theorem), which a weak derivative in L²(a, b; V*) needs.
The proof #
For coercive A(t) (the case β = 0) this is an application of Lions' representation theorem
(LinearMap.exists_forall_apply_eq_and_norm_le_of_coercive), with the Hilbert space
L²(a, b; V) for the solution and the C¹ functions φ with φ(b) = 0 for the test
functions. The left-hand side E(φ, u) is continuous in u ∈ L²(a, b; V): its integrand is
bounded by a multiple of ‖u(t)‖, and L²(a, b) ⊆ L¹(a, b) continuously. On the diagonal,
the fundamental theorem of calculus for t ↦ ‖ι φ(t)‖² and φ(b) = 0 give
E(φ, φ) = ∫ₐᵇ A(t) φ φ + ½ ‖ι φ(a)‖² ≥ α ‖φ‖²_{L²(V)} + ½ ‖ι φ(a)‖²,
so c p(φ)² ≤ E(φ, φ) for p(φ) = (‖φ‖²_{L²(V)} + ‖ι φ(a)‖²)^{1/2} and c = min α ½, and the
right-hand side is bounded by (‖f‖_{L²(V*)} + ‖u₀‖) p(φ) by Cauchy–Schwarz.
In general, u = e^{β (t - a)} w solves the problem exactly when w solves it for the coercive
operator A(t) + β ι* ι and the right-hand side e^{-β (t - a)} f.
The coefficient A is only assumed weakly measurable, t ↦ A(t) u v almost everywhere strongly
measurable on (a, b) for all u, v ∈ V as in Lions and Showalter, and essentially bounded by
Λ. This covers divergence-form operators with L^∞ coefficients, which are in general not
strongly measurable as maps into V →L[ℝ] V*. Measurability of t ↦ A(t) u(t) φ(t) for
u ∈ L²(a, b; V) then follows from
MeasureTheory.AEStronglyMeasurable.apply_of_forall_of_continuousAt, which approximates (u, φ)
with simple functions, so the variational existence theorem needs no separability of V.
For the weak derivative, test the variational formulation against φ(t) = ψ(t) v with ψ
smooth and compactly supported in (a, b). For the initial value, test it against
φ(t) = (b - t) / (b - a) v and integrate by parts against the primitive of u'.
Main declarations #
TauCeti.exists_memLp_forall_setIntegral_eq_add_inner: the variational formulation ofu' + A(t) u = f,u(a) = u₀, has a solution inL²(a, b; V).TauCeti.exists_memLp_forall_setIntegral_eq_add_inner_of_ae_eq: the same, with the hypotheses and the conclusion stated for bilinear functionalsB(t)that agree withA(t)for almost everyt.TauCeti.hasWeakLineDerivOn_gelfandDual_of_forall_setIntegral_eq_add_inner: a solution of the variational formulation has weak time derivativef - A u.TauCeti.gelfandDual_eq_of_forall_setIntegral_eq_add_inner: its continuous representative takes the initial valueu₀modulo(range ι)ᗮ.TauCeti.exists_hasWeakLineDerivOn_gelfandDual: existence of a weak solution ofu' + A(t) u = f,u(a) = u₀, in a Gelfand triple.TauCeti.exists_hasWeakLineDerivOn_gelfandDual_of_ae_eq: the same, with the hypotheses and the equation stated for bilinear functionalsB(t)that agree withA(t)for almost everyt.
References #
- J.-L. Lions, Équations différentielles opérationnelles et problèmes aux limites, Grundlehren 111, Springer, 1961.
- R. E. Showalter, Monotone Operators in Banach Space and Nonlinear Partial Differential Equations, Mathematical Surveys and Monographs 49, AMS, 1997, Chapter III, Section 2.
- L. C. Evans, Partial Differential Equations, 2nd ed., §7.1.2, which constructs weak solutions of second-order parabolic equations by the Galerkin method instead.
Existence for linear parabolic equations, in variational form. Let ι : V →L[ℝ] H
be any continuous linear map (neither injectivity nor dense range is assumed) with V a Hilbert
space, and let A(t) : V →L[ℝ] V* be weakly
measurable in t (t ↦ A(t) u v almost everywhere strongly measurable on (a, b) for all
u, v), bounded by Λ and satisfy
Gårding's inequality α ‖v‖² - β ‖ι v‖² ≤ A(t) v v with α > 0, for almost every
t ∈ (a, b). Then for every
f ∈ L²(a, b; V*) and u₀ ∈ H there is u ∈ L²(a, b; V) with
∫ₐᵇ (A(t) u(t) φ(t) - ⟪ι u(t), ι φ'(t)⟫) dt = ∫ₐᵇ f(t) φ(t) dt + ⟪u₀, ι φ(a)⟫
for every C¹ function φ : ℝ → V with φ(b) = 0. This is the weak formulation of
u' + A(t) u = f with initial value u₀, obtained by integrating ⟪u', φ⟫ by parts. Since u₀
enters only through ⟪u₀, ι φ(a)⟫, it is seen only modulo (range ι)ᗮ; the condition is
u(a) = u₀ itself when ι has dense range. No sign is imposed on
β.
TauCeti.exists_memLp_forall_setIntegral_eq_add_inner with the operators A(t) known only
through a family of bilinear functionals B(t) that they agree with for almost every t:
measurability, boundedness and Gårding's inequality are then hypotheses on B, and so is the
conclusion. This is the form in which a concrete parabolic problem supplies its operators.
The variational solution is a weak solution #
The variational formulation gives the weak time derivative. Let V be a separable Hilbert
space, let A(t) : V →L[ℝ] V* be weakly measurable and essentially bounded on (a, b), and let
f ∈ L²(a, b; V*). If u ∈ L²(a, b; V) satisfies the variational formulation
∫ₐᵇ (A(t) u(t) φ(t) - ⟪ι u(t), ι φ'(t)⟫) dt = ∫ₐᵇ f(t) φ(t) dt + ⟪u₀, ι φ(a)⟫
for every C¹ function φ : ℝ → V with φ(b) = 0, then u' = f - A u is the weak time
derivative of ι.gelfandDual ∘ ι ∘ u on (a, b): u is a weak solution of u' + A(t) u = f.
The variational formulation gives the initial value. In the setting of
TauCeti.hasWeakLineDerivOn_gelfandDual_of_forall_setIntegral_eq_add_inner, let a < b and let
w be a representative of ι ∘ u continuous on [a, b]. Then w a agrees with u₀ modulo
(range ι)ᗮ: ⟪w a, ι v⟫ = ⟪u₀, ι v⟫ for every v ∈ V.
Existence of weak solutions for linear parabolic equations. Let V ↪ H ↪ V* be a Gelfand
triple: V a separable Hilbert space, H a Hilbert space and ι : V →L[ℝ] H with dense range.
Let A(t) : V →L[ℝ] V* be weakly measurable (t ↦ A(t) u v almost everywhere strongly
measurable on (a, b) for all u, v), bounded by Λ and satisfy Gårding's inequality
α ‖v‖² - β ‖ι v‖² ≤ A(t) v v with α > 0, for almost every t ∈ (a, b). Then for every
f ∈ L²(a, b; V*) and u₀ ∈ H there is a weak solution of
u' + A(t) u = f, u(a) = u₀:
a u ∈ L²(a, b; V) such that u' = f - A u ∈ L²(a, b; V*) is the weak time derivative of
ι.gelfandDual ∘ ι ∘ u on (a, b), and a representative w of ι ∘ u continuous on [a, b]
with w a = u₀. For β ≥ 0 it is unique: see TauCeti.HasWeakLineDerivOn.eqOn_of_gelfandDual
and TauCeti.HasWeakLineDerivOn.ae_eq_of_gelfandDual.
TauCeti.exists_hasWeakLineDerivOn_gelfandDual with the operators A(t) known only through a
family of bilinear functionals B(t) that they agree with for almost every t, as in
TauCeti.exists_memLp_forall_setIntegral_eq_add_inner_of_ae_eq: measurability, boundedness and
Gårding's inequality are hypotheses on B, and the equation u' + A(t) u = f is stated tested
against every v ∈ V, as u'(t)(v) + B(t)(u(t), v) = f(t)(v) for almost every t.