Localising coefficients of finite order on an open set #
Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1 (p. 327) assumes
a^{ij} ∈ C¹(U) and b^i, c ∈ L^∞(U), and Theorem 2 (p. 332) assumes
a^{ij}, b^i, c ∈ C^{m+1}(U). Neither asks a bound on a^{ij} over U, and neither asks anything
of a coefficient off U. Localise/LocalOp.lean blends coefficients smooth on U into a
FullEllipticOp; this file does the same at finite order, and for lower-order coefficients that
are only essentially bounded and almost everywhere strongly measurable on U.
Blend #
For a test function χ of U valued in [0, 1], the principal part is
ã = λ I + χ (a − λ I), as in localOp. At order m the product χ (a − λ I) is C^m on the
whole space with compact support, so every derivative up to order m is bounded
(exists_iteratedFDeriv_bound_of_le), which is IsCkCoeff at order m. The lower-order
coefficients are supplied already cut off. For L^∞(U) coefficients the cutoff multiplies a
measurable modification (AEStronglyMeasurable.mk), which agrees with the coefficient almost
everywhere on U; for C^m(U) coefficients it multiplies the coefficient itself.
Main declarations #
PrincipalOn: a principal part of classC^monU, uniformly elliptic almost everywhere onU.blendOp: the blended global operator, withblendOp_isCkCoeffandblendOp_a_eq.C1OpOn,exists_localOp_C1: the coefficients of Theorem 1 and their localisation.CkOpOn,exists_localOp_Ck: the coefficients of Theorem 2 and their localisation.LocalWeakSol.congr_ae: the local weak formulation transported along coefficients equal almost everywhere.
A function of class C^n on an open U, multiplied by a test function supported in U,
is of class C^n on the whole space.
A compactly supported function of class C^m has every iterated derivative of order at
most m bounded, with a nonnegative bound at each order.
A compactly supported function of class C^m lies in W^{m,∞}.
A continuous compactly supported function has a nonnegative uniform bound.
Principal part of finite order #
Principal part of class C^m on an open set. Entries of class C^m on U, uniformly
elliptic almost everywhere on U with constant lam > 0, with no bound, no symmetry and nothing
asked off U.
The principal-part coefficient matrix.
- lam : ℝ
The ellipticity constant.
The ellipticity constant is strictly positive.
- contDiffOn (i j : Fin d) : ContDiffOn ℝ (↑m) (fun (x : EuclideanSpace ℝ (Fin d)) => self.a x i j) U
Every entry is of class
C^monU. - 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
Uniform ellipticity almost everywhere on
U.
Instances For
The principal part shifted down to λ I, cut off by χ.
Instances For
The blended principal part λ I + χ (a − λ I).
Instances For
The quadratic form of the blend, as a convex combination of λ |ξ|² and the quadratic form
of a.
Uniform ellipticity of the blend on the whole space at the constant λ.
Blended operator at finite order. Principal part λ I + χ (a − λ I), and
lower-order coefficients b, c supplied measurable and essentially bounded on the whole
space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
C^m bundle of the blend. Each entry is a constant plus a compactly supported function
of class C^m, so its derivatives of order 1 to m are bounded.
The blend is the given principal part wherever the cutoff is one.
The cutoff of exists_isTestFn_one_nhdsSet_of_isCompact and the open interior of the set
where it is one, which contains the compact set and sits inside U.
Coefficients of Theorem 1 #
Coefficients of Evans §6.3.1 Theorem 1 on an open set. a^{ij} ∈ C¹(U), uniformly
elliptic almost everywhere on U, and b^i, c ∈ L^∞(U): almost everywhere strongly measurable
and essentially bounded on U. Nothing is asked off U.
- b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ
The transport (first-order) coefficients.
- c : EuclideanSpace ℝ (Fin d) → ℝ
The zeroth-order coefficient.
- Bsup : ℝ
The essential bound on the transport coefficients over
U. - Csup : ℝ
The essential bound on the zeroth-order coefficient over
U. - b_aesm (i : Fin d) : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin d)) => self.b x i) (MeasureTheory.volume.restrict U)
Every transport component is almost everywhere strongly measurable on
U. - c_aesm : MeasureTheory.AEStronglyMeasurable self.c (MeasureTheory.volume.restrict U)
The zeroth-order coefficient is almost everywhere strongly measurable on
U. - b_bdd (i : Fin d) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict U, |self.b x i| ≤ self.Bsup
Every transport component is essentially bounded on
U. The zeroth-order coefficient is essentially bounded on
U.
Instances For
A cutoff of U times a measurable modification of a function essentially bounded on U
is measurable and essentially bounded on the whole space.
Localisation of the coefficients of Theorem 1. For every compact K ⊆ U there are a
global operator with C¹ principal part of bounded derivative and an open W with
K ⊆ W ⊆ U, on which the principal part agrees with the given one everywhere and the
lower-order coefficients agree with the given ones almost everywhere.
Coefficients of Theorem 2 #
Coefficients of Evans §6.3.1 Theorem 2 on an open set at order m. a^{ij}, b^i, c
of class C^m on U, with a^{ij} uniformly elliptic almost everywhere on U. Evans's
hypothesis at order m is this structure at m + 1. Nothing is asked off U.
- b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ
The transport (first-order) coefficients.
- c : EuclideanSpace ℝ (Fin d) → ℝ
The zeroth-order coefficient.
- b_contDiffOn (i : Fin d) : ContDiffOn ℝ (↑m) (fun (x : EuclideanSpace ℝ (Fin d)) => self.b x i) U
Every transport component is of class
C^monU. - c_contDiffOn : ContDiffOn ℝ (↑m) self.c U
The zeroth-order coefficient is of class
C^monU.
Instances For
Localisation of the coefficients of Theorem 2. For every compact K ⊆ U there are a
global operator with every coefficient of class C^m with bounded derivatives, packaged as
IsCkCoeff and IsWkInftyLower at order m, and an open W with K ⊆ W ⊆ U on which it agrees
with the given coefficients.
Transport of the weak formulation along almost everywhere equal coefficients #
Coefficients equal on W almost everywhere, with a principal part equal everywhere on W,
give the same local weak formulation on W.