Uniform ellipticity from pointwise positive definiteness

SmoothOpOn.elliptic asks directly for a uniform ellipticity constant on U. In practice a coefficient matrix is more often known through pointwise positive definiteness together with continuity, with no uniform constant given in advance: this file supplies the compactness argument that produces one on any compact subset, an alternative route to discharging SmoothOpOn.elliptic when U is exhausted by compact sets.

The constant comes from a minimum of the quadratic form over the compact product of the base set with the unit sphere of directions, which is positive because the integrand is, by continuity and compactness of that product.

Main declarations

• exists_uniform_elliptic_of_continuousOn: a matrix field continuous and pointwise positive definite on a compact set is uniformly elliptic there, with an explicit ellipticity constant.

theorem EllipticPdes.Regularity.exists_uniform_elliptic_of_continuousOn {d : ℕ} {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {a : X → Fin d → Fin d → ℝ} (ha : ∀ (i j : Fin d), ContinuousOn (fun (x : X) => a x i j) K) (hpos : ∀ x ∈ K, ∀ (ξ : Fin d → ℝ), ξ ≠ 0 → 0 < ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) : ∃ lam > 0, ∀ x ∈ K, ∀ (ξ : Fin d → ℝ), lam * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j

Uniform ellipticity on a compact set from pointwise positivity. A matrix field continuous on a compact K and positive definite at every point of K is uniformly elliptic on K. The constant is a minimum of the quadratic form over K against the unit sphere of directions, attained and positive by continuity and compactness.