The mollified equation of lem:aniso:comparison

Mollifying eq:aniso:comparison:equation in space turns a bounded distributional solution into the pointwise-in-space identity eq:aniso:comparison:mollified,

∂_τ q_ε + B·∇q_ε = Δ_X q_ε + R_ε,

where q_ε = η_ε * q is the spatial mollification of q and R_ε is the commutator of DiPerna and Lions. This module proves that identity in the form in which the distributional hypothesis delivers it: for every scalar test function χ of time supported in I,

∫ q_ε(x, τ) (-χ'(τ)) dτ = ∫ χ(τ) (Δ_X q_ε - ∇q_ε·B + R_ε)(x, τ) dτ.

The proof tests the distributional equation with the product φ(y, τ) = η_ε(x - y) χ(τ), computes the three derivatives of φ in closed form, exchanges the order of integration, and reassembles the drift and divergence contributions into the explicit integral form of diPernaLionsCommutator by adding and subtracting B(x, τ)·∇q_ε(x, τ).

Coordinates of a continuous linear form

theorem CIV.apply_eq_sum_basisVec {m : ℕ} (L : CKN.Vec m →L[ℝ] ℝ) (v : CKN.Vec m) : L v = ∑ i : Fin m, v i * L (CKN.basisVec i)

A continuous linear form on Vec m is determined by its values on the coordinate basis.

Smoothness of a directional derivative

theorem CIV.contDiff_fderiv_apply {m : ℕ} {k : CKN.Vec m → ℝ} (hk : ContDiff ℝ (↑⊤) k) (v : CKN.Vec m) : ContDiff ℝ ↑⊤ fun (w : CKN.Vec m) => (fderiv ℝ k w) v

A directional derivative of a smooth function is smooth.

theorem CIV.hasCompactSupport_fderiv_apply {m : ℕ} {k : CKN.Vec m → ℝ} (hk : HasCompactSupport k) (v : CKN.Vec m) : HasCompactSupport fun (w : CKN.Vec m) => (fderiv ℝ k w) v

A directional derivative of a compactly supported function is compactly supported.

The chain rule for the reflected kernel

theorem CIV.fderiv_const_sub_mul_const {m : ℕ} {k : CKN.Vec m → ℝ} (hk : Differentiable ℝ k) (x : CKN.Vec m) (c : ℝ) (y v : CKN.Vec m) : (fderiv ℝ (fun (y' : CKN.Vec m) => k (x - y') * c) y) v = -(fderiv ℝ k (x - y)) v * c

The derivative of y ↦ k (x - y) c in the direction v.

The product test function

noncomputable def CIV.mollifierTest (m : ℕ) (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) (z : CKN.Vec m × ℝ) : ℝ

The test function φ(y, τ) = η_ε(x - y) χ(τ) used to mollify the equation at x.

Equations

• CIV.mollifierTest m ε x χ z = CIV.mollifierKernel m ε (x - z.1) * χ z.2

theorem CIV.mollifierTest_apply {m : ℕ} (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) (y : CKN.Vec m) (τ : ℝ) : mollifierTest m ε x χ (y, τ) = mollifierKernel m ε (x - y) * χ τ

theorem CIV.contDiff_mollifierTest {m : ℕ} (ε : ℝ) (x : CKN.Vec m) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) : ContDiff ℝ (↑⊤) (mollifierTest m ε x χ)

The test function is smooth.

theorem CIV.mollifierTest_eq_zero {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) (χ : ℝ → ℝ) {z : CKN.Vec m × ℝ} (hz : z ∉ Metric.closedBall x ε ×ˢ tsupport χ) : mollifierTest m ε x χ z = 0

The test function vanishes off a product of the closed ε-ball with the support of χ.

theorem CIV.hasCompactSupport_mollifierTest {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {χ : ℝ → ℝ} (hχc : HasCompactSupport χ) : HasCompactSupport (mollifierTest m ε x χ)

The test function has compact support.

theorem CIV.tsupport_mollifierTest_subset {m : ℕ} (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) : tsupport (mollifierTest m ε x χ) ⊆ Set.univ ×ˢ tsupport χ

The support of the test function lies over the support of χ.

theorem CIV.mollifierTest_mem_testFunctions {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {I : Set ℝ} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχI : tsupport χ ⊆ I) : mollifierTest m ε x χ ∈ testFunctions m I

Stage (i): the product η_ε(x - ·) χ is a test function on Vec m × I.

The second-order kernel

noncomputable def CIV.partialLaplacianKernel (m d : ℕ) (ε : ℝ) (w : CKN.Vec m) : ℝ

The partial Laplacian, in the first d coordinates, of the kernel η_ε.

Equations

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

theorem CIV.continuous_partialLaplacianKernel (m d : ℕ) (ε : ℝ) : Continuous (partialLaplacianKernel m d ε)

theorem CIV.hasCompactSupport_partialLaplacianKernel {m : ℕ} (d : ℕ) {ε : ℝ} (hε : 0 < ε) : HasCompactSupport (partialLaplacianKernel m d ε)

Stage (ii): the derivatives of the test function

theorem CIV.timeDeriv_mollifierTest {m : ℕ} (ε : ℝ) (x : CKN.Vec m) {χ : ℝ → ℝ} (hχ : Differentiable ℝ χ) (y : CKN.Vec m) (τ : ℝ) : timeDeriv m (mollifierTest m ε x χ) (y, τ) = mollifierKernel m ε (x - y) * deriv χ τ

The time derivative of φ(y, τ) = η_ε(x - y) χ(τ).

theorem CIV.gradPair_mollifierTest {m : ℕ} (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) (y : CKN.Vec m) (τ : ℝ) (v : CKN.Vec m) : gradPair m (mollifierTest m ε x χ) (y, τ) v = -(fderiv ℝ (mollifierKernel m ε) (x - y)) v * χ τ

The spatial gradient of φ(y, τ) = η_ε(x - y) χ(τ) paired with a vector.

theorem CIV.fderiv_slice_mollifierTest {m : ℕ} (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) (τ : ℝ) (v : CKN.Vec m) : (fun (y : CKN.Vec m) => (fderiv ℝ (fun (y' : CKN.Vec m) => mollifierTest m ε x χ (y', τ)) y) v) = fun (y : CKN.Vec m) => (fderiv ℝ (mollifierKernel m ε) (x - y)) v * -χ τ

The first spatial derivative of φ(y, τ) = η_ε(x - y) χ(τ) as a function of the base point, in the direction v.

theorem CIV.partialLaplacian_mollifierTest {m : ℕ} (d : ℕ) (ε : ℝ) (x : CKN.Vec m) (χ : ℝ → ℝ) (y : CKN.Vec m) (τ : ℝ) : partialLaplacian m d (mollifierTest m ε x χ) (y, τ) = partialLaplacianKernel m d ε (x - y) * χ τ

The partial Laplacian of φ(y, τ) = η_ε(x - y) χ(τ).

Derivatives of an integral against a smooth compactly supported kernel

theorem CIV.mollifySlice_apply {m : ℕ} (ε : ℝ) (q : CKN.Vec m × ℝ → ℝ) (x : CKN.Vec m) (τ : ℝ) : mollifySlice m ε q (x, τ) = ∫ (y : CKN.Vec m), mollifierKernel m ε (x - y) * q (y, τ)

theorem CIV.fderiv_kernelIntegral {m : ℕ} {k : CKN.Vec m → ℝ} (hk : ContDiff ℝ (↑⊤) k) (hkc : HasCompactSupport k) {g : CKN.Vec m → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (x v : CKN.Vec m) : (fderiv ℝ (fun (x' : CKN.Vec m) => ∫ (y : CKN.Vec m), k (x' - y) * g y) x) v = ∫ (y : CKN.Vec m), (fderiv ℝ k (x - y)) v * g y

Differentiating under the integral sign against a smooth compactly supported kernel.

theorem CIV.integrable_kernel_mul {m : ℕ} {k : CKN.Vec m → ℝ} (hk : Continuous k) (hkc : HasCompactSupport k) {g : CKN.Vec m → ℝ} {M : ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |g y| ≤ M) (x : CKN.Vec m) : MeasureTheory.Integrable (fun (y : CKN.Vec m) => k (x - y) * g y) MeasureTheory.volume

Integrability of a bounded measurable function against a continuous compactly supported kernel.

theorem CIV.gradPair_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) (q : CKN.Vec m × ℝ → ℝ) (τ M : ℝ) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x v : CKN.Vec m) : gradPair m (mollifySlice m ε q) (x, τ) v = ∫ (y : CKN.Vec m), (fderiv ℝ (mollifierKernel m ε) (x - y)) v * q (y, τ)

The spatial gradient of the mollified slice, obtained by moving ∇ onto the kernel.

theorem CIV.partialLaplacian_mollifySlice {m : ℕ} (d : ℕ) {ε : ℝ} (hε : 0 < ε) (q : CKN.Vec m × ℝ → ℝ) (τ M : ℝ) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x : CKN.Vec m) : partialLaplacian m d (mollifySlice m ε q) (x, τ) = ∫ (y : CKN.Vec m), partialLaplacianKernel m d ε (x - y) * q (y, τ)

The partial Laplacian of the mollified slice, obtained by moving Δ_X onto the kernel.

The tested integrand vanishes off the support of the test function

theorem CIV.timeDeriv_eq_zero_of_notMem_tsupport {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hz : z ∉ tsupport φ) : timeDeriv m φ z = 0

The time derivative of a test function vanishes off its support.

theorem CIV.gradPair_eq_zero_of_notMem_tsupport {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hz : z ∉ tsupport φ) (v : CKN.Vec m) : gradPair m φ z v = 0

The spatial gradient of a test function vanishes off its support.

theorem CIV.partialLaplacian_eq_zero_of_notMem_tsupport {m : ℕ} (d : ℕ) {φ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hz : z ∉ tsupport φ) : partialLaplacian m d φ z = 0

The partial Laplacian of a test function vanishes off its support.

theorem CIV.testedIntegrand_eq_zero_of_notMem_tsupport {m : ℕ} (d : ℕ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q φ : CKN.Vec m × ℝ → ℝ) {z : CKN.Vec m × ℝ} (hz : z ∉ tsupport φ) : q z * (-timeDeriv m φ z - gradPair m φ z (B z) - divB z * φ z - partialLaplacian m d φ z) = 0

The integrand of IsDistributionalDriftDiffusion vanishes off the support of the test function.

Stage (iii): the tested equation with the order of integration exchanged

theorem CIV.integrable_testedIntegrand {m : ℕ} (d : ℕ) {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (heq : IsDistributionalDriftDiffusion m d I B divB q) {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => q z * (-timeDeriv m φ z - gradPair m φ z (B z) - divB z * φ z - partialLaplacian m d φ z)) MeasureTheory.volume

The integrand of IsDistributionalDriftDiffusion is integrable on all of Vec m × ℝ.

theorem CIV.integral_integral_testedIntegrand {m : ℕ} (d : ℕ) {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (heq : IsDistributionalDriftDiffusion m d I B divB q) {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : ∫ (τ : ℝ) (y : CKN.Vec m), q (y, τ) * (-timeDeriv m φ (y, τ) - gradPair m φ (y, τ) (B (y, τ)) - divB (y, τ) * φ (y, τ) - partialLaplacian m d φ (y, τ)) = 0

Stage (iii): the tested equation, with the space integral inside the time integral.

theorem CIV.integral_add_four {m : ℕ} {f₁ f₂ f₃ f₄ : CKN.Vec m → ℝ} (h₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (h₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (h₃ : MeasureTheory.Integrable f₃ MeasureTheory.volume) (h₄ : MeasureTheory.Integrable f₄ MeasureTheory.volume) : ∫ (y : CKN.Vec m), f₁ y + f₂ y + f₃ y + f₄ y = (((∫ (y : CKN.Vec m), f₁ y) + ∫ (y : CKN.Vec m), f₂ y) + ∫ (y : CKN.Vec m), f₃ y) + ∫ (y : CKN.Vec m), f₄ y

Linearity of the integral over a sum of four integrable functions.

Stage (iv): one time slice of the tested equation

theorem CIV.integral_slice_testedIntegrand {m : ℕ} (d : ℕ) {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} {χ : ℝ → ℝ} (hχ : Differentiable ℝ χ) {τ M : ℝ} {Λ : NNReal} (hqm : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hqb : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (hBm : Measurable fun (y : CKN.Vec m) => B (y, τ)) (hdm : Measurable fun (y : CKN.Vec m) => divB (y, τ)) (hBb : ∀ (y : CKN.Vec m), ‖B (y, τ)‖ ≤ ↑Λ) (hdb : ∀ (y : CKN.Vec m), |divB (y, τ)| ≤ ↑Λ) : ∫ (y : CKN.Vec m), q (y, τ) * (-timeDeriv m (mollifierTest m ε x χ) (y, τ) - gradPair m (mollifierTest m ε x χ) (y, τ) (B (y, τ)) - divB (y, τ) * mollifierTest m ε x χ (y, τ) - partialLaplacian m d (mollifierTest m ε x χ) (y, τ)) = mollifySlice m ε q (x, τ) * -deriv χ τ - χ τ * (partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x)

On a time slice on which q is bounded and the drift obeys eq:aniso:comparison:drift, the space integral of the tested integrand is the slice of the mollified equation: adding and subtracting B(x, τ)·∇q_ε(x, τ) turns the drift and divergence contributions into the explicit integral form of diPernaLionsCommutator.

Integrability of the mollified slice against a test function of time

theorem CIV.integrable_of_vanishing_outside {m : ℕ} {J : Set ℝ} (hJ : MeasurableSet J) {f : CKN.Vec m × ℝ → ℝ} (hzero : ∀ (z : CKN.Vec m × ℝ), z.2 ∉ J → f z = 0) (hint : MeasureTheory.IntegrableOn f (Set.univ ×ˢ J) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

A function on Vec m × ℝ vanishing off univ ×ˢ J and integrable there is integrable.

theorem CIV.integrable_mul_of_isLocallyBoundedOn {m : ℕ} {I : Set ℝ} {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) {g : CKN.Vec m × ℝ → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) (hgI : tsupport g ⊆ Set.univ ×ˢ I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => g z * q z) MeasureTheory.volume

A locally bounded function is integrable against a continuous compactly supported weight whose support lies over I.

theorem CIV.integrable_mollifySlice_mul {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {I : Set ℝ} {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) {c : ℝ → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hcc : HasCompactSupport c) (hcI : tsupport c ⊆ I) : MeasureTheory.Integrable (fun (τ : ℝ) => mollifySlice m ε q (x, τ) * c τ) MeasureTheory.volume

The mollified slice is integrable in time against a test function of time.

The mollified equation

theorem CIV.mollified_equation (m d : ℕ) (I : Set ℝ) (hI : IsOpen I) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q : CKN.Vec m × ℝ → ℝ) (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) (χ : ℝ → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχI : tsupport χ ⊆ I) : ∫ (τ : ℝ), mollifySlice m ε q (x, τ) * -deriv χ τ = ∫ (τ : ℝ), χ τ * (partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x)

Step 2 of lem:aniso:comparison: the mollified equation eq:aniso:comparison:mollified, tested against a smooth compactly supported function of time supported in I. Here q_ε = mollifySlice m ε q and the commutator of DiPerna and Lions is diPernaLionsCommutator.