Extracting an admissible drift from a sequence of drifts

Generic in the ambient dimension m and the time horizon T: given a sequence of drifts (b n, divb n) that are, eventually in n, bounded and Lipschitz in space on every compact time-window J ⊆ Iic T (deviation D14 in docs/DEVIATIONS.md), this file extracts a subsequence along which (b, divb) converges, in the sense required by CIV.IsAdmissibleDrift, to an admissible drift (B, divB) on Iio T.

The route avoids weak-* (Banach-Alaoglu) compactness, which the hypotheses do not support in general (a bounded, equi-Lipschitz-in-space sequence such as b n (x, τ) = sin (n τ) need not have any pointwise- or weak-*-convergent subsequence in time). Instead it uses:

• time-T-clamped primitives z ↦ ∫ s in (T - 1)..(min z.2 T), φ i n (z.1, s), built from each scalar component of (b, divb), which inherit a joint space-time Lipschitz bound from the space-Lipschitz bound on (b, divb);
• a box-diagonal chaining of the classical (Arzelà-Ascoli) compactness theorem to extract one subsequence along which every primitive converges, locally uniformly, to a continuous limit;
• a from-scratch real-analysis lemma (exists_measurable_ae_hasDerivAt_of_lipschitz_mixed) recovering a Borel, a.e.-Lipschitz-and-bounded classical time-derivative of each limit from its joint Lipschitz structure, via a countable dense set, absolute continuity, the McShane extension of a Lipschitz function, and a limsup/liminf sandwich of difference quotients;
• CIV.ae_weakDiv_of_tendstoUniformlyOn_primitive and CIV.tendsto_integral_mul_of_tendstoUniformlyOn_primitive (CIV/Zoom/DriftLimitPassage.lean), which pass the finite-n weak-divergence identity and the weak-convergence conclusion to the limit along the same subsequence.

The oscillatory example above is fine on this route: a_n → 0 uniformly and the limit drift is 0, matching the conclusion of CIV.exists_subseq_admissibleDrift below.

Chaining finitely many scalar Arzelà–Ascoli extractions

theorem CIV.exists_subseq_forall_tendstoUniformlyOn_of_modulus_finset {X : Type u_1} [MetricSpace X] {ι : Type u_2} (S : Set X) (hS : IsCompact S) (f : ι → ℕ → X → ℝ) (M : ℝ) (s : Finset ι) (hbdd : ∀ i ∈ s, ∀ (n : ℕ), ∀ x ∈ S, |f i n x| ≤ M) (hmod : ∀ i ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ (n : ℕ), ∀ x ∈ S, ∀ y ∈ S, dist x y < δ → |f i n x - f i n y| ≤ ε) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ i ∈ s, ∃ (g : X → ℝ), ContinuousOn g S ∧ TendstoUniformlyOn (fun (n : ℕ) => f i (φ n)) g Filter.atTop S

Chain scalar Arzelà–Ascoli extractions (exists_subseq_tendstoUniformlyOn_of_modulus) over a finite family of scalar sequences sharing one bound and modulus of continuity on a compact set, producing one subsequence along which every member of the family converges uniformly.

theorem CIV.tendstoUniformlyOn_pi_of_forall {X : Type u_1} {ι : Type u_2} [Finite ι] {S : Set X} {F : ℕ → X → ι → ℝ} {g : X → ι → ℝ} (h : ∀ (i : ι), TendstoUniformlyOn (fun (n : ℕ) (x : X) => F n x i) (fun (x : X) => g x i) Filter.atTop S) : TendstoUniformlyOn F g Filter.atTop S

Uniform convergence of every coordinate of a finite-dimensional vector-valued sequence, with a shared subsequence and a shared set, glues into joint uniform convergence in the (sup-metric) product ι → ℝ.

From a mixed Lipschitz bound on a primitive to its a.e.-Lipschitz time-derivative

theorem CIV.exists_measurable_ae_hasDerivAt_of_lipschitz_mixed {m : ℕ} {F : CKN.Vec m × ℝ → ℝ} (hFc : Continuous F) (hmix : ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ (∀ (x : CKN.Vec m), LipschitzOnWith Λ.toNNReal (fun (τ : ℝ) => F (x, τ)) (Set.Icc c d)) ∧ ∀ (x y : CKN.Vec m), ∀ τ ∈ Set.Icc c d, ∀ τ' ∈ Set.Icc c d, |F (x, τ') - F (x, τ) - (F (y, τ') - F (y, τ))| ≤ Λ * ‖x - y‖ * |τ' - τ|) : ∃ (G : CKN.Vec m × ℝ → ℝ), Measurable G ∧ ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => F (x, τ')) (G (x, τ)) τ) ∧ (∀ (x : CKN.Vec m), |G (x, τ)| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => G (x, τ)

Given F : Vec m × ℝ → ℝ, continuous, such that on every compact time-window Icc c d there is one constant Λ bounding both the time-Lipschitz constant of F(x, ·) (each x) and the "mixed" Lipschitz constant of its increments over [τ, τ'] as a function of x — the structure enjoyed by the time-primitive of a field that is bounded and Lipschitz in space, uniformly in time on Icc c d — the classical (limsup-of-difference-quotients) time-derivative G of F is Borel measurable, and for a.e. τ in every compact time-window it is, at every x, the genuine derivative of F(x, ·), again bounded and Lipschitz in x with the same Λ.

Time-clamped primitives of a globally space-Lipschitz, space-time-bounded family

theorem CIV.abs_min_sub_min_le (a b c : ℝ) : |min a c - min b c| ≤ |a - b|

min is 1-Lipschitz in its first argument.

theorem CIV.exists_subseq_primitives_ae_hasDerivAt {m : ℕ} {T : ℝ} (φ : Option (Fin m) → ℕ → CKN.Vec m × ℝ → ℝ) (hcontJ : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : Option (Fin m)), ContinuousOn (φ i n) K) (hbd : ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic T → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : Option (Fin m)), ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, |φ i n (x, τ)| ≤ Λ ∧ |φ i n (x, τ) - φ i n (y, τ)| ≤ Λ * ‖x - y‖) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ ∃ (p : Option (Fin m) → CKN.Vec m × ℝ → ℝ), (∀ (i : Option (Fin m)), Continuous (p i)) ∧ (∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → ∀ (i : Option (Fin m)), TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec m × ℝ) => ∫ (s : ℝ) in T - 1..min z.2 T, φ i (ψ n) (z.1, s)) (p i) Filter.atTop K) ∧ ∀ (i : Option (Fin m)), ∃ (B : CKN.Vec m × ℝ → ℝ), Measurable B ∧ ∀ (c d : ℝ), c ≤ d → ∃ (Λ : ℝ), 0 ≤ Λ ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc c d), (∀ (x : CKN.Vec m), HasDerivAt (fun (τ' : ℝ) => p i (x, τ')) (B (x, τ)) τ) ∧ (∀ (x : CKN.Vec m), |B (x, τ)| ≤ Λ) ∧ LipschitzWith Λ.toNNReal fun (x : CKN.Vec m) => B (x, τ)

Given m + 1 families of scalar fields φ i n (indexed by Option (Fin m), standing for the m components of a drift plus its divergence) that are, eventually in n, globally Λ-Lipschitz in space and Λ-bounded on every time-window J compact in Iic T — the structure hbd of eq:aniso:comparison:drift — the time-T-clamped primitives z ↦ ∫_{T-1}^{min(z.2,T)} φ i n (z.1, s) ds converge, along one common subsequence, locally uniformly to continuous limits p i, each of which has a Borel, a.e.-Lipschitz-and-bounded time-derivative on every compact time-window (via exists_measurable_ae_hasDerivAt_of_lipschitz_mixed).

def CIV.packBD {m : ℕ} (b : ℕ → CKN.Vec m × ℝ → CKN.Vec m) (divb : ℕ → CKN.Vec m × ℝ → ℝ) : Option (Fin m) → ℕ → CKN.Vec m × ℝ → ℝ

Pack b (vector-valued drift) and divb (scalar divergence) into one Option (Fin m) indexed family of scalar fields, with some i picking out the i-th component of b and none picking out divb.

Equations

• CIV.packBD b divb i n z = Option.rec (divb n z) (fun (i0 : Fin m) => b n z i0) i

theorem CIV.exists_subseq_admissibleDrift {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)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ), IsAdmissibleDrift m (Set.Iio T) B divB ∧ ∀ (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-in-time, Lipschitz-in-space extraction of an admissible drift, via the route of deviation D14 (time primitives, box-diagonal Arzelà-Ascoli, and the a.e.-derivative lemma exists_measurable_ae_hasDerivAt_of_lipschitz_mixed above) rather than weak-* compactness. b and divb are packed into one Option (Fin m)-indexed family of scalar fields via packBD, fed to exists_subseq_primitives_ae_hasDerivAt, and the resulting per-component limits and derivatives are reassembled into a vector-valued admissible drift (B, divB); the weak divergence identity and the weak-convergence conclusion are supplied by CIV.ae_weakDiv_of_tendstoUniformlyOn_primitive and CIV.tendsto_integral_mul_of_tendstoUniformlyOn_primitive.