Equicontinuity in time from spatial mollification

This file proves the abstract analytic step behind route D5 for prop:aniso:small: a way to obtain equicontinuity in time of a rescaled potential-vorticity sequence without controlling a negative-order Sobolev norm of its time derivative.

The setting is a sequence Θ n : (ℝ × ℝ) × ℝ → ℝ of functions of a spatial variable in ℝ × ℝ and a time variable in ℝ, uniformly Lipschitz in space on a compact set K (hypothesis hlip), together with a pairing hypothesis hpair: for every smooth, compactly supported test function ψ with support in interior K and every sup-norm budget B for ψ and its first two derivatives, the time difference of Θ n paired against ψ is controlled by Cₒ * B * |τ − τ'| for one constant Cₒ, independent of ψ, B, n, τ, and τ'. This is exactly the estimate integration by parts produces when ∂_τ Θ n is a finite sum of spatial derivatives, of order at most two, of quantities bounded on K uniformly in n: the constant Cₒ collects the number of terms, their bounds, and the measure of K, so it is genuinely independent of the test function used, which is essential because the argument below applies hpair to a whole family of translated test functions sharing one budget B.

The main theorem equicontinuous_of_lipschitz_of_pairings derives equicontinuity in time, locally uniform in space on compact subsets K' of interior K: mollifying Θ n (·, τ) against a bump ψ_η of radius η centered at a point y ∈ K' gives Θ n (y, τ) − Θ n (y, τ') = (Θ n (y, τ) − (Θ n (·, τ) ∗ ψ_η) y) + ((Θ n (·, τ) − Θ n (·, τ')) ∗ ψ_η) y + ((Θ n (·, τ') ∗ ψ_η) y − Θ n (y, τ')). The two outer terms are bounded by the spatial Lipschitz constant times η (abs_sub_integral_mul_le), independently of the pairing hypothesis, while the middle term is exactly what hpair bounds, applied to the translate of the fixed profile ψ_η (exists_bump_with_uniform_bound, bound_of_translate). Choosing η small so the outer terms are below ε / 2, then δ small so the middle term is below ε / 2 whenever |τ − τ'| < δ, gives the equicontinuity modulus, uniform in n and in y ∈ K'.

theorem CIV.exists_bound_of_hasCompactSupport {F : Type u_1} [NormedAddCommGroup F] {g : ℝ × ℝ → F} (hc : Continuous g) (hs : HasCompactSupport g) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : ℝ × ℝ), ‖g x‖ ≤ M

A continuous function on ℝ × ℝ with compact support is bounded, with an explicit nonnegative bound valid at every point.

theorem CIV.fderiv_sub_const_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : ℝ × ℝ → F} (hg : Differentiable ℝ g) (p x : ℝ × ℝ) : fderiv ℝ (fun (x : ℝ × ℝ) => g (x - p)) x = fderiv ℝ g (x - p)

The derivative of a spatial translate is the translated derivative: differentiating x ↦ g (x - p) at x gives the same continuous linear map as differentiating g itself at x - p. Used twice below, once for the bump profile and once for its own derivative, to show that a family of translated bump functions shares a common derivative bound.

theorem CIV.hasCompactSupport_of_ball_subset {K : Set (ℝ × ℝ)} (hK : IsCompact K) {p : ℝ × ℝ} {η : ℝ} {φ : ℝ × ℝ → ℝ} (hφsupp : Function.support φ ⊆ Metric.ball p η) (hballK : Metric.closedBall p η ⊆ K) : HasCompactSupport φ

A bump function continuous on ℝ × ℝ with support in a ball whose closure lies in a compact set K has compact support.

theorem CIV.integrable_mul_of_ball_subset {K : Set (ℝ × ℝ)} (hK : IsCompact K) {f : ℝ × ℝ → ℝ} (hfCont : ContinuousOn f K) {p : ℝ × ℝ} {η : ℝ} {φ : ℝ × ℝ → ℝ} (hφcont : Continuous φ) (hφsupp : Function.support φ ⊆ Metric.ball p η) (hballK : Metric.closedBall p η ⊆ K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => f y * φ y) MeasureTheory.volume

A function continuous on a compact set K, multiplied by a continuous bump supported in a ball whose closure lies in K, is (globally) integrable: the product vanishes outside K, where it agrees with a function continuous on the compact set K.

theorem CIV.abs_sub_integral_mul_le {K : Set (ℝ × ℝ)} (hK : IsCompact K) {f : ℝ × ℝ → ℝ} {L : ℝ} (hL : 0 ≤ L) {p : ℝ × ℝ} (hp : p ∈ K) (hlip : LipschitzOnWith L.toNNReal f K) {η : ℝ} {φ : ℝ × ℝ → ℝ} (hφnn : ∀ (x : ℝ × ℝ), 0 ≤ φ x) (hφcont : Continuous φ) (hφsupp : Function.support φ ⊆ Metric.ball p η) (hφint : ∫ (x : ℝ × ℝ), φ x = 1) (hballK : Metric.closedBall p η ⊆ K) : |f p - ∫ (y : ℝ × ℝ), f y * φ y| ≤ L * η

Mollifying a function that is Lipschitz on a compact set K against a nonnegative, mass-one bump φ supported in the ball of radius η around a point p, with that ball contained in K, changes the value at p by at most the Lipschitz constant times η.

theorem CIV.exists_bump_with_uniform_bound (η : ℝ) (hη : 0 < η) : ∃ (κ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) κ ∧ (∀ (x : ℝ × ℝ), 0 ≤ κ x) ∧ ∫ (x : ℝ × ℝ), κ x = 1 ∧ Function.support κ ⊆ Metric.ball 0 η ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : ℝ × ℝ), |κ x| ≤ B ∧ ‖fderiv ℝ κ x‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ κ) x‖ ≤ B

For every radius η > 0 there is a smooth, nonnegative, mass-one bump κ on ℝ × ℝ, supported in the open ball of radius η around the origin, together with a single nonnegative real number bounding κ itself, its derivative, and its second derivative at every point.

theorem CIV.bound_of_translate {κ : ℝ × ℝ → ℝ} (hκSmooth : ContDiff ℝ (↑⊤) κ) {B : ℝ} (hB : ∀ (x : ℝ × ℝ), |κ x| ≤ B ∧ ‖fderiv ℝ κ x‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ κ) x‖ ≤ B) (p x : ℝ × ℝ) : |κ (x - p)| ≤ B ∧ ‖fderiv ℝ (fun (x : ℝ × ℝ) => κ (x - p)) x‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ fun (x : ℝ × ℝ) => κ (x - p)) x‖ ≤ B

Translating a bounded bump profile κ to be centered at p preserves the pointwise bound B on κ and on its first two derivatives: the derivative of a translate is the translate of the derivative, which has the same norm.

theorem CIV.equicontinuous_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 (ℝ × ℝ)) : IsCompact K' → K' ⊆ interior K → ∀ ε > 0, ∃ δ > 0, ∀ (n : ℕ), ∀ y ∈ K', ∀ τ ∈ J, ∀ τ' ∈ J, |τ - τ'| < δ → |Θ n (y, τ) - Θ n (y, τ')| ≤ ε

Equicontinuity in time, on interior compacts, of a sequence uniformly bounded and uniformly Lipschitz in space, whose time-difference pairings against admissible test functions obey a uniform Lipschitz bound in time with a constant depending only on a sup-norm budget for the test function and its first two derivatives. This is the abstract route around negative Sobolev norms recorded for prop:aniso:small: a spatial mollification at scale η controls the outer error by the spatial Lipschitz constant times η, while the pairing hypothesis controls the mollified difference in time, uniformly over the family of translated test functions used at every point of the target compact.