Parabolic Hölder seminorms on time slabs

For a function v on a set of parabolic space-time, typically the closed time slab E × [a, b], the parabolic α-Hölder seminorm [v]_{α,par} is Mathlib's eHolderNorm α v, taken with respect to the parabolic distance dist x y + √|t - s|. This file identifies it with the supremum of the parabolic difference quotients and, on slabs, compares it with two separate seminorms:

• the spatial seminorm spaceEHolderNorm α v, the supremum over times t of the α-Hölder seminorms of the slices x ↦ v (x, t);
• the temporal seminorm timeEHolderNorm γ v, the supremum over positions x of the γ-Hölder seminorms of the slices t ↦ v (x, t), with respect to the ordinary time distance |t - s|.

A function is parabolically α-Hölder exactly when it is α-Hölder in space and α / 2-Hölder in time, uniformly, with max (spaceEHolderNorm α v) (timeEHolderNorm (α / 2) v) ≤ eHolderNorm α v and eHolderNorm α v ≤ spaceEHolderNorm α v + timeEHolderNorm (α / 2) v.

For a function u of the coordinates, twice differentiable in space and differentiable in time, the temporal (1 + α) / 2 seminorm of the spatial gradient D_x u on a slab is at most the sum of the parabolic α seminorms of the Hessian D_x² u and of the time derivative ∂ₜ u. Thus this seminorm, which enters the norm of C^{2+α, 1+α/2}, is controlled by the other top-order terms.

Bounded Lipschitz maps on ordinary space-time also give uniformly parabolic Hölder maps under translations of space and time.

Finally, a bounded α-Hölder field on space is a time-independent bounded parabolically α-Hölder field on any slab, since the spatial position is 1-Lipschitz for the parabolic distance.

Main declarations

• TauCeti.ParabolicSpaceTime.exists_holderWith_comp_coords: the bounded Lipschitz bridge from ordinary space-time to parabolic Hölder maps, uniformly under translation.
• TauCeti.ParabolicSpaceTime.eHolderNorm_eq_iSup_dist_add_sqrt: the parabolic seminorm is the supremum of dist (v p) (v q) / (dist x y + √|t - s|) ^ α.
• TauCeti.ParabolicSpaceTime.spaceEHolderNorm, TauCeti.ParabolicSpaceTime.timeEHolderNorm: the separate spatial and temporal seminorms.
• TauCeti.ParabolicSpaceTime.holderWith_of_holderOnWith_slab: the time slices of a parabolically Hölder function on a slab are Hölder in space with the same constant.
• TauCeti.ParabolicSpaceTime.eHolderNorm_le_timeEHolderNorm, TauCeti.ParabolicSpaceTime.memHolder_timeSlice_of_timeEHolderNorm_lt_top: each time slice is controlled by the temporal seminorm.
• TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_of_lipschitzWith: reparametrizing time by a 1-Lipschitz map, such as a restriction or a time reversal, does not increase the temporal seminorm.
• TauCeti.ParabolicSpaceTime.spaceEHolderNorm_le_eHolderNorm, TauCeti.ParabolicSpaceTime.timeEHolderNorm_div_two_le_eHolderNorm, TauCeti.ParabolicSpaceTime.eHolderNorm_le_spaceEHolderNorm_add_timeEHolderNorm: the comparison of the parabolic seminorm with the separate ones.
• TauCeti.ParabolicSpaceTime.memHolder_slab_iff: the corresponding characterisation of parabolic Hölder functions.
• TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_timeEHolderNorm_add_spaceEHolderNorm, TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_eHolderNorm_add_eHolderNorm: control of the temporal seminorm of the spatial gradient.
• TauCeti.HolderSpace.compSlabSpaceL: a Hölder field on space as a time-independent parabolic Hölder field on a slab.

References

• N. V. Krylov, Lectures on elliptic and parabolic equations in Hölder spaces, AMS, 1996.
• A. Lunardi, Linear and nonlinear diffusion problems, lecture notes, Cortona, 2004.

theorem TauCeti.ParabolicSpaceTime.exists_holderWith_comp_coords {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {α : NNReal} (hα : α ≤ 1) {f : E × ℝ → F} {K : NNReal} (hf : LipschitzWith K f) {M : ℝ} (hbound : ∀ (x : E × ℝ), ‖f x‖ ≤ M) : ∃ (C : NNReal), ∀ (z : E × ℝ), HolderWith C α fun (p : ParabolicSpaceTime E) => f (p.space - z.1, p.time - z.2)

Bounded Lipschitz maps on ordinary space-time are uniformly Hölder for the parabolic distance, even when time ranges over the whole real line.

theorem TauCeti.ParabolicSpaceTime.eHolderNorm_eq_iSup_dist_add_sqrt {E : Type u_1} {F : Type u_2} [MetricSpace E] [PseudoMetricSpace F] (α : NNReal) {S : Set (ParabolicSpaceTime E)} (v : ↑S → F) : eHolderNorm α v = ⨆ (p : ↑S), ⨆ (q : ↑S), ⨆ (_ : p ≠ q), ENNReal.ofReal (dist (v p) (v q) / (dist (↑p).space (↑q).space + √|(↑p).time - (↑q).time|) ^ ↑α)

The parabolic Hölder seminorm of a function on a set of parabolic space-time is the supremum of the parabolic difference quotients dist (v p) (v q) / (dist x y + √|t - s|) ^ α over distinct points p = (x, t) and q = (y, s).

noncomputable def TauCeti.ParabolicSpaceTime.spaceEHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [PseudoEMetricSpace E] (α : NNReal) (v : ↑(slab a b) → F) : ENNReal

The spatial α-Hölder seminorm of a function on the slab E × [a, b]: the supremum over times t ∈ [a, b] of the α-Hölder seminorms of the slices x ↦ v (x, t).

noncomputable def TauCeti.ParabolicSpaceTime.timeEHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] (γ : NNReal) (v : ↑(slab a b) → F) : ENNReal

The temporal γ-Hölder seminorm of a function on the slab E × [a, b]: the supremum over positions x of the γ-Hölder seminorms of the slices t ↦ v (x, t), with respect to the ordinary distance |t - s| on [a, b].

theorem TauCeti.ParabolicSpaceTime.spaceEHolderNorm_le_iff {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [MetricSpace E] {α : NNReal} {v : ↑(slab a b) → F} {C : ENNReal} : spaceEHolderNorm α v ≤ C ↔ ∀ (t : ↑(Set.Icc a b)) (x y : E), edist (v (slabMk x t)) (v (slabMk y t)) ≤ C * edist x y ^ ↑α

The spatial seminorm is bounded by C exactly when every time slice satisfies the α-Hölder inequality with constant C.

theorem TauCeti.ParabolicSpaceTime.holderWith_of_holderOnWith_slab {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [PseudoEMetricSpace E] {f : ℝ → E → F} {H α : NNReal} {s : ℝ} (hpar : HolderOnWith H α (fun (p : ParabolicSpaceTime E) => f p.time p.space) (slab a b)) (hs : s ∈ Set.Icc a b) : HolderWith H α (f s)

A function of the coordinates that is parabolically α-Hölder on the slab E × [a, b] is α-Hölder in space, with the same constant, on every time slice of the slab.

theorem TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_iff {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] {γ : NNReal} {v : ↑(slab a b) → F} {C : ENNReal} : timeEHolderNorm γ v ≤ C ↔ ∀ (x : E) (t s : ↑(Set.Icc a b)), edist (v (slabMk x t)) (v (slabMk x s)) ≤ C * edist t s ^ ↑γ

The temporal seminorm is bounded by C exactly when every spatial position satisfies the γ-Hölder inequality in time with constant C.

theorem TauCeti.ParabolicSpaceTime.eHolderNorm_le_timeEHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] (γ : NNReal) (v : ↑(slab a b) → F) (x : E) : (eHolderNorm γ fun (t : ↑(Set.Icc a b)) => v (slabMk x t)) ≤ timeEHolderNorm γ v

The Hölder seminorm of each time slice is bounded by the temporal seminorm.

theorem TauCeti.ParabolicSpaceTime.memHolder_timeSlice_of_timeEHolderNorm_lt_top {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] {γ : NNReal} {v : ↑(slab a b) → F} (h : timeEHolderNorm γ v < ⊤) (x : E) : MemHolder γ fun (t : ↑(Set.Icc a b)) => v (slabMk x t)

If the temporal γ-seminorm is finite, then every time slice is γ-Hölder.

theorem TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_of_lipschitzWith {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] {a' b' : ℝ} {γ : NNReal} {v : ↑(slab a b) → F} {w : ↑(slab a' b') → F} {φ : ↑(Set.Icc a' b') → ↑(Set.Icc a b)} (hφ : LipschitzWith 1 φ) (hw : ∀ (x : E) (t : ↑(Set.Icc a' b')), w (slabMk x t) = v (slabMk x (φ t))) : timeEHolderNorm γ w ≤ timeEHolderNorm γ v

Reparametrizing time by a 1-Lipschitz map does not increase the temporal seminorm: if w (x, t) = v (x, φ t) on the slab E × [a', b'] for a 1-Lipschitz φ : [a', b'] → [a, b], such as the inclusion of a subinterval or the reversal t ↦ T - t, then [w]_{t,γ} ≤ [v]_{t,γ}.

theorem TauCeti.ParabolicSpaceTime.spaceEHolderNorm_le_eHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [MetricSpace E] (α : NNReal) (v : ↑(slab a b) → F) : spaceEHolderNorm α v ≤ eHolderNorm α v

The spatial seminorm is bounded by the parabolic seminorm: at a common time, the parabolic distance is the spatial distance.

theorem TauCeti.ParabolicSpaceTime.timeEHolderNorm_div_two_le_eHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [MetricSpace E] (α : NNReal) (v : ↑(slab a b) → F) : timeEHolderNorm (α / 2) v ≤ eHolderNorm α v

The temporal α / 2-seminorm is bounded by the parabolic α-seminorm: at a common position, the parabolic distance is the square root of the time distance.

theorem TauCeti.ParabolicSpaceTime.eHolderNorm_le_spaceEHolderNorm_add_timeEHolderNorm {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [MetricSpace E] (α : NNReal) (v : ↑(slab a b) → F) : eHolderNorm α v ≤ spaceEHolderNorm α v + timeEHolderNorm (α / 2) v

The parabolic α-seminorm is bounded by the sum of the spatial α-seminorm and the temporal α / 2-seminorm.

theorem TauCeti.ParabolicSpaceTime.memHolder_slab_iff {E : Type u_1} {F : Type u_2} {a b : ℝ} [PseudoEMetricSpace F] [MetricSpace E] {α : NNReal} {v : ↑(slab a b) → F} : MemHolder α v ↔ spaceEHolderNorm α v < ⊤ ∧ timeEHolderNorm (α / 2) v < ⊤

A function on a slab is parabolically α-Hölder exactly when it is α-Hölder in space and α / 2-Hölder in time, uniformly in the other variable.

The temporal seminorm of the spatial gradient

theorem TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_timeEHolderNorm_add_spaceEHolderNorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u : E → ℝ → F} {u' : E → ℝ → E →L[ℝ] F} {u'' : E → ℝ → E →L[ℝ] E →L[ℝ] F} {uₜ : E → ℝ → F} (α : NNReal) (hu' : ∀ t ∈ Set.Icc a b, ∀ (y : E), HasFDerivAt (fun (x : E) => u x t) (u' y t) y) (hu'' : ∀ t ∈ Set.Icc a b, ∀ (y : E), HasFDerivAt (fun (x : E) => u' x t) (u'' y t) y) (huₜ : ∀ (y : E), ∀ t ∈ Set.Icc a b, HasDerivWithinAt (u y) (uₜ y t) (Set.Icc a b) t) : (timeEHolderNorm ((1 + α) / 2) fun (p : ↑(slab a b)) => u' (↑p).space ↑(slabTime p)) ≤ (timeEHolderNorm (α / 2) fun (p : ↑(slab a b)) => u'' (↑p).space ↑(slabTime p)) + spaceEHolderNorm α fun (p : ↑(slab a b)) => uₜ (↑p).space ↑(slabTime p)

The temporal seminorm of the spatial gradient is controlled. Let u (x, t) be twice differentiable in x ∈ E and differentiable in t within [a, b], with spatial derivatives u', u'' and time derivative uₜ. On the slab E × [a, b], the temporal (1 + α) / 2 seminorm of the gradient u' is at most the sum of the temporal α / 2 seminorm of the Hessian u'' and the spatial α seminorm of uₜ.

theorem TauCeti.ParabolicSpaceTime.timeEHolderNorm_le_eHolderNorm_add_eHolderNorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u : E → ℝ → F} {u' : E → ℝ → E →L[ℝ] F} {u'' : E → ℝ → E →L[ℝ] E →L[ℝ] F} {uₜ : E → ℝ → F} (α : NNReal) (hu' : ∀ t ∈ Set.Icc a b, ∀ (y : E), HasFDerivAt (fun (x : E) => u x t) (u' y t) y) (hu'' : ∀ t ∈ Set.Icc a b, ∀ (y : E), HasFDerivAt (fun (x : E) => u' x t) (u'' y t) y) (huₜ : ∀ (y : E), ∀ t ∈ Set.Icc a b, HasDerivWithinAt (u y) (uₜ y t) (Set.Icc a b) t) : (timeEHolderNorm ((1 + α) / 2) fun (p : ↑(slab a b)) => u' (↑p).space ↑(slabTime p)) ≤ (eHolderNorm α fun (p : ↑(slab a b)) => u'' (↑p).space ↑(slabTime p)) + eHolderNorm α fun (p : ↑(slab a b)) => uₜ (↑p).space ↑(slabTime p)

The temporal seminorm of the spatial gradient is controlled by parabolic seminorms. On the slab E × [a, b], the temporal (1 + α) / 2 seminorm of the spatial gradient of u is at most the sum of the parabolic α seminorms of its Hessian and of its time derivative. In particular it is finite whenever these are.

Time-independent Hölder fields on a slab

noncomputable def TauCeti.HolderSpace.compSlabSpaceL {α : NNReal} {E : Type u_1} {Y : Type u_2} [MetricSpace E] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {a b : ℝ} : HolderSpace α E Y →L[ℝ] HolderSpace α (↑(ParabolicSpaceTime.slab a b)) Y

A bounded α-Hölder field on space, viewed as a time-independent bounded parabolically α-Hölder field on the slab E × [a, b]: precomposition with the spatial position, which is 1-Lipschitz for the parabolic distance.

@[simp]

theorem TauCeti.HolderSpace.compSlabSpaceL_apply {α : NNReal} {E : Type u_1} {Y : Type u_2} [MetricSpace E] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {a b : ℝ} (f : HolderSpace α E Y) (p : ↑(ParabolicSpaceTime.slab a b)) : ↑(compSlabSpaceL f).toHolderSubmodule p = ↑f.toHolderSubmodule (↑p).space