Passing a drift-diffusion residual to the limit

Generic in the ambient dimension m, the truncation dimension d, and the time horizon T: given a sequence of scalars qn converging to q in L¹_{loc} and a sequence of drifts (b n, divb n) converging weak-* to an admissible drift (B, divB), this file shows that if the finite-n distributional pairing of qn n against the drift-diffusion residual built from (b n, divb n) tends to zero for every test function, then the limit data (B, divB, q) solves eq:aniso:comparison:equation exactly (CIV.IsDistributionalDriftDiffusion).

The four terms of the residual — the time derivative, the drift-gradient pairing, the divergence pairing, and the truncated Laplacian — are passed to the limit by four different mechanisms: the two terms free of the drift use only the strong L¹_{loc} convergence of qn against a fixed weight, while the two drift terms split into a vanishing piece (handled the same way, since the drift stays uniformly bounded) and a piece driven directly by the weak-* hypothesis. A limit-uniqueness argument against the hypothesis that the finite-n residual itself tends to zero then identifies the sum of the four limits as zero.

Elementary sequence lemmas

theorem CIV.aestronglyMeasurable_finsetSum {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} (s : Finset ι) {f : ι → α → ℝ} (hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEStronglyMeasurable (fun (z : α) => ∑ i ∈ s, f i z) μ

A finite sum of a.e. strongly measurable functions is a.e. strongly measurable.

theorem CIV.tendsto_of_eventually_abs_sub_le {a : ℕ → ℝ} {L : ℝ} {b : ℕ → ℝ} (hb : Filter.Tendsto b Filter.atTop (nhds 0)) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |a n - L| ≤ b n) : Filter.Tendsto a Filter.atTop (nhds L)

If a n is eventually within b n of L and b n → 0, then a n → L.

theorem CIV.tendsto_integral_mul_of_tendsto_lintegral_enorm_zero {m : ℕ} {K : Set (CKN.Vec m × ℝ)} (hK : IsCompact K) {fn gn : ℕ → CKN.Vec m × ℝ → ℝ} (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Vec m × ℝ) in K, ‖fn n z‖ₑ) Filter.atTop (nhds 0)) {C : ℝ} (hbd : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (fn n) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (gn n) (MeasureTheory.volume.restrict K) ∧ ∀ z ∈ K, |gn n z| ≤ C) (hsupp : ∀ (n : ℕ), ∀ z ∉ K, fn n z * gn n z = 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), fn n z * gn n z) Filter.atTop (nhds 0)

A product f_n · g_n, vanishing outside a fixed compact set K, tends to 0 in integral provided f_n → 0 in the L¹(K) sense (∫⁻_K ‖f_n‖ₑ → 0) and g_n is eventually bounded by a fixed constant on K. This is the generic dominated-convergence mechanism behind passing a strongly convergent factor times an eventually-bounded factor to the limit.

theorem CIV.integrableOn_of_bdd_isCompact {m : ℕ} {K : Set (CKN.Vec m × ℝ)} (hK : IsCompact K) {f : CKN.Vec m × ℝ → ℝ} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict K)) {M : ℝ} (hfbd : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict K, |f z| ≤ M) : MeasureTheory.IntegrableOn f K MeasureTheory.volume

A function a.e.-bounded on a compact set is integrable there.

theorem CIV.integrable_mul_of_bdd_isCompact_of_vanishing_outside {m : ℕ} {K : Set (CKN.Vec m × ℝ)} (hK : IsCompact K) {f w : CKN.Vec m × ℝ → ℝ} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict K)) {M : ℝ} (hfbd : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict K, |f z| ≤ M) (hwm : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict K)) {C : ℝ} (hwbd : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict K, |w z| ≤ C) (hsupp : ∀ z ∉ K, f z * w z = 0) : MeasureTheory.Integrable (fun (z : CKN.Vec m × ℝ) => f z * w z) MeasureTheory.volume

A product f · w, with f a.e.-bounded on a compact set K and w a.e.-bounded and vanishing outside K, is globally integrable.

theorem CIV.tendsto_integral_qn_mul_const_of_isLocallyBoundedOn {m : ℕ} {K : Set (CKN.Vec m × ℝ)} (hK : IsCompact K) {qn : ℕ → CKN.Vec m × ℝ → ℝ} {q w : CKN.Vec m × ℝ → ℝ} (hL1 : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Vec m × ℝ) in K, ‖qn n z - q z‖ₑ) Filter.atTop (nhds 0)) {M : ℝ} (hqnbd : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (qn n) (MeasureTheory.volume.restrict K) ∧ ∀ z ∈ K, |qn n z| ≤ M) (hqm : MeasureTheory.AEStronglyMeasurable q (MeasureTheory.volume.restrict K)) (hqbd : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict K, |q z| ≤ M) {C : ℝ} (hwm : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict K)) (hwC : ∀ z ∈ K, |w z| ≤ C) (hwsupp : ∀ z ∉ K, w z = 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), qn n z * w z) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ), q z * w z))

Passing a factor converging strongly in L¹(K) against a fixed weight w, bounded and vanishing outside K, to the limit: the workhorse for the time-derivative and Laplacian pairings, which do not involve the drift.

G-LIMIT

theorem CIV.isDistributionalDriftDiffusion_of_tendsto {m d : ℕ} {T : ℝ} (qn : ℕ → CKN.Vec m × ℝ → ℝ) (q : CKN.Vec m × ℝ → ℝ) (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hB : IsAdmissibleDrift m (Set.Iio T) B divB) (hweak : ∀ (g : CKN.Vec m × ℝ → ℝ), MeasureTheory.Integrable g MeasureTheory.volume → HasCompactSupport g → tsupport g ⊆ Set.univ ×ˢ Set.Iio T → (∀ (i : Fin m), Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), g z * b n z i) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ), g z * B z i))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), g z * divb n z) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ), g z * divB z))) (hq : IsLocallyBoundedOn m (Set.Iio T) q) (hbd : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (qn n) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (b n) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (divb n) (MeasureTheory.volume.restrict K) ∧ ∀ z ∈ K, |qn n z| ≤ M ∧ ‖b n z‖ ≤ M ∧ |divb n z| ≤ M) (hL1 : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio T → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Vec m × ℝ) in K, ‖qn n z - q z‖ₑ) Filter.atTop (nhds 0)) (hres : ∀ φ ∈ testFunctions m (Set.Iio T), Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), qn n z * (-timeDeriv m φ z - gradPair m φ z (b n z) - divb n z * φ z - partialLaplacian m d φ z)) Filter.atTop (nhds 0)) : IsDistributionalDriftDiffusion m d (Set.Iio T) B divB q