The pointwise integrand of a divergence-form energy bilinear form

For a divergence-form operator L u = -∂ⱼ(aⁱʲ ∂ᵢ u) + bⁱ ∂ᵢ u + c u, the weak (energy) bilinear form is

a(u, v) = ∫_Ω (aⁱʲ ∂ᵢu ∂ⱼv + bⁱ ∂ᵢu v + c u v),

whose integrand at a point x depends only on the jets (u(x), ∇u(x)) and (v(x), ∇v(x)), that is, on pairs in ℝ × EuclideanSpace ℝ n. This file assembles the three pointwise coefficient forms already available

• the principal matrix form matrixBilinearForm (a x) (in TauCeti.Analysis.PDE.Ellipticity.Basic),
• the drift form driftForm (b x) and the mass form massForm (c x) (in TauCeti.Analysis.PDE.LowerOrder),

into a single bundled continuous bilinear form on jets, energyIntegrand (a x) (b x) (c x), matching (U, V) ↦ ⟨a(x) U.2, V.2⟩ + ⟪b(x), U.2⟫ V.1 + c(x) U.1 V.1, where U.2 = ∇u, U.1 = u. Integrating this jet form over Ω against the jets of u and v recovers the energy bilinear form, so this is the pointwise seed of Lane D's weak formulation.

The two estimates the energy method needs are proved pointwise, with their constants left explicit (never hidden in a ∃ C):

• boundedness: the operator norm of the jet form is at most Λ + β + γ, the sum of the ellipticity, drift, and mass constants;
• Gårding's inequality (pointwise): with a sign condition c ≥ 0 on the mass coefficient, the diagonal of the jet form is bounded below by (λ/2)‖∇u‖² − (β²/2λ)|u|², the integrand-level version of Gårding's a(u, u) ≥ α‖u‖²_{H¹} − K‖u‖²_{L²}. The drift is absorbed by Young's inequality, paid for out of half of the ellipticity floor.

Main declarations

• TauCeti.PDE.energyIntegrand: the bundled jet bilinear form of a divergence-form operator.
• TauCeti.PDE.energyIntegrand_apply, TauCeti.PDE.energyIntegrand_self: its value and its diagonal value.
• TauCeti.PDE.energyIntegrand_one_zero_zero_apply, TauCeti.PDE.energyIntegrand_one_zero_zero_self: the Laplacian model −Δ, whose jet form is the Dirichlet integrand ⟨∇u, ∇v⟩, with diagonal ‖∇u‖².
• TauCeti.PDE.energyIntegrand_one_zero_mass_apply, TauCeti.PDE.energyIntegrand_one_zero_mass_self: the shifted Laplacian model −Δ + c, whose jet form is ⟨∇u, ∇v⟩ + c u v.
• TauCeti.PDE.norm_energyIntegrand_apply_le_of_bounds, TauCeti.PDE.opNorm_energyIntegrand_le_of_bounds: pointwise boundedness with explicit constant Λ + β + γ.
• TauCeti.PDE.garding_energyIntegrand_self_of_bounds: the pointwise Gårding lower bound on the diagonal.

The main estimates take single coefficients and inline bounds (‖b₀‖ ≤ β, and so on).

@[instance_reducible]

noncomputable def TauCeti.PDE.energyFormDecidableEq {n : Type u_1} : DecidableEq n

Local classical decidable equality for finite coordinate indices in energy-form proofs.

Equations

• TauCeti.PDE.energyFormDecidableEq = Classical.decEq n

noncomputable def TauCeti.PDE.energyIntegrand {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) : ℝ × EuclideanSpace ℝ n →L[ℝ] ℝ × EuclideanSpace ℝ n →L[ℝ] ℝ

The pointwise weak-form (energy) integrand of a divergence-form operator L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u, as a bundled continuous bilinear form on jets (value, gradient) ∈ ℝ × EuclideanSpace ℝ n.

On jets U = (u, ∇u) and V = (v, ∇v) it evaluates to ⟨a ∇u, ∇v⟩ + ⟪b, ∇u⟫ v + c u v, the integrand of a(u, v). Bundling it as a ContinuousLinearMap lets it feed Mathlib's bounded-bilinear-form and Lax--Milgram APIs once the energy form is integrated over the Sobolev space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PDE.energyIntegrand_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand A b c) U) V = ((matrixBilinearForm A) V.2) U.2 + ((driftForm b) V.1) U.2 + ((massForm c) U.1) V.1

The jet form evaluates to ⟨a ∇u, ∇v⟩ + ⟪b, ∇u⟫ v + c u v on jets U, V.

theorem TauCeti.PDE.energyIntegrand_self {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) (U : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand A b c) U) U = A.toQuadraticForm' U.2.ofLp + inner ℝ b U.2 * U.1 + c * U.1 ^ 2

The diagonal of the jet form, the energy density ⟨a ∇u, ∇u⟩ + ⟪b, ∇u⟫ u + c u².

theorem TauCeti.PDE.energyIntegrand_one_zero_zero_apply {n : Type u_1} [Fintype n] (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand 1 0 0) U) V = V.2.ofLp ⬝ᵥ U.2.ofLp

The Laplacian model −Δ (a = 1, no drift, no mass) has jet form the Dirichlet integrand ⟨∇u, ∇v⟩.

theorem TauCeti.PDE.energyIntegrand_one_zero_zero_self {n : Type u_1} [Fintype n] (U : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand 1 0 0) U) U = ‖U.2‖ ^ 2

The diagonal of the Laplacian model's jet form is the Dirichlet energy density ‖∇u‖².

theorem TauCeti.PDE.energyIntegrand_one_zero_mass_apply {n : Type u_1} [Fintype n] (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand 1 0 c) U) V = V.2.ofLp ⬝ᵥ U.2.ofLp + c * U.1 * V.1

The shifted Laplacian model -Δ + c has jet form (U, V) ↦ ∇u · ∇v + c u v.

theorem TauCeti.PDE.energyIntegrand_one_zero_mass_self {n : Type u_1} [Fintype n] (c : ℝ) (U : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand 1 0 c) U) U = ‖U.2‖ ^ 2 + c * U.1 ^ 2

The shifted Laplacian model -Δ + c has diagonal jet density ‖∇u‖² + c u².

theorem TauCeti.PDE.norm_energyIntegrand_apply_le_of_bounds {n : Type u_1} [Fintype n] {Lam beta gamma : ℝ} (hLam : 0 ≤ Lam) {A : Matrix n n ℝ} {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (ha : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb : ‖b₀‖ ≤ beta) (hc : ‖c₀‖ ≤ gamma) (U V : ℝ × EuclideanSpace ℝ n) : ‖((energyIntegrand A b₀ c₀) U) V‖ ≤ (Lam + beta + gamma) * ‖U‖ * ‖V‖

Pointwise boundedness of the jet form with explicit constant Λ + β + γ: the principal, drift, and mass contributions are each controlled by the corresponding constant times the jet norms.

theorem TauCeti.PDE.opNorm_energyIntegrand_le_of_bounds {n : Type u_1} [Fintype n] {Lam beta gamma : ℝ} (hLam : 0 ≤ Lam) {A : Matrix n n ℝ} {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (ha : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb : ‖b₀‖ ≤ beta) (hc : ‖c₀‖ ≤ gamma) : ‖energyIntegrand A b₀ c₀‖ ≤ Lam + beta + gamma

The operator norm of the pointwise jet form is at most Λ + β + γ.

This finite-dimensional estimate is consumed after integration to prove boundedness of the Sobolev-space energy form; it is not itself the Lax--Milgram boundedness hypothesis.

theorem TauCeti.PDE.norm_energyIntegrand_one_zero_mass_apply_le {n : Type u_1} [Fintype n] (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ‖((energyIntegrand 1 0 c) U) V‖ ≤ (1 + ‖c‖) * ‖U‖ * ‖V‖

Pointwise boundedness of the shifted Laplacian jet form with constant 1 + ‖c‖.

theorem TauCeti.PDE.opNorm_energyIntegrand_one_zero_mass_le {n : Type u_1} [Fintype n] (c : ℝ) : ‖energyIntegrand 1 0 c‖ ≤ 1 + ‖c‖

Operator-norm boundedness of the shifted Laplacian jet form with constant 1 + ‖c‖.

theorem TauCeti.PDE.garding_energyIntegrand_self_of_bounds_with_parameter {n : Type u_1} [Fintype n] {lam beta eps : ℝ} (heps : 0 < eps) {A : Matrix n n ℝ} {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hQ : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hb : ‖b₀‖ ≤ beta) (hc : 0 ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : (lam - eps) * ‖U.2‖ ^ 2 - beta ^ 2 / (4 * eps) * U.1 ^ 2 ≤ ((energyIntegrand A b₀ c₀) U) U

The pointwise Gårding bound with a free positive Young parameter. The gradient coefficient is λ - ε, and the mass defect is β²/(4ε). No sign condition on λ - ε is needed.

theorem TauCeti.PDE.garding_energyIntegrand_self_of_bounds {n : Type u_1} [Fintype n] {lam beta : ℝ} (hlam : 0 < lam) {A : Matrix n n ℝ} {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hQ : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hb : ‖b₀‖ ≤ beta) (hc : 0 ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : lam / 2 * ‖U.2‖ ^ 2 - beta ^ 2 / (2 * lam) * U.1 ^ 2 ≤ ((energyIntegrand A b₀ c₀) U) U

Pointwise Gårding inequality. With a nonnegative mass coefficient (c ≥ 0), the diagonal of the jet form is bounded below by (λ/2)‖∇u‖² − (β²/2λ)|u|². The ellipticity floor λ‖∇u‖² pays for the drift term via Young's inequality, leaving half the floor and a mass defect proportional to β²/λ. Integrating over Ω this is Gårding's inequality a(u, u) ≥ (λ/2)‖∇u‖²_{L²} − (β²/2λ)‖u‖²_{L²}.