The Dirichlet problem: existence and uniqueness of a weak solution #
Lane D, item 17 of TauCetiRoadmap/PDE/README.md asks for the first end-to-end existence
theorem of the roadmap: for a divergence-form operator
L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u
whose energy form is coercive on H¹₀(Ω), the homogeneous Dirichlet problem L u = f in Ω,
u = 0 on ∂Ω, has a unique weak solution. This file assembles that theorem out of pieces
that are already in place: the bundled energy form TauCeti.PDE.energyFormH1L0 and its lower
bounds from TauCeti/Analysis/PDE/EnergyForm/Sobolev.lean, and the variational form of
Lax--Milgram IsCoercive.existsUnique_forall_eq from
TauCeti/Analysis/InnerProductSpace/LaxMilgram.lean.
The weak formulation #
A weak solution is a function u ∈ H¹₀(Ω) satisfying
a(u, v) = ∫_Ω f v for every v ∈ H¹₀(Ω),
which is TauCeti.PDE.IsWeakSolutionDirichlet. Two hypotheses are hidden in that sentence and
neither is a boundary-regularity assumption. The homogeneous boundary condition is carried by
membership in H¹₀(Ω) = W^{1,2}_0(Ω), the closure of C_c^∞(Ω), so no trace operator and no
regularity of ∂Ω is needed to state it. The right-hand side is an L²(Ω) function paired
against the value component of the test function, which is what makes it a continuous linear
functional on H¹₀(Ω): TauCeti.PDE.dirichletForcing, of norm at most ‖f‖_{L²} because the
value component of a Sobolev jet is dominated by the graph norm.
Where coercivity comes from #
Lax--Milgram needs IsCoercive, that is ∃ C > 0, ∀ u, C‖u‖‖u‖ ≤ a(u, u), and the energy-form
file supplies exactly such diagonal lower bounds without packaging them.
TauCeti.PDE.isCoercive_energyFormH1L0 converts any of them, and the two geometric routes of
that file are instantiated here: a domain trapped between two hyperplanes and a domain contained
in a ball, whose Poincaré constants are the slab width t - s and the diameter bound 2R. In
both cases the drift smallness condition βP < λ is what makes the resulting constant positive,
and with no drift it is vacuous.
A mass floor δ satisfying β² < 4λδ gives another route. Choose 0 < ε < λ with
β² < 4εδ; the coercivity constant is min (λ - ε) (δ - β²/(4ε)), on any open domain,
including all of Euclidean space. The theorem
TauCeti.PDE.UniformlyEllipticOn.existsUnique_isWeakSolutionDirichlet_of_mass_lower_bound
therefore needs no geometric or Poincaré hypothesis. These are sufficient conditions; when
coercivity is unavailable the Fredholm alternative (Lane D, item 18) replaces Lax--Milgram.
The -Δ payoff #
Specialising to a = 1, b = 0, c = 0 on a ball gives
TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_laplacian_of_subset_ball: the Poisson problem
-Δu = f in Ω, u = 0 on ∂Ω, has a unique weak solution whenever Ω is contained in a
ball. Unfolded through TauCeti.PDE.isWeakSolutionDirichlet_one_zero_zero_iff the variational
equation reads ∫_Ω ∇v · ∇u = ∫_Ω f v, the classical weak form of Poisson's equation. This is
the existence half of the roadmap's "end-to-end existence" acceptance criterion; the smoothness
half is Lane E and the identification with the Newtonian potential is Lane C.
A priori bound #
TauCeti.PDE.norm_le_of_isWeakSolutionDirichlet records the energy estimate ‖u‖_{H¹} ≤ ‖f‖/C
attached to a coercivity constant C. It is proved for every weak solution rather than for
the constructed one, so it is available before, and independently of, uniqueness.
Main declarations #
TauCeti.PDE.dirichletForcing: theL²right-hand side as a continuous linear functional onH¹₀(Ω), withTauCeti.PDE.norm_dirichletForcing_le.TauCeti.PDE.IsWeakSolutionDirichlet: the weak formulation ofL u = finΩ,u = 0on∂Ω.TauCeti.PDE.isWeakSolutionDirichlet_iff_forall_testFunction: for bounded coefficients it is enough to test the weak formulation againstC_c^∞(Ω).TauCeti.PDE.isCoercive_energyFormH1L0: a diagonal lower bound packaged asIsCoercive.TauCeti.PDE.weakSolutionDirichletandTauCeti.PDE.existsUnique_isWeakSolutionDirichlet: the Lax--Milgram solution and the existence-and-uniqueness theorem.TauCeti.PDE.norm_le_of_isWeakSolutionDirichlet: the energy estimate‖u‖ ≤ ‖f‖/C.TauCeti.PDE.UniformlyEllipticOn.existsUnique_isWeakSolutionDirichlet_of_mass_lower_bound: existence and uniqueness on an arbitrary open domain when the potential absorbs the drift.TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_of_subset_slabandTauCeti.PDE.existsUnique_isWeakSolutionDirichlet_of_subset_ball: existence and uniqueness under the geometric hypotheses that make the energy form coercive.TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_laplacian_of_subset_ball: the Poisson problem-Δu = fon a ball-contained domain.
References #
Lane D, item 17 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial Differential
Equations, Section 6.2.2 (existence of weak solutions); D. Gilbarg and N. Trudinger, Elliptic
Partial Differential Equations of Second Order, Chapter 8, Theorem 8.3.
Shortcut normed group instance on H¹₀(Ω), the separated form of the seminorm; the
inner-product shortcut below needs it and does not find it on its own.
Instances For
Shortcut inner-product instance on H¹₀(Ω): the Hilbert structure Lax--Milgram runs on,
inherited from the L² jet space through the same two closed subspaces.
Instances For
The forcing functional #
The right-hand side of the Dirichlet problem as a continuous linear functional on
H¹₀(Ω): an L²(Ω) function f acts by v ↦ ∫_Ω f v, pairing against the value component of
the Sobolev jet. Continuity is automatic from the construction, the value map
TauCeti.W1p0.valueL being continuous and the pairing being the L² inner product.
Equations
Instances For
The forcing functional is the L² inner product against the value component.
The forcing functional written as the integral ∫_Ω f v it names.
The forcing functional is bounded by the L² norm of its density, because the value
component of a Sobolev jet is dominated by the graph norm.
The operator norm of the forcing functional is at most ‖f‖_{L²(Ω)}.
The weak formulation #
The weak formulation of the homogeneous Dirichlet problem. u ∈ H¹₀(Ω) is a weak
solution of L u = f in Ω, u = 0 on ∂Ω, for
L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u, when
a(u, v) = ∫_Ω f v for every test function v ∈ H¹₀(Ω).
The boundary condition is not a side condition here: it is membership of u in H¹₀(Ω), the
closure of C_c^∞(Ω), so no regularity of ∂Ω and no trace operator enters the statement.
Nothing is assumed about the coefficients; each theorem below names the hypotheses it uses.
Equations
- TauCeti.PDE.IsWeakSolutionDirichlet a b c f u = ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a b c ↑u ↑v = (TauCeti.PDE.dirichletForcing f) v
Instances For
Being a weak solution, written out as the integral identity a(u, v) = ∫_Ω f v.
Testing against test functions suffices. When the energy density is essentially bounded,
so that the energy form is continuous on H¹(Ω), u is a weak solution as soon as the weak
equation a(u, φ) = ∫_Ω f φ holds for every test function φ ∈ C_c^∞(Ω): both sides are
continuous in the test function, and H¹₀(Ω) is the closure of C_c^∞(Ω).
The energy estimate. Any weak solution is bounded in H¹ by the L² norm of the data,
with the coercivity constant as the only other ingredient. The estimate is stated for every
weak solution, so it does not presuppose uniqueness.
Coercivity and Lax--Milgram #
A diagonal lower bound is coercivity. The energy-form file proves bounds of the shape
C‖u‖² ≤ a(u, u); this packages one, together with positivity of its constant, as the
IsCoercive hypothesis of Mathlib's Lax--Milgram theorem.
The weak solution of the Dirichlet problem, produced by Lax--Milgram from coercivity of
the energy form. It is characterised by
TauCeti.PDE.isWeakSolutionDirichlet_weakSolutionDirichlet together with
TauCeti.PDE.eq_weakSolutionDirichlet.
Equations
- TauCeti.PDE.weakSolutionDirichlet hcoeff hcoercive f = hcoercive.solutionOfFunctional (TauCeti.PDE.dirichletForcing f)
Instances For
The Lax--Milgram solution is a weak solution of the Dirichlet problem.
A weak solution of the Dirichlet problem is the Lax--Milgram solution.
Existence and uniqueness of the weak solution of the Dirichlet problem. For a
divergence-form operator whose energy form is bounded and coercive on H¹₀(Ω), and for every
f ∈ L²(Ω), there is exactly one u ∈ H¹₀(Ω) with
a(u, v) = ∫_Ω f v for all v ∈ H¹₀(Ω).
This is Lane D, item 17 of the PDE roadmap: the energy method's existence theorem, obtained by consuming Mathlib's Lax--Milgram theorem through the variational interface.
Existence and uniqueness of the weak solution, stated from a diagonal lower bound on the
energy form instead of a packaged IsCoercive hypothesis.
Existence and uniqueness on an arbitrary open domain under the mass-floor condition
β² < 4λδ. A Young parameter between β²/(4δ) and λ makes the gradient and value
coefficients positive. No domain boundedness, Poincaré inequality, or symmetry of the
principal coefficient is required.
The Laplacian model #
The energy form of the Laplacian model -Δ (a = 1, no drift, no mass) is the Dirichlet
form ∫_Ω ∇v · ∇u.
The weak formulation of the Laplacian model -Δ is the classical one: u ∈ H¹₀(Ω) solves
-Δu = f weakly exactly when ∫_Ω ∇v · ∇u = ∫_Ω f v for every v ∈ H¹₀(Ω).
Existence on a slab- or ball-contained domain #
Existence and uniqueness for a domain trapped in a slab. If Ω ⊆ ℝ^{n+1} lies between
the hyperplanes xᵢ = s and xᵢ = t, the principal part is uniformly elliptic with constants
λ ≤ Λ, the drift is bounded by β, the mass coefficient is bounded by γ and nonnegative,
and the drift is small in the sense β(t - s) < λ, then the Dirichlet problem has exactly one
weak solution for every f ∈ L²(Ω). The Poincaré constant of the slab is its width, and the
domain need not be bounded: boundedness in one direction is enough.
Existence and uniqueness for a domain inside a ball. For Ω ⊆ B(z, R) ⊆ ℝ^{n+1} with a
uniformly elliptic principal part, a drift bounded by β, a bounded nonnegative mass
coefficient and the smallness condition 2βR < λ, the Dirichlet problem has exactly one weak
solution for every f ∈ L²(Ω). The Poincaré constant used is the diameter bound 2R, not the
sharp one, so the smallness condition is not sharp either.
The Poisson problem #
The Poisson problem on a ball-contained domain. For Ω ⊆ B(z, R) ⊆ ℝ^{n+1} and every
f ∈ L²(Ω) there is exactly one u ∈ H¹₀(Ω) solving -Δu = f in Ω, u = 0 on ∂Ω,
weakly. This is the constant-coefficient case a = 1, b = 0, c = 0 of
TauCeti.PDE.UniformlyEllipticOn.existsUnique_isWeakSolutionDirichlet_of_subset_ball, where the
drift smallness condition is vacuous; unfolded through
TauCeti.PDE.isWeakSolutionDirichlet_one_zero_zero_iff the equation reads
∫_Ω ∇v · ∇u = ∫_Ω f v. It is the existence half of the roadmap's end-to-end acceptance
criterion for the Dirichlet problem on a ball.