A constant is a distributional solution of the drift-diffusion equation

For every admissible drift (B, div B) (IsAdmissibleDrift) and every constant c, the constant function is a distributional solution of eq:aniso:comparison:equation on Vec m × I (IsDistributionalDriftDiffusion): against any test function φ, each of the three pairings ∫ timeDeriv φ, ∫ partialLaplacian φ, and ∫ (gradPair φ (B·) + div B · φ) vanishes over the whole space, the first two because a compactly supported smooth function's directional derivative integrates to zero, the third by Fubini together with the admissible drift's weak-divergence identity isAdmissibleDrift_weak_divergence.

Bridging the frozen slice derivatives to the joint fderiv

theorem CIV.fderiv_slice_fst_eq {m : ℕ} {ψ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hψ : DifferentiableAt ℝ ψ z) (v : CKN.Vec m) : (fderiv ℝ (fun (x : CKN.Vec m) => ψ (x, z.2)) z.1) v = (fderiv ℝ ψ z) (v, 0)

The spatial slice derivative of a joint function at a fixed time is the joint derivative paired with a spatial direction.

theorem CIV.fderiv_slice_snd_eq {m : ℕ} {ψ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hψ : DifferentiableAt ℝ ψ z) (h : ℝ) : (fderiv ℝ (fun (τ : ℝ) => ψ (z.1, τ)) z.2) h = (fderiv ℝ ψ z) (0, h)

The time slice derivative of a joint function at a fixed point is the joint derivative paired with the time direction.

theorem CIV.timeDeriv_eq_fderiv_apply {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hφ : DifferentiableAt ℝ φ z) : timeDeriv m φ z = (fderiv ℝ φ z) (0, 1)

theorem CIV.gradPair_eq_fderiv_apply {m : ℕ} {ψ : CKN.Vec m × ℝ → ℝ} {z : CKN.Vec m × ℝ} (hψ : DifferentiableAt ℝ ψ z) (v : CKN.Vec m) : gradPair m ψ z v = (fderiv ℝ ψ z) (v, 0)

Compact support and continuity of the spatial slice and its gradient pairing

theorem CIV.hasCompactSupport_slice_fst {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} (hsupp : HasCompactSupport φ) (τ : ℝ) : HasCompactSupport fun (x : CKN.Vec m) => φ (x, τ)

theorem CIV.continuous_gradPair_joint {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (v : CKN.Vec m) : Continuous fun (z : CKN.Vec m × ℝ) => gradPair m φ z v

theorem CIV.hasCompactSupport_gradPair_joint {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : HasCompactSupport φ) (v : CKN.Vec m) : HasCompactSupport fun (z : CKN.Vec m × ℝ) => gradPair m φ z v

theorem CIV.tsupport_gradPair_joint_subset {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (v : CKN.Vec m) : (tsupport fun (z : CKN.Vec m × ℝ) => gradPair m φ z v) ⊆ tsupport φ

From a slicewise a.e. property to the product-measure a.e. property

theorem CIV.ae_prod_of_ae_forall {m : ℕ} {J : Set ℝ} {P : ℝ → Prop} {Q : CKN.Vec m → ℝ → Prop} (hP : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict J, P τ) (hQ : ∀ (τ : ℝ), P τ → ∀ (x : CKN.Vec m), Q x τ) : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J), Q z.1 z.2

theorem CIV.isLocallyBoundedOn_divB_of_isAdmissibleDrift {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) : IsLocallyBoundedOn m I divB

theorem CIV.isLocallyBoundedOn_component_of_isAdmissibleDrift {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (i : Fin m) : IsLocallyBoundedOn m I fun (z : CKN.Vec m × ℝ) => B z i

A compactly supported smooth function's directional derivative integrates to zero

theorem CIV.isAddHaarMeasure_volume_prod (m : ℕ) : MeasureTheory.volume.IsAddHaarMeasure

theorem CIV.integrable_fderiv_apply_of_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {k : E → ℝ} (hk : ContDiff ℝ (↑⊤) k) (hsupp : HasCompactSupport k) (v : E) : MeasureTheory.Integrable (fun (x : E) => (fderiv ℝ k x) v) μ

A directional derivative of a compactly supported smooth function is globally integrable against any additive Haar measure.

theorem CIV.integral_fderiv_apply_eq_zero_of_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {k : E → ℝ} (hk : ContDiff ℝ (↑⊤) k) (hsupp : HasCompactSupport k) (v : E) : ∫ (x : E), (fderiv ℝ k x) v ∂μ = 0

A compactly supported smooth function's directional derivative integrates to zero over the whole space, for any additive Haar measure. This is the divergence theorem for a single direction, with no boundary term since k vanishes outside a compact set.

The time-derivative and Laplacian pairings vanish over the whole space

theorem CIV.integrable_timeDeriv_of_testFunction {m : ℕ} {I : Set ℝ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => timeDeriv m φ z) MeasureTheory.volume

The time derivative of a test function is globally integrable.

theorem CIV.integral_timeDeriv_eq_zero {m : ℕ} {I : Set ℝ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : ∫ (z : CKN.Vec m × ℝ), timeDeriv m φ z = 0

The integral over the whole space of a test function's time derivative vanishes.

theorem CIV.integrable_partialLaplacian_of_testFunction {m : ℕ} (d : ℕ) {I : Set ℝ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => partialLaplacian m d φ z) MeasureTheory.volume

The partial Laplacian of a test function is globally integrable.

theorem CIV.integral_partialLaplacian_eq_zero {m : ℕ} (d : ℕ) {I : Set ℝ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : φ ∈ testFunctions m I) : ∫ (z : CKN.Vec m × ℝ), partialLaplacian m d φ z = 0

The integral over the whole space of a test function's partial Laplacian vanishes.

The drift pairing is globally integrable and its total pairing vanishes

theorem CIV.integrable_divB_mul_of_isAdmissibleDrift {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB φ : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hφ : φ ∈ testFunctions m I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => divB z * φ z) MeasureTheory.volume

theorem CIV.integrable_gradPair_mul_of_isAdmissibleDrift {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB φ : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hφ : φ ∈ testFunctions m I) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => gradPair m φ z (B z)) MeasureTheory.volume

theorem CIV.integral_gradPair_add_divB_mul_eq_zero {m : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB φ : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hφ : φ ∈ testFunctions m I) : ∫ (z : CKN.Vec m × ℝ), gradPair m φ z (B z) + divB z * φ z = 0

The two commutator-drift terms of the distributional pairing, integrated jointly against a test function, cancel: the divergence theorem for the truncated Laplacian's first-order sibling.

The main theorem

theorem CIV.isDistributionalDriftDiffusion_const {m d : ℕ} {I : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (c : ℝ) : IsDistributionalDriftDiffusion m d I B divB fun (x : CKN.Vec m × ℝ) => c

A constant is a distributional solution of eq:aniso:comparison:equation for every admissible drift. Against any test function φ, the pairing splits into the time derivative, the Laplacian, and the drift terms, each of which integrates to zero over the whole space (integral_timeDeriv_eq_zero, integral_partialLaplacian_eq_zero, integral_gradPair_add_divB_mul_eq_zero), so the total pairing against the constant c vanishes as well.