The weak form of a drift-diffusion equation on Vec 5 × ℝ off a closed set

The operators timeDeriv, gradPair and partialLaplacian acting on a smooth test function are full Fréchet derivatives in the corresponding directions (timeDeriv_eq_fderiv, gradPair_eq_fderiv, partialLaplacian_eq_fderiv).

If a scalar q, a drift B with divergence divB, a flux F and a source G are smooth on an open set S of the lifted variables (X, Z, τ) ∈ ℝ⁴ × ℝ × ℝ and satisfy there, pointwise, ∂_τ q + B · ∇q = Δ_X q + κ ∂_ZZ q + ∂_Z F + G, then against every test function supported in S the pairing of q with the adjoint operator of eq:aniso:zoom:finite:limit equals κ ∫ q ∂_ZZ ψ - ∫ F ∂_Z ψ + ∫ G ψ (integral_liftedResidual_eq). This is the integration by parts of the passage to the limit (deviation D17), performed off the axis.

theorem CIV.fderiv_slice_fst_apply {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {x : CKN.Vec m} {t : ℝ} (hφ : DifferentiableAt ℝ φ (x, t)) (v : CKN.Vec m) : (fderiv ℝ (fun (y : CKN.Vec m) => φ (y, t)) x) v = (fderiv ℝ φ (x, t)) (v, 0)

The derivative of the spatial slice of a function of Vec m × ℝ is its full derivative in the corresponding spatial direction.

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

The time derivative of a test function is its full derivative in the direction (0, 1).

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

The spatial gradient pairing of a test function is its full derivative in the direction (v, 0).

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

The gradient pairing expands along the coordinate basis.

theorem CIV.partialLaplacian_eq_fderiv {m d : ℕ} {φ : CKN.Vec m × ℝ → ℝ} (hφ : ContDiff ℝ 2 φ) (z : CKN.Vec m × ℝ) : partialLaplacian m d φ z = ∑ i : Fin m, if ↑i < d then (fderiv ℝ (fun (w : CKN.Vec m × ℝ) => (fderiv ℝ φ w) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0) else 0

The partial Laplacian of a C² test function in terms of full second derivatives.

theorem CIV.contDiffOn_fderiv_apply_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} (hS : IsOpen S) {h : E → ℝ} (hh : ContDiffOn ℝ (↑⊤) h S) (v : E) : ContDiffOn ℝ (↑⊤) (fun (z : E) => (fderiv ℝ h z) v) S

Directional derivatives of a function smooth on an open set are smooth there.

theorem CIV.contDiff_fderiv_apply_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} (hh : ContDiff ℝ (↑⊤) h) (v : E) : ContDiff ℝ ↑⊤ fun (z : E) => (fderiv ℝ h z) v

Directional derivatives of a smooth function are smooth.

theorem CIV.integrable_of_continuousOn_of_forall_notMem {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [T2Space E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {S K : Set E} (hK : IsCompact K) (hKS : K ⊆ S) {f : E → ℝ} (hf : ContinuousOn f S) (h0 : ∀ z ∉ K, f z = 0) : MeasureTheory.Integrable f μ

A function continuous on an open set S and vanishing off a compact K ⊆ S is integrable.

theorem CIV.integrable_and_integral_ibpPair_eq_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {S K : Set E} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {h χ : E → ℝ} (hh : ContDiffOn ℝ (↑⊤) h S) (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχK : tsupport χ ⊆ K) (v : E) : MeasureTheory.Integrable (fun (z : E) => h z * (fderiv ℝ χ z) v + (fderiv ℝ h z) v * χ z) μ ∧ ∫ (z : E), h z * (fderiv ℝ χ z) v + (fderiv ℝ h z) v * χ z ∂μ = 0

One integration by parts, as a pair of integrable terms with vanishing total integral.

theorem CIV.integrable_and_integral_finset_sum_eq_zero {E : Type u_1} {ι : Type u_2} [MeasurableSpace E] {μ : MeasureTheory.Measure E} (s : Finset ι) {f : ι → E → ℝ} (hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ ∧ ∫ (z : E), f i z ∂μ = 0) : MeasureTheory.Integrable (fun (z : E) => ∑ i ∈ s, f i z) μ ∧ ∫ (z : E), ∑ i ∈ s, f i z ∂μ = 0

Functions that are integrable with vanishing integral are closed under finite sums.

theorem CIV.integrable_and_integral_add_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {f g : E → ℝ} (hf : MeasureTheory.Integrable f μ ∧ ∫ (z : E), f z ∂μ = 0) (hg : MeasureTheory.Integrable g μ ∧ ∫ (z : E), g z ∂μ = 0) : MeasureTheory.Integrable (fun (z : E) => f z + g z) μ ∧ ∫ (z : E), f z + g z ∂μ = 0

Functions that are integrable with vanishing integral are closed under addition.

theorem CIV.integrable_and_integral_sub_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {f g : E → ℝ} (hf : MeasureTheory.Integrable f μ ∧ ∫ (z : E), f z ∂μ = 0) (hg : MeasureTheory.Integrable g μ ∧ ∫ (z : E), g z ∂μ = 0) : MeasureTheory.Integrable (fun (z : E) => f z - g z) μ ∧ ∫ (z : E), f z - g z ∂μ = 0

Functions that are integrable with vanishing integral are closed under subtraction.

theorem CIV.integrable_and_integral_neg_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {f : E → ℝ} (hf : MeasureTheory.Integrable f μ ∧ ∫ (z : E), f z ∂μ = 0) : MeasureTheory.Integrable (fun (z : E) => -f z) μ ∧ ∫ (z : E), -f z ∂μ = 0

Functions that are integrable with vanishing integral are closed under negation.

theorem CIV.integrable_and_integral_const_mul_eq_zero {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {f : E → ℝ} (c : ℝ) (hf : MeasureTheory.Integrable f μ ∧ ∫ (z : E), f z ∂μ = 0) : MeasureTheory.Integrable (fun (z : E) => c * f z) μ ∧ ∫ (z : E), c * f z ∂μ = 0

Functions that are integrable with vanishing integral are closed under scaling.

theorem CIV.sum_fin_five_ite_lt_four (a : Fin 5 → ℝ) : (∑ i : Fin 5, if ↑i < 4 then a i else 0) = a 0 + a 1 + a 2 + a 3

The sum of the first four of five terms, written as the masked sum of partialLaplacian.

theorem CIV.fderiv_apply_eq_zero_of_notMem_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {z : E} (hz : z ∉ tsupport ψ) (v : E) : (fderiv ℝ ψ z) v = 0

A derivative of a test function vanishes off its topological support.

theorem CIV.integral_liftedResidual_eq {S K : Set (CKN.Vec 5 × ℝ)} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {q Fz G divB : CKN.Vec 5 × ℝ → ℝ} {B : CKN.Vec 5 × ℝ → CKN.Vec 5} (κ : ℝ) (hq : ContDiffOn ℝ (↑⊤) q S) (hB : ∀ (i : Fin 5), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Vec 5 × ℝ) => B z i) S) (hF : ContDiffOn ℝ (↑⊤) Fz S) (hG : ContinuousOn G S) (hdiv : ∀ z ∈ S, ∑ i : Fin 5, (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => B w i) z) (CKN.basisVec i, 0) = divB z) (hpde : ∀ z ∈ S, (fderiv ℝ q z) (0, 1) + ∑ i : Fin 5, B z i * (fderiv ℝ q z) (CKN.basisVec i, 0) = (∑ i : Fin 5, if ↑i < 4 then (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ q w) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0) else 0) + κ * (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ q w) (CKN.basisVec 4, 0)) z) (CKN.basisVec 4, 0) + (fderiv ℝ Fz z) (CKN.basisVec 4, 0) + G z) {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψK : tsupport ψ ⊆ K) : ∫ (z : CKN.Vec 5 × ℝ), q z * (-timeDeriv 5 ψ z - gradPair 5 ψ z (B z) - divB z * ψ z - partialLaplacian 5 4 ψ z) = ∫ (z : CKN.Vec 5 × ℝ), κ * q z * (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ ψ w) (CKN.basisVec 4, 0)) z) (CKN.basisVec 4, 0) - Fz z * (fderiv ℝ ψ z) (CKN.basisVec 4, 0) + G z * ψ z

The integration by parts of the passage to the limit off the axis: if q, the drift B, the flux F and the source G satisfy ∂_τ q + B · ∇q = Δ_X q + κ ∂_ZZ q + ∂_Z F + G pointwise on an open set S, with divB the divergence of B there, then against every test function supported in a compact subset of S the residual of eq:aniso:zoom:finite:limit is κ ∫ q ∂_ZZ ψ - ∫ F ∂_Z ψ + ∫ G ψ.