Divergence-form bilinear form (dependency-chain step 5)

We treat the symmetric, transport-free, zeroth-order-free case first: the bilinear form of the Laplacian, B[U, V] = ∑ᵢ ⟪∂ᵢu, ∂ᵢv⟫_{L²}, i.e. the coefficient matrix is the identity and c = 0. In the graph encoding of Sobolev/Basic.lean the i-th weak partial of U ∈ H₀¹(Ω) is the coordinate U (i.succ), so

B[U, V] = ∑ i, ⟪(↑U) i.succ, (↑V) i.succ⟫.

• Continuity (β = d): each coordinate norm is bounded by the ambient H¹ norm.
• Coercivity (α = 1 / (C_P + 1)): B[U, U] = ∑ᵢ ‖∂ᵢu‖² is the Dirichlet energy, and the density Poincaré inequality poincare_H01 controls the function part ‖u‖² by that energy, so B dominates the full H¹ norm.

This is the γ = 0 case of the coercivity examples closing Evans §6.2.2: coercivity is immediate from the energy identity plus Poincaré, with no Gårding absorption. It is exactly the hypothesis the Lax-Milgram theorem (M6) consumes. The general elliptic matrix A and c ≥ 0 follow the same shape with A's ellipticity constant in place of 1 (cf. DeGiorgi WeakFormulation/CoefficientOperator.lean).

noncomputable def EllipticPdes.laplaceBilinₗ {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : ↥(Sobolev.H01 Ω) →ₗ[ℝ] ↥(Sobolev.H01 Ω) →ₗ[ℝ] ℝ

The bilinear form of the Laplacian as a bare bilinear map on H₀¹(Ω): B[U, V] = ∑ᵢ ⟪∂ᵢu, ∂ᵢv⟫_{L²}.

Equations

• EllipticPdes.laplaceBilinₗ Ω = LinearMap.mk₂ ℝ (fun (U V : ↥(EllipticPdes.Sobolev.H01 Ω)) => ∑ i : Fin d, inner ℝ ((↑U).ofLp i.succ) ((↑V).ofLp i.succ)) ⋯ ⋯ ⋯ ⋯

noncomputable def EllipticPdes.laplaceBilin {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : ↥(Sobolev.H01 Ω) →L[ℝ] ↥(Sobolev.H01 Ω) →L[ℝ] ℝ

The bilinear form of the Laplacian on H₀¹(Ω) as a bounded (continuous) bilinear form, with operator-norm bound d.

Equations

• EllipticPdes.laplaceBilin Ω = (EllipticPdes.laplaceBilinₗ Ω).mkContinuous₂ ↑d ⋯

@[simp]

theorem EllipticPdes.laplaceBilin_apply {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (U V : ↥(Sobolev.H01 Ω)) : ((laplaceBilin Ω) U) V = ∑ i : Fin d, inner ℝ ((↑U).ofLp i.succ) ((↑V).ofLp i.succ)

Simp lemma: laplaceBilin Ω U V = ∑ i, ⟪(U : H1amb Ω) i.succ, (V : H1amb Ω) i.succ⟫.

theorem EllipticPdes.laplaceBilin_self {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (U : ↥(Sobolev.H01 Ω)) : ((laplaceBilin Ω) U) U = ∑ i : Fin d, ‖(↑U).ofLp i.succ‖ ^ 2

The Dirichlet energy identity: B[U, U] = ∑ᵢ ‖∂ᵢu‖².

theorem EllipticPdes.laplaceBilin_coercive_const {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) (U : ↥(Sobolev.H01 Ω)) : 1 / (CP + 1) * ‖U‖ * ‖U‖ ≤ ((laplaceBilin Ω) U) U

Quantitative coercivity of the bilinear form of the Laplacian. Given the test-function Poincaré bound with constant C_P ≥ 0, that form dominates the full H¹ norm with the explicit constant 1 / (C_P + 1): the density Poincaré inequality controls the function part by the Dirichlet energy. This is the constant-level form of [laplaceBilin_coercive]; the explicit constant feeds the Lax-Milgram a-priori estimate [norm_weak_solution_le].

theorem EllipticPdes.laplaceBilin_coercive {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) : IsCoercive (laplaceBilin Ω)

Coercivity of the bilinear form of the Laplacian. Given the test-function Poincaré bound with constant C_P ≥ 0, that form is coercive on H₀¹(Ω) with constant 1 / (C_P + 1): the density Poincaré inequality controls the function part by the Dirichlet energy, so B[U, U] dominates the full H¹ norm.

Lax-Milgram

theorem EllipticPdes.lax_milgram {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : H →L[ℝ] H →L[ℝ] ℝ} (hB : IsCoercive B) (f : H →L[ℝ] ℝ) : ∃! u : H, ∀ (v : H), (B u) v = f v

Lax-Milgram Theorem. If (H, (·, ·)) is a Hilbert space and B : H × H → ℝ is a bounded coercive (i.e. B(u, u) ≥ β‖u‖²_H) bilinear form, and f is a continuous linear functional on H, then there is a unique u ∈ H such that B(u, v) = ⟪f, v⟫ for all v ∈ H.

Guo, Partial Differential Equations (Course Lecture Notes), Theorem VII.3.1, p. 49. The two hypotheses are boundedness and coercivity, and B is otherwise arbitrary, which is Remark VII.3.2 there.

Boundedness is the continuity the type H →L[ℝ] H →L[ℝ] ℝ states, and coercivity is IsCoercive. Mathlib's IsCoercive.continuousLinearEquivOfBilin supplies the equivalence B♯ with ⟪B♯ u, v⟫ = B[u, v]; the step taken here is from that equivalence to solvability against a functional, by Riesz representation of f.

Lax-Milgram a-priori estimate

theorem EllipticPdes.norm_weak_solution_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : H →L[ℝ] H →L[ℝ] ℝ} {α : ℝ} (hα : 0 < α) (hcoer : ∀ (U : H), α * ‖U‖ * ‖U‖ ≤ (B U) U) {f : H →L[ℝ] ℝ} {u : H} (hu : ∀ (v : H), (B u) v = f v) : ‖u‖ ≤ α⁻¹ * ‖f‖

Lax-Milgram a-priori estimate. If the bilinear form B satisfies the quantitative coercivity bound α ‖U‖² ≤ B[U, U] with α > 0, then any weak solution u of B[u, v] = f v obeys ‖u‖ ≤ α⁻¹ ‖f‖: coercivity gives α ‖u‖² ≤ B[u, u] = f u ≤ ‖f‖ ‖u‖, and dividing by ‖u‖ gives the bound. This is the Hilbert-space a-priori estimate underlying the Lax-Milgram theorem (Evans §6.2.1, Theorem 1, step 3): β ‖u‖ ≤ ‖Au‖.

L² right-hand sides as functionals on H₀¹

noncomputable def EllipticPdes.l2Functional {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : Sobolev.L2D Ω) : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ

A right-hand side f ∈ L²(Ω) as a continuous linear functional on H₀¹(Ω): v ↦ ⟪f, v₀⟫_{L²}, the weak pairing ⟨f, v⟩ = ∫_Ω f · v₀. This is the embedding L²(Ω) ⊆ H⁻¹(Ω) (Evans §5.9.1, Theorem 1(iii)) through which the classical Dirichlet problem Lu = f, f ∈ L²(Ω), enters the abstract Lax-Milgram statement.

Equations

• EllipticPdes.l2Functional Ω f = ((innerSL ℝ) f ∘SL PiLp.proj 2 (fun (x : Fin (d + 1)) => EllipticPdes.Sobolev.L2D Ω) 0) ∘SL (EllipticPdes.Sobolev.H01 Ω).subtypeL

@[simp]

theorem EllipticPdes.l2Functional_apply {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : Sobolev.L2D Ω) (V : ↥(Sobolev.H01 Ω)) : (l2Functional Ω f) V = inner ℝ f ((↑V).ofLp 0)

Simp lemma: l2Functional Ω f V = ⟪f, (V : H1amb Ω) 0⟫.

theorem EllipticPdes.l2Functional_eq_integral {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : Sobolev.L2D Ω) (V : ↥(Sobolev.H01 Ω)) : (l2Functional Ω f) V = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑V).ofLp 0) x

The L² pairing is the integral ⟨f, v⟩ = ∫_Ω f · v₀.

theorem EllipticPdes.norm_l2Functional_le {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : Sobolev.L2D Ω) : ‖l2Functional Ω f‖ ≤ ‖f‖

The embedding L²(Ω) ⊆ H⁻¹(Ω) is a contraction: ‖⟨f, ·⟩‖_{H⁻¹} ≤ ‖f‖_{L²}, since ‖v₀‖_{L²} ≤ ‖V‖_{H¹} in the graph encoding.