Pairing an L² class against a test function

Evans's step 3 of §6.3.1, Theorem 2 assembles a datum out of a dozen products of a coefficient against a derivative of the solution, and every one of them reaches the statement as an integral against a test function. Moving between the sum of the integrals and the integral of the sum is all of the bookkeeping, the same three facts each time: the pairing is additive, it commutes with a finite sum, and a weighted class pairs as the weight times the class.

Integrability is what makes the moves legal, and it is uniform: an L² class against a continuous compactly supported function is integrable, by Hölder. Every lemma here takes the test function as smooth with compact support and asks nothing about its support, since none of these steps localises.

Main declarations

• integrable_mul_testFn: the product of an L²(V) class with a test function is integrable.
• setIntegral_add_mul_testFn, setIntegral_sub_mul_testFn, setIntegral_neg_mul_testFn: the pairing is additive.
• setIntegral_finsetSum_mul_testFn, setIntegral_sum_mul_testFn: the pairing commutes with a finite sum.
• setIntegral_mulL2_mul_testFn: a weighted class pairs as the weight against the class.

theorem EllipticPdes.Regularity.integrable_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.L2D V) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑F x * φ x) (MeasureTheory.volume.restrict V)

Integrability of an L² class against a test function. Hölder with the two exponents 2 and the continuous compactly supported factor in L².

theorem EllipticPdes.Regularity.setIntegral_add_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (F G : Sobolev.L2D V) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(F + G) x * φ x = (∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑F x * φ x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑G x * φ x

The pairing is additive in the class.

theorem EllipticPdes.Regularity.setIntegral_sub_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (F G : Sobolev.L2D V) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(F - G) x * φ x = (∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑F x * φ x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑G x * φ x

The pairing subtracts in the class.

theorem EllipticPdes.Regularity.setIntegral_neg_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.L2D V) (φ : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(-F) x * φ x = -∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑F x * φ x

The pairing negates in the class.

theorem EllipticPdes.Regularity.setIntegral_finsetSum_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ι : Type u_1} (s : Finset ι) (F : ι → Sobolev.L2D V) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(∑ i ∈ s, F i) x * φ x = ∑ i ∈ s, ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(F i) x * φ x

The pairing commutes with a finite sum over a Finset.

theorem EllipticPdes.Regularity.setIntegral_sum_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {ι : Type u_1} [Fintype ι] (F : ι → Sobolev.L2D V) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφc : ContDiff ℝ (↑⊤) φ) (hφcs : HasCompactSupport φ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(∑ i : ι, F i) x * φ x = ∑ i : ι, ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(F i) x * φ x

The pairing commutes with a finite sum over a Fintype.

theorem EllipticPdes.Regularity.integral_extendL2_mul_mul {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (hVm : MeasurableSet V) (F : Sobolev.L2D V) (a b : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin d)), a x * ↑↑((extendL2 hVm) F) x * b x = ∫ (x : EuclideanSpace ℝ (Fin d)) in V, a x * ↑↑F x * b x

Pairing of an extension by zero over its original set. A whole-space integral of a weight against the extension of an L²(S) class collapses to an integral over S. Stated with a weight on each side, which is the shape every block of the bilinear form takes.

theorem EllipticPdes.Regularity.setIntegral_mul_cutoff_partialD_split {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (P : Sobolev.L2D V) {χ v : EuclideanSpace ℝ (Fin d) → ℝ} (hχc : ContDiff ℝ (↑⊤) χ) (hχcs : HasCompactSupport χ) (hvc : ContDiff ℝ (↑⊤) v) (j : Fin d) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑P x * (χ x * Sobolev.partialD j v x) = (∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑P x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => χ y * v y) x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑P x * (Sobolev.partialD j χ x * v x)

Splitting off a derivative of the test function by a cutoff. Writing χ ∂ⱼv as ∂ⱼ(χv) - (∂ⱼχ)v moves the pairing onto the cut-off test function, which is the form the differentiated equation is stated against.

theorem EllipticPdes.Regularity.setIntegral_mul_congr_of_cutoff_ae {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {θ : EuclideanSpace ℝ (Fin d) → ℝ} {X Y : Sobolev.L2D V} (h : (fun (x : EuclideanSpace ℝ (Fin d)) => θ x * ↑↑X x) =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => θ x * ↑↑Y x) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ∀ (x : EuclideanSpace ℝ (Fin d)), θ x * ψ x = ψ x) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑X x * ψ x = ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑Y x * ψ x

Two classes agreeing under a cutoff pair identically against anything the cutoff fixes. Where θ·X = θ·Y almost everywhere and θψ = ψ pointwise, the pairings against ψ agree.

This is how an identification valid only after a cutoff is used: every weight the datum assembly pairs against is supported where the outer cutoff of the tower is identically 1, so θψ = ψ there and the cutoff disappears from the conclusion.

theorem EllipticPdes.Regularity.setIntegral_weight_mul_congr_of_cutoff_ae {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {θ : EuclideanSpace ℝ (Fin d) → ℝ} {X Y : Sobolev.L2D V} (h : (fun (x : EuclideanSpace ℝ (Fin d)) => θ x * ↑↑X x) =ᵐ[MeasureTheory.volume.restrict V] fun (x : EuclideanSpace ℝ (Fin d)) => θ x * ↑↑Y x) (a : EuclideanSpace ℝ (Fin d) → ℝ) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ∀ (x : EuclideanSpace ℝ (Fin d)), θ x * ψ x = ψ x) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, a x * ↑↑X x * ψ x = ∫ (x : EuclideanSpace ℝ (Fin d)) in V, a x * ↑↑Y x * ψ x

The same with a weight in front, which is the shape every block of the bilinear form takes. The cutoff passes through the weight, so the hypothesis is unchanged.

theorem EllipticPdes.Regularity.setIntegral_add_weight_mul_cutoff {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {a₁ a₂ : EuclideanSpace ℝ (Fin d) → ℝ} (h₁m : Measurable a₁) {M₁ : ℝ} (h₁b : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a₁ x| ≤ M₁) (h₂m : Measurable a₂) {M₂ : ℝ} (h₂b : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a₂ x| ≤ M₂) (p₁ p₂ : Sobolev.L2D V) {ξ v : EuclideanSpace ℝ (Fin d) → ℝ} (hξc : ContDiff ℝ (↑⊤) ξ) (hξcs : HasCompactSupport ξ) (hvc : ContDiff ℝ (↑⊤) v) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, (a₁ x * ↑↑p₁ x + a₂ x * ↑↑p₂ x) * (ξ x * v x) = (∫ (x : EuclideanSpace ℝ (Fin d)) in V, ξ x * (a₁ x * ↑↑p₁ x) * v x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ξ x * (a₂ x * ↑↑p₂ x) * v x

Sum of two weighted classes paired against a cut-off test function. The differentiated equation groups its datum two terms at a time, one with a derivative of a coefficient and one with a derivative of the solution, and the datum of the induction step names them separately. This is the split, with the cutoff moved to the front where the datum has it.

theorem EllipticPdes.Regularity.setIntegral_mulL2_mul_testFn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {a : EuclideanSpace ℝ (Fin d) → ℝ} (ham : Measurable a) {M : ℝ} (haM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |a x| ≤ M) (p : Sobolev.L2D V) (φ : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in V, ↑↑(mulL2 ham haM p) x * φ x = ∫ (x : EuclideanSpace ℝ (Fin d)) in V, a x * ↑↑p x * φ x

A weighted class pairs as the weight against the class.