Localising coefficients smooth on an open set into a global elliptic operator

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3 states its conclusion for coefficients and a datum smooth on the whole region Ω, with no bound assumed anywhere. The interior-regularity chain in this development runs on a FullEllipticOp, whose coefficients are global, essentially bounded and measurable, which is a different hypothesis shape. This file bridges the two: SmoothOpOn states coefficients smooth and uniformly elliptic on an open set U with no global bound, and localOp blends them against λ I, 0, 0 outside a cutoff to build a FullEllipticOp agreeing with the given coefficients wherever the cutoff is 1.

The blend

For a test function χ of U, valued in [0, 1],

• ã = λ I + χ (a − λ I) = χ a + (1 − χ) λ I,
• b̃ = χ b,
• c̃ = χ c.

Wherever χ = 1 the blend agrees with P.a, P.b, P.c; wherever χ = 0 it reduces to the constant-coefficient Laplacian at level λ, which is trivially uniformly elliptic, bounded and of every regularity class. Ellipticity of the blend follows from ellipticity of P.a on U and convexity of the quadratic form in χ between the two extremes, needing no symmetry.

Main declarations

• SmoothOpOn: coefficients smooth and uniformly elliptic a.e. on an open set, unbounded.
• localOp: the blended global operator.
• exists_localOp: for every compact K ⊆ U there is a cutoff and an open W ⊇ K on which localOp agrees with the given coefficients and meets every regularity mixin interior_smooth asks for.

structure EllipticPdes.Regularity.SmoothOpOn (d : ℕ) (U : Set (EuclideanSpace ℝ (Fin d))) : Type

Coefficients of Evans §6.3.1, Theorem 3. Smooth on the open set U, uniformly elliptic almost everywhere on U, with no global bound, no measurability asked off U and no symmetry asked anywhere. This is the hypothesis shape the theorem's classical statement supplies, before it is localised into the global bounded-measurable shape FullEllipticOp asks for.

• a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ

  The principal-part coefficient matrix.

• b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ

  The transport (first-order) coefficients.

• c : EuclideanSpace ℝ (Fin d) → ℝ

  The zeroth-order coefficient.

• lam : ℝ

  The ellipticity constant.

• lam_pos : 0 < self.lam

  The ellipticity constant is strictly positive.

• a_smooth (i j : Fin d) : ContDiffOn ℝ (↑⊤) (fun (x : EuclideanSpace ℝ (Fin d)) => self.a x i j) U

  Every entry of the principal part is smooth on U.

• b_smooth (i : Fin d) : ContDiffOn ℝ (↑⊤) (fun (x : EuclideanSpace ℝ (Fin d)) => self.b x i) U

  Every transport component is smooth on U.

• c_smooth : ContDiffOn ℝ (↑⊤) self.c U

  The zeroth-order coefficient is smooth on U.

• elliptic : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict U, ∀ (ξ : Fin d → ℝ), self.lam * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, self.a x i j * ξ i * ξ j

  The principal part is uniformly elliptic almost everywhere on U.

def EllipticPdes.Regularity.SmoothOpOn.δ {d : ℕ} (i j : Fin d) : ℝ

Kronecker delta as a real number.

Equations

• EllipticPdes.Regularity.SmoothOpOn.δ i j = if i = j then 1 else 0

def EllipticPdes.Regularity.SmoothOpOn.gA {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (i j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The principal part shifted down to λ I, cut off by χ.

Equations

• P.gA χ i j x = χ x * (P.a x i j - P.lam * EllipticPdes.Regularity.SmoothOpOn.δ i j)

def EllipticPdes.Regularity.SmoothOpOn.aT {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) (i j : Fin d) : ℝ

The blended principal part ã = λ I + χ (a − λ I) = χ a + (1 − χ) λ I.

Equations

• P.aT χ x i j = P.lam * EllipticPdes.Regularity.SmoothOpOn.δ i j + P.gA χ i j x

def EllipticPdes.Regularity.SmoothOpOn.bT {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) (i : Fin d) : ℝ

The cut-off transport field.

Equations

• P.bT χ x i = χ x * P.b x i

def EllipticPdes.Regularity.SmoothOpOn.cT {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (χ : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The cut-off zeroth-order coefficient.

Equations

• P.cT χ x = χ x * P.c x

theorem EllipticPdes.Regularity.SmoothOpOn.gA_contDiff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (i j : Fin d) : ContDiff ℝ (↑⊤) (P.gA χ i j)

theorem EllipticPdes.Regularity.SmoothOpOn.gA_hasCompactSupport {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (i j : Fin d) : HasCompactSupport (P.gA χ i j)

theorem EllipticPdes.Regularity.SmoothOpOn.aT_contDiff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (i j : Fin d) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin d)) => P.aT χ x i j

theorem EllipticPdes.Regularity.SmoothOpOn.bT_contDiff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin d)) => P.bT χ x i

theorem EllipticPdes.Regularity.SmoothOpOn.cT_contDiff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) : ContDiff ℝ (↑⊤) (P.cT χ)

theorem EllipticPdes.Regularity.SmoothOpOn.quad_aT {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (x : EuclideanSpace ℝ (Fin d)) (ξ : Fin d → ℝ) : ∑ i : Fin d, ∑ j : Fin d, P.aT χ x i j * ξ i * ξ j = P.lam * ∑ i : Fin d, ξ i ^ 2 + χ x * (∑ i : Fin d, ∑ j : Fin d, P.a x i j * ξ i * ξ j - P.lam * ∑ i : Fin d, ξ i ^ 2)

The quadratic form of the blend, as a convex combination of λ |ξ|² and the quadratic form of P.a.

theorem EllipticPdes.Regularity.SmoothOpOn.aT_elliptic {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) (hUm : MeasurableSet U) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ∀ (ξ : Fin d → ℝ), P.lam * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, P.aT χ x i j * ξ i * ξ j

Uniform ellipticity of the blend on all of ℝᵈ, at the constant λ. Where χ = 0 the blend is the constant-coefficient form λ I, trivially elliptic at λ; where χ ∈ (0, 1] and x ∈ U, the quadratic form is a convex combination of λ |ξ|² and a quantity at least λ |ξ|² by ellipticity of P.a, hence itself at least λ |ξ|². No symmetry of P.a enters.

theorem EllipticPdes.Regularity.exists_sup_bound {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : EuclideanSpace ℝ (Fin d)), |g x| ≤ C

A smooth compactly supported function has a uniform bound, chosen once and reused.

noncomputable def EllipticPdes.Regularity.localOp {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) : Sobolev.FullEllipticOp d

The localised operator. Global coefficients on EuclideanSpace ℝ (Fin d), equal to λ I + χ (a − λ I), χ b, χ c, meeting every hypothesis FullEllipticOp asks: measurability and boundedness come from smoothness plus compact support, and ellipticity from aT_elliptic.

Equations

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

theorem EllipticPdes.Regularity.nonempty_isCkCoeff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) (k : ℕ) : Nonempty (IsCkCoeff (localOp P hU hχ hχ01).toEllipticCoeff k)

Cᵏ bundle for the localised principal part, at every order: each entry is a constant plus a smooth compactly supported function, and exists_iteratedFDeriv_bound_const_add supplies the bound.

theorem EllipticPdes.Regularity.nonempty_isC1Coeff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) : Nonempty (IsC1Coeff (localOp P hU hχ hχ01).toEllipticCoeff)

The localised principal part meets the C¹ regularity interior_smooth asks for.

theorem EllipticPdes.Regularity.nonempty_isWkInftyCoeff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) (k : ℕ) : Nonempty (IsWkInftyCoeff (localOp P hU hχ hχ01).toEllipticCoeff k)

The localised principal part lies in W^{k,∞} at every order, through the Cᵏ bundle.

theorem EllipticPdes.Regularity.nonempty_isWkInftyLower {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) (k : ℕ) : Nonempty (IsWkInftyLower (localOp P hU hχ hχ01) k)

The localised lower-order coefficients lie in W^{k,∞} at every order, uniformly.

Agreement on the region where the cutoff is one

theorem EllipticPdes.Regularity.eqOn_a {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) {W : Set (EuclideanSpace ℝ (Fin d))} (hW : ∀ x ∈ W, χ x = 1) (x : EuclideanSpace ℝ (Fin d)) : x ∈ W → (localOp P hU hχ hχ01).a x = P.a x

theorem EllipticPdes.Regularity.eqOn_b {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) {W : Set (EuclideanSpace ℝ (Fin d))} (hW : ∀ x ∈ W, χ x = 1) (x : EuclideanSpace ℝ (Fin d)) : x ∈ W → (localOp P hU hχ hχ01).b x = P.b x

theorem EllipticPdes.Regularity.eqOn_c {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) {W : Set (EuclideanSpace ℝ (Fin d))} (hW : ∀ x ∈ W, χ x = 1) (x : EuclideanSpace ℝ (Fin d)) : x ∈ W → (localOp P hU hχ hχ01).c x = P.c x

theorem EllipticPdes.Regularity.exists_localOp {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {K : Set (EuclideanSpace ℝ (Fin d))} (hK : IsCompact K) (hKU : K ⊆ U) : ∃ (χ : EuclideanSpace ℝ (Fin d) → ℝ) (hχ : Sobolev.IsTestFn U χ) (hχ01 : ∀ (x : EuclideanSpace ℝ (Fin d)), χ x ∈ Set.Icc 0 1) (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W ∧ K ⊆ W ∧ IsCompact (closure W) ∧ closure W ⊆ U ∧ (∀ x ∈ W, χ x = 1) ∧ (localOp P hU hχ hχ01).lam = P.lam ∧ (∀ x ∈ W, (localOp P hU hχ hχ01).a x = P.a x) ∧ (∀ x ∈ W, (localOp P hU hχ hχ01).b x = P.b x) ∧ (∀ x ∈ W, (localOp P hU hχ hχ01).c x = P.c x) ∧ Nonempty (IsC1Coeff (localOp P hU hχ hχ01).toEllipticCoeff) ∧ (∀ (k : ℕ), Nonempty (IsWkInftyCoeff (localOp P hU hχ hχ01).toEllipticCoeff k)) ∧ ∀ (k : ℕ), Nonempty (IsWkInftyLower (localOp P hU hχ hχ01) k)

Localisation of the coefficients. For every compact K ⊆ U there are a cutoff χ and an open W ⊇ K, with closure W compact inside U, on which the localised operator agrees with the given coefficients, and the localised operator meets every regularity mixin interior_smooth asks for. The cutoff comes from exists_isTestFn_one_nhdsSet_of_isCompact and W is the interior of the region on which it is 1.