General divergence-form bilinear form (general elliptic matrix A)

We generalise the Poisson form ∑ᵢ ⟪∂ᵢu, ∂ᵢv⟫ of BilinearForm.lean to the symmetric second-order divergence-form operator L u = -Dⱼ(aᵢⱼ Dᵢu) with a measurable, bounded, uniformly elliptic coefficient matrix A (Evans §6.1.1: the divergence-form operator and the uniform ellipticity condition):

B_A[U, V] = ∑ᵢ ∑ⱼ ⟪aᵢⱼ ∂ᵢu, ∂ⱼv⟫_{L²}.

• Continuity (β = d² Λ): coefficient actions have operator norm ≤ Λ, and coordinate norm is bounded by the ambient H¹ norm.
• Energy identity / lower bound (bilin_self_ge): B_A[U, U] = ∫_Ω ∑ᵢⱼ aᵢⱼ ∂ᵢu ∂ⱼu, and pointwise ellipticity ∑ᵢⱼ aᵢⱼ ξᵢ ξⱼ ≥ λ |ξ|² integrates to B_A[U, U] ≥ λ · ‖∇u‖².
• Coercivity (α = λ / (C_P + 1)): the density Poincaré inequality poincare_H01 controls the function part, so B_A dominates the full H¹ norm.

This is the closing Examples remark of Evans §6.2.2: the symmetric, transport-free, c = 0 case where γ = 0 in the Gårding inequality and coercivity is immediate from ellipticity plus Poincaré. It mirrors the technique of DeGiorgi WeakFormulation/CoefficientOperator.lean (coeffBilinSubmodule_coercive) on our scalar PiLp Sobolev encoding.

Integrability helpers for products of L² classes

theorem EllipticPdes.Sobolev.integrable_sq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (p : L2D Ω) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑p x ^ 2) (MeasureTheory.volume.restrict Ω)

The square of an L² class is integrable.

theorem EllipticPdes.Sobolev.sq_integral_eq_norm_sq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (p : L2D Ω) : ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑p x ^ 2 = ‖p‖ ^ 2

∫_Ω (p)² = ‖p‖² for an L² class p.

theorem EllipticPdes.Sobolev.EllipticCoeff.integrable_triple {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (i j : Fin d) (p q : L2D Ω) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j * ↑↑p x * ↑↑q x) (MeasureTheory.volume.restrict Ω)

The triple product aᵢⱼ · p · q of bounded coefficient and two L² classes is integrable on Ω.

General divergence-form bilinear form

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

The general divergence-form bilinear form as a bare bilinear map on H₀¹(Ω): B_A[U, V] = ∑ᵢⱼ ⟪aᵢⱼ ∂ᵢu, ∂ⱼv⟫.

Equations

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

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

The general divergence-form bilinear form as a bounded (continuous) bilinear form, with operator-norm bound d² Λ.

Equations

• A.bilin Ω = (A.bilinₗ Ω).mkContinuous₂ (↑d ^ 2 * A.Λ) ⋯

@[simp]

theorem EllipticPdes.Sobolev.EllipticCoeff.bilin_apply {d : ℕ} (A : EllipticCoeff d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (U V : ↥(H01 Ω)) : ((A.bilin Ω) U) V = ∑ i : Fin d, ∑ j : Fin d, inner ℝ ((A.actL i j) ((↑U).ofLp i.succ)) ((↑V).ofLp j.succ)

Simp lemma: A.bilin Ω U V = ∑ i, ∑ j, ⟪A.actL i j (∂ᵢu), (∂ⱼv)⟫.

theorem EllipticPdes.Sobolev.EllipticCoeff.bilin_self_ge {d : ℕ} (A : EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (U : ↥(H01 Ω)) : A.lam * ∑ i : Fin d, ‖(↑U).ofLp i.succ‖ ^ 2 ≤ ((A.bilin Ω) U) U

Energy lower bound from ellipticity: B_A[U, U] ≥ λ · ∑ᵢ ‖∂ᵢu‖².

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

Coercivity of the general elliptic form (the closing Examples remark of Evans §6.2.2, γ = 0). Given the test-function Poincaré bound with constant C_P ≥ 0, the symmetric uniformly elliptic divergence form B_A is coercive on H₀¹(Ω) with constant λ / (C_P + 1).