Locally uniform extraction for the rescaled potential vorticity

Step 2 of the finite-h zoom-in argument of Section sec:aniso:zoom, the compactness statement eq:aniso:zoom:finite:compactness: the rescaled potential vorticities Ω_n of eq:aniso:zoom:fields converge, along a subsequence, locally uniformly on {R > 0} × ℝ × (-∞, -1].

The route is the one recorded for prop:aniso:small. Instead of a negative-order Sobolev norm of ∂_τ Ω_n, the regularity in time is carried by a pairing bound

|∫ (Ω_n(·, τ) - Ω_n(·, τ')) ψ| ≤ Cₒ B |τ - τ'|,

for every test function ψ supported in the interior of a closed rectangle K ⊆ {R > 0} and every bound B for ψ and its first two derivatives. Together with a uniform Lipschitz bound in space this gives equicontinuity in time through CIV.equicontinuous_of_lipschitz_of_pairings, hence a space–time modulus of continuity on K ×ˢ J; Arzelà–Ascoli and a diagonal extraction over the rectangles [1/(j+1), j+1] × [-(j+1), j+1] and the time intervals [-(j+1), -1] then produce one subsequence converging uniformly on every compact subset of {R > 0} × ℝ × (-∞, -1].

The file contains, in this order:

• the transport term of eq:aniso:zoom:finite:equation in divergence form, namely V_n ∂_R Ω_n + W_n ∂_Z Ω_n = ∂_R (V_n Ω_n) + ∂_Z (W_n Ω_n) + (V_n / R) Ω_n, which comes from the divergence identity ∂_R V_n + V_n / R + ∂_Z W_n = 0 of eq:aniso:zoom:finite:identities, and the whole equation rewritten in that form;
• integration by parts on the plane against a smooth compactly supported test function — the step which moves the derivatives of the equation onto ψ — together with the elementary bound for a pairing against a coefficient bounded on a set of finite measure;
• the space–time modulus of continuity on a rectangle, Arzelà–Ascoli on a compact set of a metric space, the extraction on a single rectangle, an abstract diagonal extraction, and their combination on {R > 0} × ℝ × (-∞, -1].

The uniform Lipschitz bound in space and the pairing bound itself enter as hypotheses: the first is supplied by the first-derivative bounds on Ω_n, the second by integrating the equation in τ and integrating by parts with the lemmas of the second group above.

The transport term in divergence form

theorem CIV.zoomOmega_transport_divergenceForm (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pres f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) (hr : p.1.1 ≠ 0) : zoomV lam h zc u p * dr (zoomOmega lam h zc u) p + zoomW lam h zc u p * dz (zoomOmega lam h zc u) p = dr (fun (q : (ℝ × ℝ) × ℝ) => zoomV lam h zc u q * zoomOmega lam h zc u q) p + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomW lam h zc u q * zoomOmega lam h zc u q) p + zoomV lam h zc u p / p.1.1 * zoomOmega lam h zc u p

The transport term of eq:aniso:zoom:finite:equation in divergence form: off the axis V_n ∂_R Ω_n + W_n ∂_Z Ω_n = ∂_R (V_n Ω_n) + ∂_Z (W_n Ω_n) + (V_n / R) Ω_n, the zeroth-order term being -Ω_n times the divergence ∂_R V_n + ∂_Z W_n = -V_n / R of eq:aniso:zoom:finite:identities. This is the form in which the derivatives are moved onto a test function in the passage to the limit.

theorem CIV.zoomOmega_pde_divergenceForm (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pres f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) (hr : p.1.1 ≠ 0) : dtPast (zoomOmega lam h zc u) p + dr (fun (q : (ℝ × ℝ) × ℝ) => zoomV lam h zc u q * zoomOmega lam h zc u q) p + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomW lam h zc u q * zoomOmega lam h zc u q) p + zoomV lam h zc u p / p.1.1 * zoomOmega lam h zc u p = dr (dr (zoomOmega lam h zc u)) p + 3 / p.1.1 * dr (zoomOmega lam h zc u) p + (lam ^ (2 * h)) ^ 2 * dz (dz (zoomOmega lam h zc u)) p + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomS lam h zc u q ^ 2 / q.1.1 ^ 2) p + lam ^ 5 * lam ^ (2 * h) * potentialVorticity f (zoomPoint lam h zc p)

The rescaled potential vorticity equation eq:aniso:zoom:finite:equation with its transport term in divergence form, off the axis. Every term on both sides is at most two derivatives of a quantity bounded on a rectangle of {R ≥ ε}, which is what the passage to the limit uses.

Integration by parts against a compactly supported test function

theorem CIV.integral_partial_fst_mul_add_eq_zero {U : Set (ℝ × ℝ)} (hU : IsOpen U) {F Gp : ℝ × ℝ → ℝ} (hFcont : ContinuousOn F U) (hGcont : ContinuousOn Gp U) (hFderiv : ∀ y ∈ U, HasDerivAt (fun (t : ℝ) => F (t, y.2)) (Gp y) y.1) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) : (∫ (y : ℝ × ℝ), Gp y * ψ y) + ∫ (y : ℝ × ℝ), F y * deriv (fun (t : ℝ) => ψ (t, y.2)) y.1 = 0

Integration by parts in the first variable of the plane: if Gp is the partial derivative of F in that variable on an open set U, both continuous on U, and ψ is smooth with compact support inside U, then ∫ (∂₁F) ψ = -∫ F (∂₁ψ). This is the step which moves a derivative off the coefficient and onto the test function.

theorem CIV.integral_partial_snd_mul_add_eq_zero {U : Set (ℝ × ℝ)} (hU : IsOpen U) {F Gp : ℝ × ℝ → ℝ} (hFcont : ContinuousOn F U) (hGcont : ContinuousOn Gp U) (hFderiv : ∀ y ∈ U, HasDerivAt (fun (s : ℝ) => F (y.1, s)) (Gp y) y.2) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) : (∫ (y : ℝ × ℝ), Gp y * ψ y) + ∫ (y : ℝ × ℝ), F y * deriv (fun (s : ℝ) => ψ (y.1, s)) y.2 = 0

Integration by parts in the second variable of the plane, the companion of CIV.integral_partial_fst_mul_add_eq_zero.

theorem CIV.integral_partial_fst_mul_eq_neg {U : Set (ℝ × ℝ)} (hU : IsOpen U) {F Gp : ℝ × ℝ → ℝ} (hFcont : ContinuousOn F U) (hGcont : ContinuousOn Gp U) (hFderiv : ∀ y ∈ U, HasDerivAt (fun (t : ℝ) => F (t, y.2)) (Gp y) y.1) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) : ∫ (y : ℝ × ℝ), Gp y * ψ y = -∫ (y : ℝ × ℝ), F y * deriv (fun (t : ℝ) => ψ (t, y.2)) y.1

Integration by parts in the first variable, in the form in which the pairing estimate uses it: the derivative moves from the coefficient onto the test function, at the cost of a sign.

theorem CIV.integral_partial_snd_mul_eq_neg {U : Set (ℝ × ℝ)} (hU : IsOpen U) {F Gp : ℝ × ℝ → ℝ} (hFcont : ContinuousOn F U) (hGcont : ContinuousOn Gp U) (hFderiv : ∀ y ∈ U, HasDerivAt (fun (s : ℝ) => F (y.1, s)) (Gp y) y.2) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) : ∫ (y : ℝ × ℝ), Gp y * ψ y = -∫ (y : ℝ × ℝ), F y * deriv (fun (s : ℝ) => ψ (y.1, s)) y.2

Integration by parts in the second variable, in the form in which the pairing estimate uses it.

theorem CIV.abs_integral_mul_le_of_tsupport_subset {S : Set (ℝ × ℝ)} (hSfin : MeasureTheory.volume S < ⊤) {a ψ : ℝ × ℝ → ℝ} {Ma B : ℝ} (hψS : tsupport ψ ⊆ S) (ha : ∀ y ∈ S, |a y| ≤ Ma) (hψ : ∀ (y : ℝ × ℝ), |ψ y| ≤ B) : |∫ (y : ℝ × ℝ), a y * ψ y| ≤ Ma * B * (MeasureTheory.volume S).toReal

The pairing of a function bounded on a set of finite measure with a test function supported in that set is bounded by the product of the two bounds and the measure: this is the estimate which collects the constant Cₒ of the pairing hypothesis from the bounds on the individual terms of the equation.

A uniform modulus of continuity

theorem CIV.continuousOn_of_modulus {X : Type u_1} [MetricSpace X] (S : Set X) (f : X → ℝ) (hmod : ∀ ε > 0, ∃ δ > 0, ∀ x ∈ S, ∀ y ∈ S, dist x y < δ → |f x - f y| ≤ ε) : ContinuousOn f S

A function with a uniform modulus of continuity on a set is continuous on it.

Arzelà–Ascoli on a compact set of a metric space

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

Arzelà–Ascoli: a sequence of real functions that is uniformly bounded on a compact set S of a metric space and shares one modulus of continuity on S has a subsequence converging uniformly on S to a function continuous on S.

The space–time modulus on a rectangle

theorem CIV.exists_modulus_of_lipschitz_of_pairings (K : Set (ℝ × ℝ)) (hK : IsCompact K) (J : Set ℝ) (Θ : ℕ → (ℝ × ℝ) × ℝ → ℝ) (L : ℝ) (hlip : ∀ (n : ℕ), ∀ τ ∈ J, LipschitzOnWith L.toNNReal (fun (y : ℝ × ℝ) => Θ n (y, τ)) K) (hpair : ∃ (Cₒ : ℝ), 0 ≤ Cₒ ∧ ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ (n : ℕ), ∀ τ ∈ J, ∀ τ' ∈ J, |∫ (y : ℝ × ℝ), (Θ n (y, τ) - Θ n (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|) (K' : Set (ℝ × ℝ)) (hK' : IsCompact K') (hKK' : K' ⊆ interior K) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (n : ℕ), ∀ p ∈ K' ×ˢ J, ∀ q ∈ K' ×ˢ J, dist p q < δ → |Θ n p - Θ n q| ≤ ε

The space–time modulus of continuity of the sequence on K' ×ˢ J, uniform in n: the spatial Lipschitz bound hlip controls a move in space, and the pairing bound hpair controls a move in time through CIV.equicontinuous_of_lipschitz_of_pairings.

Extraction on a single rectangle

theorem CIV.exists_subseq_tendstoUniformlyOn_prod (K : Set (ℝ × ℝ)) (hK : IsCompact K) (J : Set ℝ) (hJ : IsCompact J) (Θ : ℕ → (ℝ × ℝ) × ℝ → ℝ) (M L : ℝ) (hbdd : ∀ (n : ℕ), ∀ y ∈ K, ∀ τ ∈ J, |Θ n (y, τ)| ≤ M) (hlip : ∀ (n : ℕ), ∀ τ ∈ J, LipschitzOnWith L.toNNReal (fun (y : ℝ × ℝ) => Θ n (y, τ)) K) (hpair : ∃ (Cₒ : ℝ), 0 ≤ Cₒ ∧ ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ (n : ℕ), ∀ τ ∈ J, ∀ τ' ∈ J, |∫ (y : ℝ × ℝ), (Θ n (y, τ) - Θ n (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|) (K' : Set (ℝ × ℝ)) (hK' : IsCompact K') (hKK' : K' ⊆ interior K) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (Ω : (ℝ × ℝ) × ℝ → ℝ), ContinuousOn Ω (K' ×ˢ J) ∧ TendstoUniformlyOn (fun (n : ℕ) => Θ (φ n)) Ω Filter.atTop (K' ×ˢ J)

Step 2 on a single closed rectangle: from the uniform bound, the uniform spatial Lipschitz bound, and the pairing bound on K, a subsequence of Θ converges uniformly on K' ×ˢ J for every compact K' in the interior of K, and the limit is continuous there.

The diagonal extraction

theorem CIV.exists_subseq_tendstoUniformlyOn_forall {X : Type u_1} (S : ℕ → Set X) (f : ℕ → X → ℝ) (hstep : ∀ (j : ℕ) (g : ℕ → ℕ), StrictMono g → ∃ (g' : ℕ → ℕ), StrictMono g' ∧ ∃ (w : X → ℝ), TendstoUniformlyOn (fun (n : ℕ) => f (g (g' n))) w Filter.atTop (S j)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (w : X → ℝ), ∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => f (φ n)) w Filter.atTop (S j)

Diagonal extraction over a countable family of sets: if from every subsequence one can extract a further subsequence converging uniformly on S j, then a single subsequence converges uniformly on every S j, with one limit function.

Exhaustion of the region by closed rectangles

Enclosing a compact set in a rectangle

theorem CIV.exists_rectangle_of_isCompact {K : Set (ℝ × ℝ)} (hK : IsCompact K) (hKpos : ∀ y ∈ K, 0 < y.1) : ∃ (a : ℝ) (b : ℝ) (c : ℝ) (d : ℝ), 0 < a ∧ K ⊆ Set.Icc a b ×ˢ Set.Icc c d

A compact subset of the open half-plane {R > 0} lies in a closed rectangle whose radial side starts at a positive radius. This is the bridge between the hypotheses below, stated for compact sets, and the bounds on Ω_n, which are proved on rectangles [Ra, Rb] × [Za, Zb] contained in {R ≥ ε}.

theorem CIV.exists_Icc_neg_one_of_isCompact {J : Set ℝ} (hJ : IsCompact J) (hJle : ∀ τ ∈ J, τ ≤ -1) : ∃ (T : ℝ), J ⊆ Set.Icc (-T) (-1)

A compact set of rescaled times in (-∞, -1] lies in a closed interval [-T, -1].

The locally uniform limit on {R > 0} × ℝ × (-∞, -1]

theorem CIV.exists_subseq_tendstoUniformlyOn_of_lipschitz_of_pairings (Θ : ℕ → (ℝ × ℝ) × ℝ → ℝ) (hbdd : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (M : ℝ), ∀ (n : ℕ), ∀ y ∈ K, ∀ τ ∈ J, |Θ n (y, τ)| ≤ M) (hlip : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (L : ℝ), ∀ (n : ℕ), ∀ τ ∈ J, LipschitzOnWith L.toNNReal (fun (y : ℝ × ℝ) => Θ n (y, τ)) K) (hpair : ∀ (K : Set (ℝ × ℝ)), IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (Cₒ : ℝ), 0 ≤ Cₒ ∧ ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ (n : ℕ), ∀ τ ∈ J, ∀ τ' ∈ J, |∫ (y : ℝ × ℝ), (Θ n (y, τ) - Θ n (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (Ω : (ℝ × ℝ) × ℝ → ℝ), ContinuousOn Ω {q : (ℝ × ℝ) × ℝ | 0 < q.1.1 ∧ q.2 ≤ -1} ∧ ∀ (C : Set ((ℝ × ℝ) × ℝ)), IsCompact C → C ⊆ {q : (ℝ × ℝ) × ℝ | 0 < q.1.1 ∧ q.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => Θ (φ n)) Ω Filter.atTop C

Step 2 of the finite-axis zoom-in argument, eq:aniso:zoom:finite:compactness: a sequence which on every closed rectangle of the open half-plane and every compact time interval in (-∞, -1] is uniformly bounded, uniformly Lipschitz in space, and obeys the pairing bound in time, has a subsequence converging uniformly on every compact subset of {R > 0} × ℝ × (-∞, -1], to a limit continuous there.