Lipschitz Bound Of Pointwise Limit #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.lipschitzWith_of_tendsto
{α : Type u_1}
[PseudoMetricSpace α]
{F : Type u_2}
[NormedAddCommGroup F]
{f : ℕ → α → F}
{g : α → F}
{K : NNReal}
(hf : ∀ (n : ℕ), LipschitzWith K (f n))
(hg : ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
:
LipschitzWith K g
A pointwise limit of uniformly K-Lipschitz functions is K-Lipschitz.
theorem
CIV.norm_le_of_tendsto
{α : Type u_1}
{F : Type u_2}
[NormedAddCommGroup F]
{f : ℕ → α → F}
{g : α → F}
{M : ℝ}
(hf : ∀ (n : ℕ) (x : α), ‖f n x‖ ≤ M)
(hg : ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
(x : α)
:
A pointwise limit of functions uniformly bounded by M is bounded by M.
theorem
CIV.lipschitzWith_and_norm_le_of_tendsto
{α : Type u_1}
[PseudoMetricSpace α]
{F : Type u_2}
[NormedAddCommGroup F]
{f : ℕ → α → F}
{g : α → F}
{K : NNReal}
{M : ℝ}
(hLip : ∀ (n : ℕ), LipschitzWith K (f n))
(hBd : ∀ (n : ℕ) (x : α), ‖f n x‖ ≤ M)
(hg : ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
:
A pointwise limit of uniformly Lipschitz, uniformly bounded functions preserves both bounds with the same constants.
theorem
CIV.ae_lipschitzWith_and_norm_le_of_tendsto
{m : ℕ}
{Bn : ℕ → CKN.Vec m × ℝ → CKN.Vec m}
{B : CKN.Vec m × ℝ → CKN.Vec m}
{Λ : NNReal}
{J : Set ℝ}
(hLip : ∀ (n : ℕ) (τ : ℝ), LipschitzWith Λ fun (x : CKN.Vec m) => Bn n (x, τ))
(hBd : ∀ (n : ℕ) (τ : ℝ) (x : CKN.Vec m), ‖Bn n (x, τ)‖ ≤ ↑Λ)
(hconv :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (x : CKN.Vec m), Filter.Tendsto (fun (n : ℕ) => Bn n (x, τ)) Filter.atTop (nhds (B (x, τ))))
:
A.e.-in-time limit of uniformly Lipschitz, uniformly bounded approximating sequences inherits the same Lipschitz and boundedness constants.
theorem
CIV.ae_norm_le_of_tendsto
{m : ℕ}
{qn : ℕ → CKN.Vec m × ℝ → ℝ}
{q : CKN.Vec m × ℝ → ℝ}
{M : ℝ}
{J : Set ℝ}
(hBd : ∀ (n : ℕ) (z : CKN.Vec m × ℝ), |qn n z| ≤ M)
(hconv :
∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ J), Filter.Tendsto (fun (n : ℕ) => qn n z) Filter.atTop (nhds (q z)))
:
A.e.-in-space-time limit of uniformly bounded scalar fields is bounded by the same constant.