Uniform ellipticity for divergence-form PDE coefficients

This file records the explicit-constant matrix inequalities used for uniformly elliptic divergence-form operators. For a coefficient field a : X → Matrix n n ℝ on a domain Ω : Set X, the predicate UniformlyEllipticOn Ω a λ Λ means

λ ‖ξ‖² ≤ ξᵀ a(x) ξ and |ηᵀ a(x) ξ| ≤ Λ ‖η‖ ‖ξ‖

for every x ∈ Ω and all vectors η, ξ, together with the quantitative side conditions 0 < λ and λ ≤ Λ. The lower bound is the coercivity hypothesis; the bilinear upper bound controls nonsymmetric coefficient fields for weak-form boundedness.

This is the coefficient hypothesis named in the PDE roadmap before the energy bilinear form and Lax--Milgram arguments: constants are parameters, not hidden existential data.

Main declarations

• TauCeti.PDE.UniformlyEllipticOn: uniform lower and upper ellipticity bounds on a set.
• TauCeti.PDE.uniformlyEllipticOn_const_one: the identity matrix is uniformly elliptic.
• TauCeti.PDE.UniformlyEllipticOn.mono_constants: weakening constants preserves the predicate.
• TauCeti.PDE.UniformlyEllipticOn.mono_set: restriction to a smaller domain preserves the predicate.
• TauCeti.PDE.UniformlyEllipticOn.congr: replace a coefficient field by one that agrees on the domain.
• TauCeti.PDE.matrixBilinearForm: the bounded bilinear form η, ξ ↦ ηᵀ A ξ attached to a coefficient matrix.
• TauCeti.PDE.sum_inner_mul_matrixBilinearForm: expansion in the standard orthonormal basis.
• TauCeti.PDE.contDiff_matrixBilinearForm_gradient and TauCeti.PDE.tsupport_matrixBilinearForm_gradient_subset: smoothness and support of a conormal component of a smooth gradient.
• TauCeti.PDE.matrixBilinearFormLinear: the coefficient matrix-to-bilinear-form map as a continuous linear map.
• TauCeti.PDE.matrixBilinearForm_opNorm_le_of_upper_bound: a pointwise bilinear upper bound controls the operator norm of the attached matrix bilinear form.
• TauCeti.PDE.mul_sq_mul_norm_sq_le_matrixBilinearForm_add: the pointwise absorption estimate used in Caccioppoli inequalities.
• TauCeti.PDE.UniformlyEllipticOn.isCoercive_matrixBilinearForm: pointwise coercivity of the bilinear form attached to a uniformly elliptic coefficient field.
• TauCeti.PDE.UniformlyEllipticOn.opNorm_matrixBilinearForm_le: pointwise operator-norm boundedness of the bilinear form attached to a uniformly elliptic coefficient field.
• TauCeti.PDE.uniformlyEllipticOn_smul_one: scalar, isotropic coefficient fields are uniformly elliptic when their scalar coefficient lies between the ellipticity constants.
• TauCeti.PDE.UniformlyEllipticOn.add_nonneg: adding a nonnegative bounded coefficient field preserves the lower ellipticity constant and adds upper constants.
• TauCeti.PDE.UniformlyEllipticOn.add_bounded: adding a bounded coefficient perturbation preserves uniform ellipticity with lower constant λ - μ when the perturbation size μ is smaller than λ.
• TauCeti.PDE.coefficientSymmetricPart: the symmetric part (A + Aᵀ) / 2 of a coefficient matrix.
• TauCeti.PDE.UniformlyEllipticOn.transpose and TauCeti.PDE.UniformlyEllipticOn.coefficientSymmetricPart: transposing or replacing a coefficient field by its symmetric part preserves uniform ellipticity with the same constants.

The vectors are EuclideanSpace ℝ n, matching the roadmap's bounded open subsets of ℝⁿ; this type is reducibly a finite L² product, so Mathlib's matrix-vector API applies directly.

Symmetric part of a coefficient matrix

noncomputable def TauCeti.PDE.coefficientSymmetricPart {n : Type u_1} (A : Matrix n n ℝ) : Matrix n n ℝ

The symmetric part (A + Aᵀ) / 2 of a coefficient matrix.

For energy estimates the diagonal quadratic form of A agrees with that of coefficientSymmetricPart A, while the resulting matrix is symmetric. This is the finite-dimensional bookkeeping needed before the integrated energy form is specialized to self-adjoint elliptic operators.

Equations

• TauCeti.PDE.coefficientSymmetricPart A = (1 / 2) • (A + A.transpose)

theorem TauCeti.PDE.coefficientSymmetricPart_isSymm {n : Type u_1} (A : Matrix n n ℝ) : (coefficientSymmetricPart A).IsSymm

The symmetric part of a coefficient matrix is symmetric.

@[simp]

theorem TauCeti.PDE.coefficientSymmetricPart_apply {n : Type u_1} (A : Matrix n n ℝ) (i j : n) : coefficientSymmetricPart A i j = (A i j + A j i) / 2

The entries of the symmetric part are the averages of opposite entries.

@[simp]

theorem TauCeti.PDE.coefficientSymmetricPart_eq_self_of_isSymm {n : Type u_1} {A : Matrix n n ℝ} (hA : A.IsSymm) : coefficientSymmetricPart A = A

A symmetric coefficient matrix is unchanged by taking its symmetric part.

The matrix bilinear form

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

The continuous bilinear form attached to a real matrix on Euclidean space.

For a coefficient matrix A, this is the pointwise weak-form integrand (η, ξ) ↦ ηᵀ A ξ. It is bundled as a continuous bilinear map so it can feed directly into Mathlib's bounded-bilinear-form and Lax--Milgram APIs once the corresponding Sobolev spaces are available.

Equations

• TauCeti.PDE.matrixBilinearForm A = LinearMap.toContinuousBilinearMap (A.toBilin'Aux.comp ↑↑(EuclideanSpace.equiv n ℝ) ↑↑(EuclideanSpace.equiv n ℝ))

@[simp]

theorem TauCeti.PDE.matrixBilinearForm_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm A) η) ξ = η.ofLp ⬝ᵥ A.mulVec ξ.ofLp

The matrix bilinear form is the dot-product expression ηᵀ A ξ.

theorem TauCeti.PDE.matrixBilinearForm_smul_apply {n : Type u_1} [Fintype n] (c : ℝ) (A : Matrix n n ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm (c • A)) η) ξ = c * ((matrixBilinearForm A) η) ξ

Matrix bilinear forms are linear in scalar multiplication of the coefficient matrix.

theorem TauCeti.PDE.matrixBilinearForm_add_apply {n : Type u_1} [Fintype n] (A B : Matrix n n ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm (A + B)) η) ξ = ((matrixBilinearForm A) η) ξ + ((matrixBilinearForm B) η) ξ

Matrix bilinear forms are additive in the coefficient matrix.

theorem TauCeti.PDE.matrixBilinearForm_transpose_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm A.transpose) η) ξ = ((matrixBilinearForm A) ξ) η

Transposing the coefficient matrix swaps the arguments of the bundled matrix bilinear form.

theorem TauCeti.PDE.matrixBilinearForm_coefficientSymmetricPart_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm (coefficientSymmetricPart A)) η) ξ = (((matrixBilinearForm A) η) ξ + ((matrixBilinearForm A) ξ) η) / 2

The bundled bilinear form of the symmetric part is the average of the original bilinear form and its transpose.

noncomputable def TauCeti.PDE.matrixBilinearFormLinear {n : Type u_1} [Fintype n] : Matrix n n ℝ →L[ℝ] EuclideanSpace ℝ n →L[ℝ] EuclideanSpace ℝ n →L[ℝ] ℝ

The principal coefficient matrix-to-bilinear-form map as a continuous linear map.

Equations

• TauCeti.PDE.matrixBilinearFormLinear = LinearMap.toContinuousLinearMap { toFun := fun (A : Matrix n n ℝ) => TauCeti.PDE.matrixBilinearForm A, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.PDE.matrixBilinearFormLinear_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) : matrixBilinearFormLinear A = matrixBilinearForm A

Applying matrixBilinearFormLinear recovers matrixBilinearForm.

theorem TauCeti.PDE.continuous_matrixBilinearForm {n : Type u_1} [Fintype n] : Continuous fun (A : Matrix n n ℝ) => matrixBilinearForm A

The principal coefficient-to-bilinear-form map is continuous.

theorem TauCeti.PDE.Continuous.matrixBilinearForm {n : Type u_1} [Fintype n] {X : Type u_2} [TopologicalSpace X] {a : X → Matrix n n ℝ} (ha : Continuous a) : Continuous fun (x : X) => PDE.matrixBilinearForm (a x)

A continuous principal coefficient field gives a continuous field of principal bilinear forms.

theorem TauCeti.PDE.ContinuousOn.matrixBilinearForm {n : Type u_1} [Fintype n] {X : Type u_2} [TopologicalSpace X] {s : Set X} {a : X → Matrix n n ℝ} (ha : ContinuousOn a s) : ContinuousOn (fun (x : X) => PDE.matrixBilinearForm (a x)) s

A continuous principal coefficient field on a set gives a continuous field of principal bilinear forms on that set.

theorem TauCeti.PDE.norm_matrixBilinearForm_le_of_upper_bound {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) {Lam : ℝ} (hA : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (η ξ : EuclideanSpace ℝ n) : ‖((matrixBilinearForm A) η) ξ‖ ≤ Lam * ‖η‖ * ‖ξ‖

A pointwise bilinear upper bound gives the corresponding norm estimate for the bundled continuous bilinear form.

theorem TauCeti.PDE.matrixBilinearForm_opNorm_le_of_upper_bound {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) {Lam : ℝ} (hLam_nonneg : 0 ≤ Lam) (hA : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) : ‖matrixBilinearForm A‖ ≤ Lam

A pointwise bilinear upper bound controls the operator norm of the bundled matrix bilinear form.

This is the matrix-coefficient specialization of Mathlib's ContinuousLinearMap.opNorm_le_bound₂.

theorem TauCeti.PDE.matrixBilinearForm_apply_norm_le_of_upper_bound {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {Lam R S : ℝ} (hLam_nonneg : 0 ≤ Lam) (hA : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) {η ξ : EuclideanSpace ℝ n} (hη : ‖η‖ ≤ R) (hξ : ‖ξ‖ ≤ S) : ‖((matrixBilinearForm A) η) ξ‖ ≤ Lam * R * S

A pointwise bilinear upper bound gives a radius-restricted estimate for the bundled matrix bilinear form.

theorem TauCeti.PDE.abs_dotProduct_add_mulVec_le {n : Type u_1} [Fintype n] {A B : Matrix n n ℝ} {Lam Mu : ℝ} (hA : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hB : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ B.mulVec ξ.ofLp| ≤ Mu * ‖η‖ * ‖ξ‖) (η ξ : EuclideanSpace ℝ n) : |η.ofLp ⬝ᵥ (A + B).mulVec ξ.ofLp| ≤ (Lam + Mu) * ‖η‖ * ‖ξ‖

Adding two pointwise bilinear upper bounds adds the constants.

theorem TauCeti.PDE.abs_dotProduct_coefficientSymmetricPart_mulVec_le {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} {Lam : ℝ} (hA : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ A.mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (η ξ : EuclideanSpace ℝ n) : |η.ofLp ⬝ᵥ (coefficientSymmetricPart A).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖

The symmetric part of a pointwise bounded coefficient matrix satisfies the same bilinear upper bound.

Matrix quadratic forms and uniform ellipticity

@[simp]

theorem TauCeti.PDE.toQuadraticForm'_one {n : Type u_2} [Fintype n] [DecidableEq n] (ξ : EuclideanSpace ℝ n) : (Matrix.toQuadraticForm' 1) ξ.ofLp = ‖ξ‖ ^ 2

The identity matrix has quadratic form ‖ξ‖².

theorem TauCeti.PDE.matrixBilinearForm_one_apply {n : Type u_2} [Fintype n] [DecidableEq n] (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm 1) η) ξ = η.ofLp ⬝ᵥ ξ.ofLp

The matrix bilinear form associated to the identity matrix is the Euclidean dot product.

theorem TauCeti.PDE.toQuadraticForm'_smul_one {n : Type u_2} [Fintype n] [DecidableEq n] (c : ℝ) (ξ : EuclideanSpace ℝ n) : (c • 1).toQuadraticForm' ξ.ofLp = c * ‖ξ‖ ^ 2

The scalar identity matrix has quadratic form c ‖ξ‖².

@[simp]

theorem TauCeti.PDE.toQuadraticForm'_add {n : Type u_2} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) (ξ : EuclideanSpace ℝ n) : (A + B).toQuadraticForm' ξ.ofLp = A.toQuadraticForm' ξ.ofLp + B.toQuadraticForm' ξ.ofLp

Matrix quadratic forms are additive in the coefficient matrix.

@[simp]

theorem TauCeti.PDE.toQuadraticForm'_transpose {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (ξ : EuclideanSpace ℝ n) : A.transpose.toQuadraticForm' ξ.ofLp = A.toQuadraticForm' ξ.ofLp

Transposing the coefficient matrix does not change its quadratic form.

theorem TauCeti.PDE.matrixBilinearForm_smul_one_apply {n : Type u_2} [Fintype n] [DecidableEq n] (c : ℝ) (η ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm (c • 1)) η) ξ = c * η.ofLp ⬝ᵥ ξ.ofLp

The matrix bilinear form associated to c • 1 is c times the Euclidean dot product.

theorem TauCeti.PDE.matrixBilinearForm_self {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (ξ : EuclideanSpace ℝ n) : ((matrixBilinearForm A) ξ) ξ = A.toQuadraticForm' ξ.ofLp

The quadratic part of the matrix bilinear form is the matrix quadratic form.

@[simp]

theorem TauCeti.PDE.toQuadraticForm'_coefficientSymmetricPart {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (ξ : EuclideanSpace ℝ n) : (coefficientSymmetricPart A).toQuadraticForm' ξ.ofLp = A.toQuadraticForm' ξ.ofLp

The symmetric part has the same quadratic form as the original coefficient matrix.

theorem TauCeti.PDE.mul_sq_mul_norm_sq_le_matrixBilinearForm_add {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} {lam Lam : ℝ} (hlam : 0 < lam) (z w : ℝ) (g q : EuclideanSpace ℝ n) (hlower : lam * ‖g‖ ^ 2 ≤ A.toQuadraticForm' g.ofLp) (hupper : |q.ofLp ⬝ᵥ A.mulVec g.ofLp| ≤ Lam * ‖q‖ * ‖g‖) : lam * (z ^ 2 * ‖g‖ ^ 2) ≤ ((matrixBilinearForm A) (z • (z • g + w • q) + (z * w) • q)) g + lam / 2 * (z ^ 2 * ‖g‖ ^ 2) + 2 * Lam ^ 2 / lam * (‖q‖ ^ 2 * w ^ 2)

A pointwise absorption estimate for matrix bilinear forms. If the quadratic form is bounded below at g by λ ‖g‖² and the bilinear form at (q, g) is bounded by Λ ‖q‖ ‖g‖, then the cross term in A(g, z²g + 2zwq) is absorbed by half of the elliptic term and a multiple of w²‖q‖².

theorem TauCeti.PDE.abs_dotProduct_smul_one_mulVec_le_of_abs_le {n : Type u_2} [Fintype n] [DecidableEq n] {c Lam : ℝ} (hc : |c| ≤ Lam) (η ξ : EuclideanSpace ℝ n) : |η.ofLp ⬝ᵥ (c • 1).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖

A scalar multiple of the identity has operator integrand bounded by any upper bound for the absolute value of the scalar.

theorem TauCeti.PDE.norm_matrixBilinearForm_smul_one_le_of_abs_le {n : Type u_2} [Fintype n] [DecidableEq n] {c Lam : ℝ} (hc : |c| ≤ Lam) (η ξ : EuclideanSpace ℝ n) : ‖((matrixBilinearForm (c • 1)) η) ξ‖ ≤ Lam * ‖η‖ * ‖ξ‖

A scalar multiple of the identity has operator integrand bounded by any upper bound for the absolute value of the scalar.

theorem TauCeti.PDE.lower_bound_toQuadraticForm'_add {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} {lam : ℝ} (hA : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hB : ∀ (ξ : EuclideanSpace ℝ n), 0 ≤ B.toQuadraticForm' ξ.ofLp) (ξ : EuclideanSpace ℝ n) : lam * ‖ξ‖ ^ 2 ≤ (A + B).toQuadraticForm' ξ.ofLp

Adding a nonnegative quadratic form preserves a lower quadratic bound.

theorem TauCeti.PDE.lower_bound_toQuadraticForm'_add_of_lower_bound {n : Type u_2} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} {lam Mu : ℝ} (hA : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hB : ∀ (ξ : EuclideanSpace ℝ n), -(Mu * ‖ξ‖ ^ 2) ≤ B.toQuadraticForm' ξ.ofLp) (ξ : EuclideanSpace ℝ n) : (lam - Mu) * ‖ξ‖ ^ 2 ≤ (A + B).toQuadraticForm' ξ.ofLp

Adding a coefficient with a one-sided quadratic lower bound lowers a quadratic lower bound by the size of that perturbation.

theorem TauCeti.PDE.abs_toQuadraticForm'_le_of_abs_dotProduct_mulVec_le {n : Type u_2} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} {Mu : ℝ} (hB : ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ B.mulVec ξ.ofLp| ≤ Mu * ‖η‖ * ‖ξ‖) (ξ : EuclideanSpace ℝ n) : |B.toQuadraticForm' ξ.ofLp| ≤ Mu * ‖ξ‖ ^ 2

A bilinear upper bound for a coefficient matrix bounds its quadratic form in absolute value by the same constant.

theorem TauCeti.PDE.isCoercive_matrixBilinearForm_of_lower_bound {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) {lam : ℝ} (hlam : 0 < lam) (hA : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) : IsCoercive (matrixBilinearForm A)

A pointwise quadratic lower bound makes the associated matrix bilinear form coercive in Mathlib's Lax--Milgram sense.

theorem TauCeti.PDE.isCoercive_matrixBilinearForm_one {n : Type u_2} [Fintype n] [DecidableEq n] : IsCoercive (matrixBilinearForm 1)

The identity matrix bilinear form is coercive with constant 1.

theorem TauCeti.PDE.isCoercive_matrixBilinearForm_smul_one {n : Type u_2} [Fintype n] [DecidableEq n] {c : ℝ} (hc : 0 < c) : IsCoercive (matrixBilinearForm (c • 1))

A positive scalar multiple of the identity matrix gives a coercive bilinear form.

def TauCeti.PDE.UniformlyEllipticOn {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) (a : X → Matrix n n ℝ) (lam Lam : ℝ) : Prop

Uniform ellipticity and boundedness with explicit constants on a domain.

The predicate says that for every x ∈ Ω, the matrix a x has quadratic form bounded below by λ‖ξ‖² and bilinear form bounded above by Λ‖η‖‖ξ‖, uniformly in x, η, and ξ. The side conditions 0 < λ and λ ≤ Λ are part of the predicate so later energy estimates can recover them directly.

Equations

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

theorem TauCeti.PDE.uniformlyEllipticOn_iff {n : Type u_2} [Fintype n] [DecidableEq n] {α✝ : Type u_3} {Ω : Set α✝} {a : α✝ → Matrix n n ℝ} {lam Lam : ℝ} : UniformlyEllipticOn Ω a lam Lam ↔ 0 < lam ∧ lam ≤ Lam ∧ ∀ ⦃x : α✝⦄, x ∈ Ω → (∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) ∧ ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖

Characteristic restatement of uniform ellipticity and boundedness on a domain.

theorem TauCeti.PDE.UniformlyEllipticOn.pos {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) : 0 < lam

The lower ellipticity constant is positive.

theorem TauCeti.PDE.UniformlyEllipticOn.le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) : lam ≤ Lam

The lower ellipticity constant is no larger than the upper constant.

theorem TauCeti.PDE.UniformlyEllipticOn.upper_nonneg {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) : 0 ≤ Lam

The upper ellipticity constant is nonnegative.

theorem TauCeti.PDE.UniformlyEllipticOn.lower_bound {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) (ξ : EuclideanSpace ℝ n) : lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp

The lower quadratic-form bound supplied by uniform ellipticity.

theorem TauCeti.PDE.UniformlyEllipticOn.upper_bound {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) (η ξ : EuclideanSpace ℝ n) : |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖

The bilinear upper bound supplied by uniform ellipticity.

theorem TauCeti.PDE.UniformlyEllipticOn.quadraticForm_nonneg {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) (ξ : EuclideanSpace ℝ n) : 0 ≤ (a x).toQuadraticForm' ξ.ofLp

Uniform ellipticity implies pointwise nonnegativity of the coefficient quadratic form.

theorem TauCeti.PDE.UniformlyEllipticOn.quadraticForm_pos {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {ξ : EuclideanSpace ℝ n} (hξ : ξ ≠ 0) : 0 < (a x).toQuadraticForm' ξ.ofLp

Uniform ellipticity gives a positive quadratic form on every nonzero vector.

theorem TauCeti.PDE.UniformlyEllipticOn.mono_set {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω Ω' : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : Ω' ⊆ Ω) : UniformlyEllipticOn Ω' a lam Lam

Restricting the domain preserves uniform ellipticity with the same constants.

theorem TauCeti.PDE.UniformlyEllipticOn.mono_constants {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam lam' Lam' : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) (hlam' : 0 < lam') (hlam'_le : lam' ≤ lam) (hLam_le : Lam ≤ Lam') : UniformlyEllipticOn Ω a lam' Lam'

Weakening the lower constant and increasing the upper constant preserves uniform ellipticity.

theorem TauCeti.PDE.UniformlyEllipticOn.of_bounds {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (hlam : 0 < lam) (hlamLam : lam ≤ Lam) (hbounds : ∀ ⦃x : X⦄, x ∈ Ω → ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) (hupper : ∀ ⦃x : X⦄, x ∈ Ω → ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) : UniformlyEllipticOn Ω a lam Lam

A constructor when the side conditions and pointwise quadratic-form bounds are already available separately.

theorem TauCeti.PDE.UniformlyEllipticOn.congr {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a b : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) (hab : Set.EqOn b a Ω) : UniformlyEllipticOn Ω b lam Lam

Uniform ellipticity depends only on the coefficient values on the domain.

theorem TauCeti.PDE.UniformlyEllipticOn.norm_point_matrixBilinearForm_le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) (η ξ : EuclideanSpace ℝ n) : ‖((matrixBilinearForm (a x)) η) ξ‖ ≤ Lam * ‖η‖ * ‖ξ‖

At every point of the domain, uniform ellipticity gives a norm bound for the attached matrix bilinear form.

theorem TauCeti.PDE.UniformlyEllipticOn.opNorm_matrixBilinearForm_le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) : ‖matrixBilinearForm (a x)‖ ≤ Lam

At every point of the domain, uniform ellipticity bounds the operator norm of the attached matrix bilinear form by the upper ellipticity constant.

theorem TauCeti.PDE.UniformlyEllipticOn.norm_point_matrixBilinearForm_le_mul_of_norm_le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {R S : ℝ} {η ξ : EuclideanSpace ℝ n} (hη : ‖η‖ ≤ R) (hξ : ‖ξ‖ ≤ S) : ‖((matrixBilinearForm (a x)) η) ξ‖ ≤ Lam * R * S

Uniform ellipticity gives a radius-restricted pointwise bound for the coefficient integrand.

theorem TauCeti.PDE.UniformlyEllipticOn.isCoercive_matrixBilinearForm {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) : IsCoercive (matrixBilinearForm (a x))

At every point of the domain, uniform ellipticity gives coercivity of the attached matrix bilinear form.

theorem TauCeti.PDE.UniformlyEllipticOn.transpose {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) : UniformlyEllipticOn Ω (fun (x : X) => (a x).transpose) lam Lam

Transposing the coefficient field preserves uniform ellipticity with the same constants.

The quadratic lower bound is unchanged, and the bilinear upper bound follows by swapping the two Euclidean arguments.

theorem TauCeti.PDE.UniformlyEllipticOn.coefficientSymmetricPart {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) : UniformlyEllipticOn Ω (fun (x : X) => PDE.coefficientSymmetricPart (a x)) lam Lam

Replacing a coefficient field by its symmetric part preserves uniform ellipticity with the same constants.

This lets the energy-method API pass from a nonsymmetric uniformly elliptic principal coefficient to the symmetric coefficient with the same diagonal energy, which is the finite-dimensional prerequisite for self-adjoint model problems.

theorem TauCeti.PDE.UniformlyEllipticOn.add_nonneg {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {b : X → Matrix n n ℝ} {Mu : ℝ} (hMu : 0 ≤ Mu) (hb_nonneg : ∀ ⦃x : X⦄, x ∈ Ω → ∀ (ξ : EuclideanSpace ℝ n), 0 ≤ (b x).toQuadraticForm' ξ.ofLp) (hb_upper : ∀ ⦃x : X⦄, x ∈ Ω → ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (b x).mulVec ξ.ofLp| ≤ Mu * ‖η‖ * ‖ξ‖) : UniformlyEllipticOn Ω (fun (x : X) => a x + b x) lam (Lam + Mu)

Adding a pointwise nonnegative bounded coefficient field preserves uniform ellipticity.

The lower ellipticity constant is unchanged, while the upper bilinear-form constant is increased by the upper bound for the perturbation. This is the pointwise matrix estimate used when an energy form is split into a uniformly elliptic principal part plus a nonnegative bounded perturbation.

theorem TauCeti.PDE.UniformlyEllipticOn.add_bounded {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {b : X → Matrix n n ℝ} {Mu : ℝ} (hMu_nonneg : 0 ≤ Mu) (hMu_lt : Mu < lam) (hb_upper : ∀ ⦃x : X⦄, x ∈ Ω → ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (b x).mulVec ξ.ofLp| ≤ Mu * ‖η‖ * ‖ξ‖) : UniformlyEllipticOn Ω (fun (x : X) => a x + b x) (lam - Mu) (Lam + Mu)

Adding a bounded coefficient perturbation preserves uniform ellipticity after reducing the lower ellipticity constant by the perturbation size.

If a is uniformly elliptic with constants λ, Λ and b has pointwise bilinear bound μ, then a + b is uniformly elliptic with constants λ - μ, Λ + μ, provided μ < λ. This is the finite-dimensional coefficient stability estimate used when perturbing a uniformly elliptic divergence-form operator.

theorem TauCeti.PDE.UniformlyEllipticOn.add_smul_one_bounded {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {c : X → ℝ} {Mu : ℝ} (hMu_nonneg : 0 ≤ Mu) (hMu_lt : Mu < lam) (hc_abs : ∀ ⦃x : X⦄, x ∈ Ω → |c x| ≤ Mu) : UniformlyEllipticOn Ω (fun (x : X) => a x + c x • 1) (lam - Mu) (Lam + Mu)

Adding a bounded scalar multiple of the identity preserves uniform ellipticity after reducing the lower ellipticity constant by the scalar bound.

This is the scalar-coefficient specialization of UniformlyEllipticOn.add_bounded: no sign condition is imposed on c, only the pointwise bound |c x| ≤ μ.

theorem TauCeti.PDE.UniformlyEllipticOn.add_const_smul_one_bounded {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {c Mu : ℝ} (hMu_lt : Mu < lam) (hc_abs : |c| ≤ Mu) : UniformlyEllipticOn Ω (fun (y : X) => a y + c • 1) (lam - Mu) (Lam + Mu)

Adding a constant bounded scalar multiple of the identity preserves uniform ellipticity after reducing the lower ellipticity constant by the absolute value bound.

theorem TauCeti.PDE.UniformlyEllipticOn.add_smul_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {c : X → ℝ} {Mu : ℝ} (hMu : 0 ≤ Mu) (hc_nonneg : ∀ ⦃x : X⦄, x ∈ Ω → 0 ≤ c x) (hc_upper : ∀ ⦃x : X⦄, x ∈ Ω → c x ≤ Mu) : UniformlyEllipticOn Ω (fun (x : X) => a x + c x • 1) lam (Lam + Mu)

Adding a bounded nonnegative scalar multiple of the identity preserves uniform ellipticity, with the upper constant increased by the scalar bound.

theorem TauCeti.PDE.UniformlyEllipticOn.add_const_smul_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {c : ℝ} (hc : 0 ≤ c) : UniformlyEllipticOn Ω (fun (x : X) => a x + c • 1) lam (Lam + c)

Adding a constant nonnegative scalar multiple of the identity preserves uniform ellipticity, with the upper constant increased by that scalar.

theorem TauCeti.PDE.uniformlyEllipticOn_congr {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a b : X → Matrix n n ℝ} {lam Lam : ℝ} (hab : Set.EqOn a b Ω) : UniformlyEllipticOn Ω a lam Lam ↔ UniformlyEllipticOn Ω b lam Lam

Equal coefficient fields on the domain give equivalent uniform-ellipticity hypotheses.

theorem TauCeti.PDE.uniformlyEllipticOn_const_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) {lam Lam : ℝ} (hlam : 0 < lam) (hlam_one : lam ≤ 1) (hone_Lam : 1 ≤ Lam) : UniformlyEllipticOn Ω (fun (x : X) => 1) lam Lam

The constant identity coefficient field is uniformly elliptic with any constants λ ≤ 1 ≤ Λ and 0 < λ. This is the coefficient field of the Laplacian model problem.

theorem TauCeti.PDE.uniformlyEllipticOn_const_one_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) : UniformlyEllipticOn Ω (fun (x : X) => 1) 1 1

In particular, the identity coefficient field is uniformly elliptic with constants λ = Λ = 1.

theorem TauCeti.PDE.uniformlyEllipticOn_smul_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) (c : X → ℝ) {lam Lam : ℝ} (hlam : 0 < lam) (hlamLam : lam ≤ Lam) (hbound : ∀ ⦃x : X⦄, x ∈ Ω → lam ≤ c x ∧ c x ≤ Lam) : UniformlyEllipticOn Ω (fun (x : X) => c x • 1) lam Lam

An isotropic scalar coefficient field is uniformly elliptic when its scalar coefficient lies between the lower and upper constants.

This packages the common model a(x) = c(x) I: if λ ≤ c x ≤ Λ on Ω, then c x • 1 satisfies the lower quadratic bound and the bilinear upper bound with constants λ and Λ.

theorem TauCeti.PDE.uniformlyEllipticOn_const_smul_one_self {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) {c : ℝ} (hc : 0 < c) : UniformlyEllipticOn Ω (fun (x : X) => c • 1) c c

A constant positive isotropic coefficient field is uniformly elliptic with matching lower and upper constants.

theorem TauCeti.PDE.uniformlyEllipticOn_const_smul_one {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] (Ω : Set X) {c lam Lam : ℝ} (hlam : 0 < lam) (hlamc : lam ≤ c) (hcLam : c ≤ Lam) : UniformlyEllipticOn Ω (fun (x : X) => c • 1) lam Lam

A constant isotropic coefficient field is uniformly elliptic for any explicit constants λ ≤ c ≤ Λ with 0 < λ.

Gradient calculus and orthonormal expansion

theorem TauCeti.PDE.sum_inner_mul_matrixBilinearForm {n : Type u_3} [Fintype n] {A : Matrix n n ℝ} (ξ η : EuclideanSpace ℝ n) : ∑ i : n, inner ℝ ξ ((EuclideanSpace.basisFun n ℝ) i) * ((matrixBilinearForm A) ((EuclideanSpace.basisFun n ℝ) i)) η = ((matrixBilinearForm A) ξ) η

Expanding the first argument of a matrix bilinear form in an orthonormal basis.

theorem TauCeti.PDE.contDiff_matrixBilinearForm_gradient {n : Type u_3} [Fintype n] {A : Matrix n n ℝ} {ψ : EuclideanSpace ℝ n → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (η : EuclideanSpace ℝ n) : ContDiff ℝ ↑⊤ fun (y : EuclideanSpace ℝ n) => ((matrixBilinearForm A) η) (gradient ψ y)

The conormal component obtained by applying a matrix bilinear form to a smooth gradient is smooth.

theorem TauCeti.PDE.tsupport_matrixBilinearForm_gradient_subset {n : Type u_3} [Fintype n] {A : Matrix n n ℝ} (ψ : EuclideanSpace ℝ n → ℝ) (η : EuclideanSpace ℝ n) : (tsupport fun (y : EuclideanSpace ℝ n) => ((matrixBilinearForm A) η) (gradient ψ y)) ⊆ tsupport ψ

The conormal component of a gradient is supported where the function is.