Passing the extracted drift to the limit

Given drift fields b n, divb n on Vec m × ℝ satisfying the hypotheses of the generic drift extraction (eventual continuity and per-slice bounds on compacts of Vec m × (-∞, T], and the per-slice weak divergence identity), and a subsequence φ along which the T-clamped time primitives ∫_{T-1}^{min(τ, T)} b_{φ n}(x, s) ds converge locally uniformly to limits a, adiv whose a.e. time derivatives are B, divB (the time-primitive route to eq:aniso:comparison:drift), this file proves:

• CIV.tendsto_integral_mul_of_tendstoUniformlyOn_primitive: b_{φ n} → B and divb_{φ n} → divB weakly against integrable compactly supported test functions on Vec m × (-∞, T);
• CIV.ae_weakDiv_of_tendstoUniformlyOn_primitive: for a.e. τ in every compact J ⊆ (-∞, T), divB(·, τ) is the weak divergence of B(·, τ).

theorem CIV.primitive_sub_eq_of_continuousOn {g : ℝ → ℝ} {c T τ₁ τ₂ : ℝ} (hc : c ≤ T - 1) (hg : ContinuousOn g (Set.Icc c T)) (h1 : c ≤ τ₁) (h2 : c ≤ τ₂) : (∫ (s : ℝ) in T - 1..min τ₂ T, g s) - ∫ (s : ℝ) in T - 1..min τ₁ T, g s = ∫ (s : ℝ) in min τ₁ T..min τ₂ T, g s

The increment of a T-clamped primitive based at T - 1 between two times is the integral between the clamped times.

theorem CIV.abs_primitive_sub_le {g : ℝ → ℝ} {c T τ₁ τ₂ M : ℝ} (hc : c ≤ T - 1) (hg : ContinuousOn g (Set.Icc c T)) (hM : ∀ s ∈ Set.Icc c T, |g s| ≤ M) (h1 : c ≤ τ₁) (h2 : c ≤ τ₂) : |(∫ (s : ℝ) in T - 1..min τ₂ T, g s) - ∫ (s : ℝ) in T - 1..min τ₁ T, g s| ≤ M * |τ₂ - τ₁|

A T-clamped primitive of a function bounded by M on [c, T] is M-Lipschitz on [c, ∞).

theorem CIV.exists_lipschitz_time_of_tendstoUniformlyOn_primitive {m : ℕ} {T : ℝ} (f : ℕ → CKN.Vec m × ℝ → ℝ) (p : CKN.Vec m × ℝ → ℝ) (hcontS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (f n) K) (hbdS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, |f n z| ≤ M) (hconvS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, f n (z.1, s)) p Filter.atTop K) (R c : ℝ) : ∃ (L : ℝ), 0 ≤ L ∧ ∀ x ∈ Metric.closedBall 0 R, ∀ (τ₁ τ₂ : ℝ), c ≤ τ₁ → c ≤ τ₂ → |p (x, τ₂) - p (x, τ₁)| ≤ L * |τ₂ - τ₁|

A locally uniform limit p of T-clamped time primitives of locally bounded, continuous fields is Lipschitz in time, uniformly for x in a ball, on every half-line [c, ∞).

theorem CIV.integral_eq_sub_of_tendstoUniformlyOn_primitive {m : ℕ} {T : ℝ} (f : ℕ → CKN.Vec m × ℝ → ℝ) (p G : CKN.Vec m × ℝ → ℝ) (hcontS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (f n) K) (hbdS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, |f n z| ≤ M) (hconvS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, f n (z.1, s)) p Filter.atTop K) (hGd : ∀ (c d : ℝ), c ≤ d → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => p (x, τ')) (G (x, τ)) τ) (x : CKN.Vec m) {s t : ℝ} (hst : s ≤ t) : ∫ (τ : ℝ) in s..t, G (x, τ) = p (x, t) - p (x, s)

Fundamental theorem of calculus for the limit primitive: if G(x, ·) is a.e. the time derivative of p(x, ·), then ∫_s^t G(x, τ) dτ = p(x, t) - p(x, s) (the limit is Lipschitz in time, hence absolutely continuous).

theorem CIV.ae_restrict_univ_prod_of_ae {m : ℕ} {Q : ℝ → Prop} {c d : ℝ} (h : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), Q τ) : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Icc c d), Q z.2

A property holding for a.e. time in [c, d] holds for a.e. point of Vec m × [c, d].

theorem CIV.integrableOn_prod_Ioc_of_ae_bound {m : ℕ} {G : CKN.Vec m × ℝ → ℝ} (hGm : Measurable G) {s t Λ : ℝ} (hΛ : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc s t), ∀ (x : CKN.Vec m), |G (x, τ)| ≤ Λ) {A : Set (CKN.Vec m)} (hvolA : MeasureTheory.volume A < ⊤) : MeasureTheory.IntegrableOn G (A ×ˢ Set.Ioc s t) MeasureTheory.volume

A measurable field bounded for a.e. time in [s, t] is integrable on A × (s, t] for every A of finite measure.

theorem CIV.tendsto_setIntegral_prod_Ioc_of_primitive {m : ℕ} {T : ℝ} (f : ℕ → CKN.Vec m × ℝ → ℝ) (p G : CKN.Vec m × ℝ → ℝ) (hcontS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (f n) K) (hbdS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, |f n z| ≤ M) (hconvS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, f n (z.1, s)) p Filter.atTop K) (hpc : Continuous p) (hGm : Measurable G) (hGd : ∀ (c d : ℝ), c ≤ d → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => p (x, τ')) (G (x, τ)) τ) (hGb : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), |G (x, τ)| ≤ Λ) {R s t : ℝ} (hst : s ≤ t) (htT : t ≤ T) {A : Set (CKN.Vec m)} (hA : MeasurableSet A) (hAR : A ⊆ Metric.closedBall 0 R) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ) in A ×ˢ Set.Ioc s t, f n z) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ) in A ×ˢ Set.Ioc s t, G z))

Convergence of the integrals of the fields over a bounded space-time rectangle A × (s, t] with t ≤ T: by Fubini both sides are ∫_A of primitive increments, which converge uniformly.

theorem CIV.tendsto_setIntegral_inter_box_of_primitive {m : ℕ} {T : ℝ} (f : ℕ → CKN.Vec m × ℝ → ℝ) (p G : CKN.Vec m × ℝ → ℝ) (hcontS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (f n) K) (hbdS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, |f n z| ≤ M) (hconvS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, f n (z.1, s)) p Filter.atTop K) (hpc : Continuous p) (hGm : Measurable G) (hGd : ∀ (c d : ℝ), c ≤ d → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => p (x, τ')) (G (x, τ)) τ) (hGb : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), |G (x, τ)| ≤ Λ) {R a₀ b₀ : ℝ} (hab : a₀ ≤ b₀) (hbT : b₀ ≤ T) (E : Set (CKN.Vec m × ℝ)) (hE : MeasurableSet E) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ) in E ∩ Metric.closedBall 0 R ×ˢ Set.Ioc a₀ b₀, f n z) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ) in E ∩ Metric.closedBall 0 R ×ˢ Set.Ioc a₀ b₀, G z))

Convergence of the integrals of the fields over E ∩ (B_R × (a₀, b₀]) for every measurable E, by the π-λ theorem from the rectangles A × (l, u]; the countable disjoint unions pass to the limit by dominated convergence of series, using the uniform bound on the fields.

theorem CIV.abs_integral_mul_sub_integral_mul_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F H w : α → ℝ} {C : ℝ} (hF : MeasureTheory.Integrable F μ) (hH : MeasureTheory.Integrable H μ) (hw : MeasureTheory.AEStronglyMeasurable w μ) (hwb : ∀ᵐ (z : α) ∂μ, ‖w z‖ ≤ C) : |∫ (z : α), F z * w z ∂μ - ∫ (z : α), H z * w z ∂μ| ≤ C * ∫ (z : α), ‖F z - H z‖ ∂μ

Testing a weight bounded by C against two integrable functions: the difference of the two pairings is at most C times the L¹ distance.

theorem CIV.tendsto_integral_mul_of_forall_setIntegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : ℕ → α → ℝ) (G : α → ℝ) {M : ℝ} (hf : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (f n) μ ∧ ∀ᵐ (z : α) ∂μ, ‖f n z‖ ≤ M) (hG : MeasureTheory.AEStronglyMeasurable G μ) (hGb : ∀ᵐ (z : α) ∂μ, ‖G z‖ ≤ M) (hset : ∀ (E : Set α), MeasurableSet E → μ E < ⊤ → Filter.Tendsto (fun (n : ℕ) => ∫ (z : α) in E, f n z ∂μ) Filter.atTop (nhds (∫ (z : α) in E, G z ∂μ))) {g : α → ℝ} (hg : MeasureTheory.Integrable g μ) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : α), g z * f n z ∂μ) Filter.atTop (nhds (∫ (z : α), g z * G z ∂μ))

A sequence uniformly bounded by M (eventually) whose integrals over every measurable set of finite measure converge to those of a limit bounded by M converges weakly against every integrable function.

theorem CIV.tendsto_integral_mul_of_tendstoUniformlyOn_primitive_scalar {m : ℕ} {T : ℝ} (f : ℕ → CKN.Vec m × ℝ → ℝ) (p G : CKN.Vec m × ℝ → ℝ) (hcontS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (f n) K) (hbdS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, |f n z| ≤ M) (hconvS : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, f n (z.1, s)) p Filter.atTop K) (hpc : Continuous p) (hGm : Measurable G) (hGd : ∀ (c d : ℝ), c ≤ d → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => p (x, τ')) (G (x, τ)) τ) (hGb : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), ∀ (x : CKN.Vec m), |G (x, τ)| ≤ Λ) {g : CKN.Vec m × ℝ → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hgs : tsupport g ⊆ Set.univ ×ˢ Set.Iic T) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec m × ℝ), g z * f n z) Filter.atTop (nhds (∫ (z : CKN.Vec m × ℝ), g z * G z))

Scalar weak convergence: fields with locally bounded, eventually continuous restrictions to Vec m × (-∞, T] whose T-clamped time primitives converge locally uniformly to p converge weakly, against every integrable compactly supported g with support in Vec m × (-∞, T], to the a.e. time derivative G of p.

theorem CIV.exists_bound_on_compact_of_slice_bounds {m : ℕ} {T : ℝ} (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) (hbd : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖b n (x, τ)‖ ≤ Λ ∧ |divb n (x, τ)| ≤ Λ ∧ ‖b n (x, τ) - b n (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |divb n (x, τ) - divb n (y, τ)| ≤ Λ * ‖x - y‖) (K : Set (CKN.Vec m × ℝ)) (hK : IsCompact K) (hKs : K ⊆ Set.univ ×ˢ Set.Iic T) : ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∈ K, ‖b n z‖ ≤ M ∧ |divb n z| ≤ M

The per-slice bounds of eq:aniso:comparison:drift on balls give eventual bounds on every compact subset of Vec m × (-∞, T].

theorem CIV.tendsto_integral_mul_of_tendstoUniformlyOn_primitive {m : ℕ} {T : ℝ} (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) (hcont : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (b n) K ∧ ContinuousOn (divb n) K) (hbd : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖b n (x, τ)‖ ≤ Λ ∧ |divb n (x, τ)| ≤ Λ ∧ ‖b n (x, τ) - b n (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |divb n (x, τ) - divb n (y, τ)| ≤ Λ * ‖x - y‖) (φ : ℕ → ℕ) (hφ : StrictMono φ) (a : CKN.Vec m × ℝ → CKN.Vec m) (adiv : CKN.Vec m × ℝ → ℝ) (ha : ∀ (i : Fin m), Continuous fun (z : CKN.Vec m × ℝ) => a z i) (hadiv : Continuous adiv) (hconv : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → ∀ (i : Fin m), TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, b (φ n) (z.1, s) i) (fun (z : CKN.Vec m × ℝ) => a z i) Filter.atTop K) (hconvd : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, divb (φ n) (z.1, s)) adiv Filter.atTop K) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hBm : Measurable B) (hdivBm : Measurable divB) (hB : ∀ (i : Fin m) (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => a (x, τ') i) (B (x, τ) i) τ) ∧ (∀ (x : CKN.Vec m), |B (x, τ) i| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => B (x, τ) i) (hdivB : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => adiv (x, τ')) (divB (x, τ)) τ) ∧ (∀ (x : CKN.Vec m), |divB (x, τ)| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => divB (x, τ)) (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))

Weak convergence of the drift and its divergence along the extracted subsequence: the T-clamped time primitives of b ∘ φ and divb ∘ φ converge locally uniformly to a, adiv, whose a.e. time derivatives are B and divB; then ∫ g b_{φ n,i} → ∫ g B_i and ∫ g divb_{φ n} → ∫ g divB for every integrable compactly supported g supported in Vec m × (-∞, T).

theorem CIV.integral_sum_mul_eq_zero_of_primitive {m : ℕ} {T : ℝ} {ι : Type u_1} [Fintype ι] (q : ι → ℕ → CKN.Vec m × ℝ → ℝ) (A : ι → CKN.Vec m × ℝ → ℝ) (W : ι → CKN.Vec m → ℝ) {R : ℝ} (hWc : ∀ (j : ι), Continuous (W j)) (hWs : ∀ (j : ι), ∀ x ∉ Metric.closedBall 0 R, W j x = 0) (hcontS : ∀ (j : ι) (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (q j n) K) (hconvS : ∀ (j : ι) (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, q j n (z.1, s)) (A j) Filter.atTop K) (hAc : ∀ (j : ι), Continuous (A j)) (hzero : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ s ∈ J, ∫ (x : CKN.Vec m), ∑ j : ι, q j n (x, s) * W j x = 0) (τ' : ℝ) : ∫ (x : CKN.Vec m), ∑ j : ι, A j (x, τ') * W j x = 0

If the fields q j n satisfy ∫ Σ_j q_j(x, s) W_j(x) dx = 0 for every time s ≤ T (eventually in n, locally uniformly in s), then so do the limits A j of their T-clamped time primitives, at every time: integrate the identity in time, exchange the integrals, and pass to the limit.

theorem CIV.hasDerivAt_integral_sum_mul_of_lipschitz_time {m : ℕ} {ι : Type u_1} [Fintype ι] (A : ι → CKN.Vec m × ℝ → ℝ) (D W : ι → CKN.Vec m → ℝ) {R τ : ℝ} (hWc : ∀ (j : ι), Continuous (W j)) (hWs : ∀ (j : ι), ∀ x ∉ Metric.closedBall 0 R, W j x = 0) (hAc : ∀ (j : ι), Continuous (A j)) (hlip : ∀ (j : ι), ∃ (L : ℝ), 0 ≤ L ∧ ∀ x ∈ Metric.closedBall 0 R, ∀ (τ₁ τ₂ : ℝ), τ - 1 ≤ τ₁ → τ - 1 ≤ τ₂ → |A j (x, τ₂) - A j (x, τ₁)| ≤ L * |τ₂ - τ₁|) (hder : ∀ (j : ι) (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => A j (x, τ')) (D j x) τ) (hDm : ∀ (j : ι), MeasureTheory.AEStronglyMeasurable (D j) MeasureTheory.volume) : HasDerivAt (fun (τ' : ℝ) => ∫ (x : CKN.Vec m), ∑ j : ι, A j (x, τ') * W j x) (∫ (x : CKN.Vec m), ∑ j : ι, D j x * W j x) τ

Differentiation under the spatial integral of Σ_j A_j(x, τ) W_j(x), for continuous compactly supported weights W_j and fields A_j Lipschitz in time uniformly on the support.

theorem CIV.weakDiv_of_hasDerivAt_slice {m : ℕ} {T : ℝ} (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) (hcont : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (b n) K ∧ ContinuousOn (divb n) K) (hbd : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖b n (x, τ)‖ ≤ Λ ∧ |divb n (x, τ)| ≤ Λ ∧ ‖b n (x, τ) - b n (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |divb n (x, τ) - divb n (y, τ)| ≤ Λ * ‖x - y‖) (hdiv : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∫ (x : CKN.Vec m), divb n (x, τ) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, b n (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)) (φ : ℕ → ℕ) (hφ : StrictMono φ) (a : CKN.Vec m × ℝ → CKN.Vec m) (adiv : CKN.Vec m × ℝ → ℝ) (ha : ∀ (i : Fin m), Continuous fun (z : CKN.Vec m × ℝ) => a z i) (hadiv : Continuous adiv) (hconv : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → ∀ (i : Fin m), TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, b (φ n) (z.1, s) i) (fun (z : CKN.Vec m × ℝ) => a z i) Filter.atTop K) (hconvd : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, divb (φ n) (z.1, s)) adiv Filter.atTop K) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hBm : Measurable B) (hdivBm : Measurable divB) {τ : ℝ} (hderB : ∀ (i : Fin m) (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => a (x, τ') i) (B (x, τ) i) τ) (hbB : ∀ (i : Fin m), ∃ (C : ℝ), ∀ (x : CKN.Vec m), |B (x, τ) i| ≤ C) (hderD : ∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => adiv (x, τ')) (divB (x, τ)) τ) (hbD : ∃ (C : ℝ), ∀ (x : CKN.Vec m), |divB (x, τ)| ≤ C) (ψ : CKN.Vec m → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : CKN.Vec m), divB (x, τ) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, B (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)

The weak-divergence identity at one time τ at which the limit primitives are differentiable in time at every x, with bounded derivatives B(·, τ) and divB(·, τ): the primitive identity holds at all times, and its time derivative at τ is the claim.

theorem CIV.ae_weakDiv_of_tendstoUniformlyOn_primitive {m : ℕ} {T : ℝ} (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) (hcont : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (b n) K ∧ ContinuousOn (divb n) K) (hbd : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖b n (x, τ)‖ ≤ Λ ∧ |divb n (x, τ)| ≤ Λ ∧ ‖b n (x, τ) - b n (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |divb n (x, τ) - divb n (y, τ)| ≤ Λ * ‖x - y‖) (hdiv : ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∫ (x : CKN.Vec m), divb n (x, τ) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, b n (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)) (φ : ℕ → ℕ) (hφ : StrictMono φ) (a : CKN.Vec m × ℝ → CKN.Vec m) (adiv : CKN.Vec m × ℝ → ℝ) (ha : ∀ (i : Fin m), Continuous fun (z : CKN.Vec m × ℝ) => a z i) (hadiv : Continuous adiv) (hconv : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → ∀ (i : Fin m), TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, b (φ n) (z.1, s) i) (fun (z : CKN.Vec m × ℝ) => a z i) Filter.atTop K) (hconvd : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, divb (φ n) (z.1, s)) adiv Filter.atTop K) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hBm : Measurable B) (hdivBm : Measurable divB) (hB : ∀ (i : Fin m) (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => a (x, τ') i) (B (x, τ) i) τ) ∧ (∀ (x : CKN.Vec m), |B (x, τ) i| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => B (x, τ) i) (hdivB : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => adiv (x, τ')) (divB (x, τ)) τ) ∧ (∀ (x : CKN.Vec m), |divB (x, τ)| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => divB (x, τ)) (J : Set ℝ) : IsCompact J → J ⊆ Set.Iio T → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (ψ : CKN.Vec m → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Vec m), divB (x, τ) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, B (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)

The weak-divergence clause of eq:aniso:comparison:drift in the limit: for a.e. τ in every compact J ⊆ (-∞, T), divB(·, τ) is the weak divergence of B(·, τ).