Linearity of pointwise PDE energy integrands

The divergence-form energy integrand energyIntegrand A b c is linear in the coefficient triple (A, b, c). This file records that bookkeeping as bundled continuous-bilinear-map equalities and as pointwise evaluation lemmas.

These lemmas are pointwise finite-dimensional prerequisites for Lane D of the PDE roadmap. When the later weak energy form is an integral of energyIntegrand (a x) (b x) (c x), this API lets bounded perturbations and decompositions into principal, drift, and mass pieces be rewritten before applying the boundedness and Gårding estimates.

Main declarations

• TauCeti.PDE.energyIntegrand_add, TauCeti.PDE.energyIntegrand_smul, TauCeti.PDE.energyIntegrand_neg, and TauCeti.PDE.energyIntegrand_sub: bundled coefficient-linearity of the pointwise energy integrand.
• TauCeti.PDE.energyIntegrand_principal_add_lowerOrder and TauCeti.PDE.energyIntegrand_principal_drift_mass: decomposition into the principal, drift, and mass pieces.
• TauCeti.PDE.energyIntegrand_add_apply, TauCeti.PDE.energyIntegrand_neg_apply, TauCeti.PDE.energyIntegrand_sub_apply, and TauCeti.PDE.energyIntegrand_smul_apply: pointwise evaluation forms of coefficient linearity.
• TauCeti.PDE.energyIntegrand_eq_one_zero_baseMass_add_perturbation and its _apply form: shifted-Laplacian-plus-residual decomposition with a chosen base mass.

@[simp]

theorem TauCeti.PDE.energyIntegrand_zero {n : Type u_1} [Fintype n] : energyIntegrand 0 0 0 = 0

The zero coefficient triple has zero pointwise energy integrand.

@[simp]

theorem TauCeti.PDE.energyIntegrand_add {n : Type u_1} [Fintype n] (A B : Matrix n n ℝ) (b d : EuclideanSpace ℝ n) (c e : ℝ) : energyIntegrand (A + B) (b + d) (c + e) = energyIntegrand A b c + energyIntegrand B d e

The pointwise energy integrand is additive in its coefficient triple.

theorem TauCeti.PDE.energyIntegrand_add_apply {n : Type u_1} [Fintype n] (A B : Matrix n n ℝ) (b d : EuclideanSpace ℝ n) (c e : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand (A + B) (b + d) (c + e)) U) V = ((energyIntegrand A b c) U) V + ((energyIntegrand B d e) U) V

Pointwise evaluation form of energyIntegrand_add.

@[simp]

theorem TauCeti.PDE.energyIntegrand_neg {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) : energyIntegrand (-A) (-b) (-c) = -energyIntegrand A b c

The pointwise energy integrand is compatible with negating all coefficients.

theorem TauCeti.PDE.energyIntegrand_neg_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 = -((energyIntegrand A b c) U) V

Pointwise evaluation form of energyIntegrand_neg.

@[simp]

theorem TauCeti.PDE.energyIntegrand_sub {n : Type u_1} [Fintype n] (A B : Matrix n n ℝ) (b d : EuclideanSpace ℝ n) (c e : ℝ) : energyIntegrand (A - B) (b - d) (c - e) = energyIntegrand A b c - energyIntegrand B d e

The pointwise energy integrand is subtractive in its coefficient triple.

theorem TauCeti.PDE.energyIntegrand_sub_apply {n : Type u_1} [Fintype n] (A B : Matrix n n ℝ) (b d : EuclideanSpace ℝ n) (c e : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand (A - B) (b - d) (c - e)) U) V = ((energyIntegrand A b c) U) V - ((energyIntegrand B d e) U) V

Pointwise evaluation form of energyIntegrand_sub.

@[simp]

theorem TauCeti.PDE.energyIntegrand_smul {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c r : ℝ) : energyIntegrand (r • A) (r • b) (r * c) = r • energyIntegrand A b c

The pointwise energy integrand is homogeneous in its coefficient triple.

theorem TauCeti.PDE.energyIntegrand_smul_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c r : ℝ) (U V : ℝ × EuclideanSpace ℝ n) : ((energyIntegrand (r • A) (r • b) (r * c)) U) V = r * ((energyIntegrand A b c) U) V

Pointwise evaluation form of energyIntegrand_smul.

theorem TauCeti.PDE.energyIntegrand_principal_add_lowerOrder {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) : energyIntegrand A b c = energyIntegrand A 0 0 + energyIntegrand 0 b c

The full energy integrand splits into its principal part and lower-order part.

theorem TauCeti.PDE.energyIntegrand_principal_drift_mass {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) : energyIntegrand A b c = energyIntegrand A 0 0 + energyIntegrand 0 b 0 + energyIntegrand 0 0 c

The full energy integrand splits into its principal, drift, and mass pieces.

theorem TauCeti.PDE.energyIntegrand_eq_one_zero_baseMass_add_perturbation {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c m : ℝ) [DecidableEq n] : energyIntegrand A b c = energyIntegrand 1 0 m + energyIntegrand (A - 1) b (c - m)

The full energy integrand is the sum of a shifted Laplacian model with chosen base mass and the residual perturbation of the coefficient triple.

theorem TauCeti.PDE.energyIntegrand_eq_one_zero_baseMass_add_perturbation_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c m : ℝ) (U V : ℝ × EuclideanSpace ℝ n) [DecidableEq n] : ((energyIntegrand A b c) U) V = ((energyIntegrand 1 0 m) U) V + ((energyIntegrand (A - 1) b (c - m)) U) V

Pointwise form of the shifted-Laplacian-plus-residual-perturbation decomposition.

theorem TauCeti.PDE.energyIntegrand_eq_one_zero_mass_add_perturbation {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) [DecidableEq n] : energyIntegrand A b c = energyIntegrand 1 0 c + energyIntegrand (A - 1) b 0

The full energy integrand is the sum of a shifted Laplacian model and a perturbation of the principal and drift coefficients.