Constant-coefficient energy forms on L² jets

Lane D of the PDE roadmap asks for the bounded bilinear energy form used by the weak formulation of a divergence-form equation. This file performs the functional-analytic bundling for constant coefficients. A pointwise jet form

(u, ∇u), (v, ∇v) ↦ (∇v)ᵀ A ∇u + v bᵀ ∇u + c u v

induces a continuous bilinear form on square-integrable value-gradient jets. The construction uses Mathlib's ContinuousLinearMap.lpPairing, which is the continuous Hölder pairing induced by a continuous bilinear map.

Variable coefficients will require the corresponding multiplication-operator construction. The constant-coefficient form here already includes the Dirichlet and shifted-Laplacian models and has the bounded-bilinear-map shape needed for a later Lax--Milgram application, after restriction to the intended Hilbert/Sobolev space and a proof of coercivity.

Main declarations

• TauCeti.PDE.energyFormLp: the constant-coefficient energy form on L² jets.
• TauCeti.PDE.energyFormLp_apply: its characterization as an integral.
• TauCeti.PDE.energyFormLp_one_zero_zero_apply and TauCeti.PDE.energyFormLp_one_zero_mass_apply: the Dirichlet and shifted-Laplacian formulas.
• TauCeti.PDE.energyFormLp_one_zero_zero_self and TauCeti.PDE.energyFormLp_one_zero_mass_self: their diagonal formulas.
• TauCeti.PDE.energyFormLp_zero_drift_flip_eq_of_isSymm: bundled symmetry when the principal matrix is symmetric and the drift vanishes.

@[instance_reducible]

noncomputable def TauCeti.PDE.energyFormLpDecidableEq {n : Type u_2} : DecidableEq n

The classical decidable equality used for finite-dimensional matrix computations.

Equations

• TauCeti.PDE.energyFormLpDecidableEq = Classical.decEq n

noncomputable def TauCeti.PDE.energyFormLp {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ) →L[ℝ] ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ) →L[ℝ] ℝ

The constant-coefficient divergence-form energy form on square-integrable value-gradient jets.

This is the Hölder pairing induced by energyIntegrand A b c; in particular it is bundled as a continuous bilinear map, with no integrability hypotheses required at use sites.

Equations

• TauCeti.PDE.energyFormLp μ A b c = ContinuousLinearMap.lpPairing μ 2 2 (TauCeti.PDE.energyIntegrand A b c)

@[simp]

theorem TauCeti.PDE.energyFormLp_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ A b c) U) V = ∫ (x : X), ((energyIntegrand A b c) (↑↑U x)) (↑↑V x) ∂μ

The L² energy form is the integral of the pointwise jet energy density.

theorem TauCeti.PDE.energyFormLp_one_zero_mass_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ 1 0 c) U) V = ∫ (x : X), (↑↑V x).2.ofLp ⬝ᵥ (↑↑U x).2.ofLp + c * (↑↑U x).1 * (↑↑V x).1 ∂μ

The shifted-Laplacian energy form is the sum of the gradient pairing and the mass pairing.

theorem TauCeti.PDE.energyFormLp_one_zero_zero_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ 1 0 0) U) V = ∫ (x : X), (↑↑V x).2.ofLp ⬝ᵥ (↑↑U x).2.ofLp ∂μ

The Dirichlet energy form pairs the gradient components of two L² jets.

theorem TauCeti.PDE.energyFormLp_one_zero_mass_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (c : ℝ) (U : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ 1 0 c) U) U = ∫ (x : X), ‖(↑↑U x).2‖ ^ 2 + c * (↑↑U x).1 ^ 2 ∂μ

The diagonal of the shifted-Laplacian L² energy form is the integral of the squared gradient norm plus the mass density.

theorem TauCeti.PDE.energyFormLp_one_zero_zero_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ 1 0 0) U) U = ∫ (x : X), ‖(↑↑U x).2‖ ^ 2 ∂μ

The diagonal of the Dirichlet L² energy form is the integral of the squared gradient norm.

theorem TauCeti.PDE.energyFormLp_coefficientSymmetricPart_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) (U : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ (coefficientSymmetricPart A) b c) U) U = ((energyFormLp μ A b c) U) U

Replacing the principal coefficient by its symmetric part does not change the diagonal L² energy form.

theorem TauCeti.PDE.energyFormLp_coefficientSymmetricPart_zero_drift_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ (coefficientSymmetricPart A) 0 c) U) V = (((energyFormLp μ A 0 c) U) V + ((energyFormLp μ A 0 c) V) U) / 2

The symmetric-part zero-drift L² energy form is the average of the original form and its transpose.

theorem TauCeti.PDE.energyFormLp_zero_drift_transpose_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ A.transpose 0 c) U) V = ((energyFormLp μ A 0 c) V) U

Transposing the principal coefficient swaps the two arguments of a zero-drift L² energy form.

theorem TauCeti.PDE.energyFormLp_zero_drift_comm_of_isSymm {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {A : Matrix n n ℝ} (hA : A.IsSymm) (μ : MeasureTheory.Measure X) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ A 0 c) U) V = ((energyFormLp μ A 0 c) V) U

A symmetric principal coefficient gives a symmetric zero-drift L² energy form.

@[simp]

theorem TauCeti.PDE.energyFormLp_zero_drift_flip_eq_of_isSymm {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {A : Matrix n n ℝ} (hA : A.IsSymm) (μ : MeasureTheory.Measure X) (c : ℝ) : (energyFormLp μ A 0 c).flip = energyFormLp μ A 0 c

A symmetric principal coefficient makes the zero-drift L² energy form equal to its flip.

theorem TauCeti.PDE.energyFormLp_coefficientSymmetricPart_zero_drift_comm {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ (coefficientSymmetricPart A) 0 c) U) V = ((energyFormLp μ (coefficientSymmetricPart A) 0 c) V) U

The symmetric-part zero-drift L² energy form is symmetric.

@[simp]

theorem TauCeti.PDE.energyFormLp_coefficientSymmetricPart_zero_drift_flip_eq {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (A : Matrix n n ℝ) (c : ℝ) : (energyFormLp μ (coefficientSymmetricPart A) 0 c).flip = energyFormLp μ (coefficientSymmetricPart A) 0 c

The symmetric-part zero-drift L² energy form is equal to its flip.

theorem TauCeti.PDE.energyFormLp_one_zero_mass_comm {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (c : ℝ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLp μ 1 0 c) U) V = ((energyFormLp μ 1 0 c) V) U

The shifted-Laplacian L² energy form is symmetric.

theorem TauCeti.PDE.energyFormLp_one_zero_mass_flip_eq {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (c : ℝ) : (energyFormLp μ 1 0 c).flip = energyFormLp μ 1 0 c

The shifted-Laplacian L² energy form is equal to its flip.