One piece of the differentiated datum

Every term of the datum of Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 step 3 has the same shape: a cutoff, a W^{k,∞} coefficient, and a derivative of the solution of order at most two. The cutoff is the middle cutoff of the tower or one of its first two partial derivatives, and it is what confines the term to the collar and lets it be extended by zero to the whole domain.

This file turns that shape into a single lemma. Given the cutoff and the coefficient, there is a constant such that every derivative with k weak derivatives on the collar produces a class on the domain that has k weak derivatives, is bounded by the constant times the bound on the derivative, and pairs against a test function as the product of the three factors.

The three conclusions are produced together because they are produced by the same construction: exists_iteratedWeakDeriv_mul puts the coefficient in, exists_iteratedWeakDeriv_extend_mulTest puts the cutoff in and moves the result to the domain, and the pairing is read off the almost-everywhere description both of them are stated against.

Main declarations

• exists_datum_piece: the class, its family, its bound, and its pairing.
• exists_datum_of_pieces: a finite family of pieces, assembled.

theorem EllipticPdes.Regularity.exists_datum_piece {d : ℕ} {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hNm : MeasurableSet N) (hNΩ : N ⊆ Ω) (k : ℕ) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn N χ) {a : EuclideanSpace ℝ (Fin d) → ℝ} (ha : IsWkInfty a k) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {p : Sobolev.L2D N} (hp : HasIteratedWeakDerivOn N k p) {M : ℝ}, IteratedL2Bound hp M → ∃ (q : Sobolev.L2D Ω) (H : HasIteratedWeakDerivOn Ω k q), IteratedL2Bound H (K * M) ∧ ∀ (v : EuclideanSpace ℝ (Fin d) → ℝ), ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑q x * v x = ∫ (x : EuclideanSpace ℝ (Fin d)) in N, χ x * (a x * ↑↑p x) * v x

One piece of the datum. For a cutoff χ supported in the collar N ⊆ Ω and a W^{k,∞} coefficient a, there is a constant K such that every p with k weak derivatives on N bounded by M yields a class q on Ω with

• k weak derivatives on Ω, bounded by K·M;
• ∫_Ω q·v = ∫_N χ·a·p·v for every v.

The constant depends on the cutoff, the coefficient and the order alone, which is what keeps the estimate of the induction step quantified before the solution and the datum.

theorem EllipticPdes.Regularity.exists_datum_of_pieces {d : ℕ} {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hNm : MeasurableSet N) (hNΩ : N ⊆ Ω) (k : ℕ) {ι : Type u_1} [Fintype ι] {χ : ι → EuclideanSpace ℝ (Fin d) → ℝ} (hχ : ∀ (t : ι), Sobolev.IsTestFn N (χ t)) {a : ι → EuclideanSpace ℝ (Fin d) → ℝ} (ha : (t : ι) → IsWkInfty (a t) k) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (p : ι → Sobolev.L2D N) (hp : (t : ι) → HasIteratedWeakDerivOn N k (p t)) {M : ℝ}, (∀ (t : ι), IteratedL2Bound (hp t) M) → ∃ (F : Sobolev.L2D Ω) (HF : HasIteratedWeakDerivOn Ω k F), IteratedL2Bound HF (K * M) ∧ ∀ (v : EuclideanSpace ℝ (Fin d) → ℝ), ContDiff ℝ (↑⊤) v → HasCompactSupport v → ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑F x * v x = ∑ t : ι, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, χ t x * (a t x * ↑↑(p t) x) * v x

Finite family of pieces assembled. The datum of the induction step is a fixed finite list of shapes, each a cutoff against a coefficient against a derivative, and only the derivatives depend on the solution. Quantifying the constant before the derivatives is what makes that work: the cutoffs and coefficients are data of the operator and the tower, so their constants are summed once.

The pairing is asked of a test function rather than of an arbitrary weight, since splitting the integral of the sum into the sum of the integrals is where integrability enters.