Parabolic space-time

The heat operator ∂ₜ - Δ scales one time derivative like two spatial derivatives, so the natural distance on space-time E × ℝ is the parabolic distance d((x, t), (y, s)) = dist x y + √|t - s|. Hölder spaces for parabolic equations are defined with respect to this distance.

This file builds the parabolic distance from existing Mathlib constructions rather than putting a second metric on E × ℝ. Time carries Mathlib's half-power snowflake metric Metric.Snowflaking ℝ (1 / 2), whose distance is |t - s| ^ (1 / 2), and space-time is the WithLp 1 product of E with this snowflake, whose distance is the sum of the two factor distances. The topology is the ordinary product topology on E × ℝ.

Main declarations

• TauCeti.ParabolicTime: the real line with the distance √|t - s|.
• TauCeti.ParabolicSpaceTime E: space-time E × ℝ with the parabolic distance.
• TauCeti.ParabolicSpaceTime.ofCoords, space, time: the coordinates of a point.
• TauCeti.ParabolicSpaceTime.dist_eq: the parabolic distance formula.
• TauCeti.ParabolicSpaceTime.coordsHomeomorph: the homeomorphism with ordinary E × ℝ.
• TauCeti.ParabolicSpaceTime.timeReverse: reversal of time about T, an isometry.
• TauCeti.ParabolicSpaceTime.slab: the closed time slab E × [a, b].
• TauCeti.ParabolicSpaceTime.spatialSlice, TauCeti.ParabolicSpaceTime.timeSlice: the continuous inclusions of a fixed-time spatial slice and of a fixed-position time slice.
• TauCeti.ParabolicSpaceTime.slabTimeReverse: reversal of time about T, an isometry from the slab E × [T - b, T - a] onto E × [a, b].
• TauCeti.ParabolicSpaceTime.slabSpaceMap: a spatial map f acting on a slab by (x, t) ↦ (f x, t), Lipschitz for the parabolic distance when f is.
• TauCeti.ParabolicSpaceTime.lipschitzWith_slabSpace: the spatial position of a point of a slab is 1-Lipschitz for the parabolic distance.

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.

@[reducible, inline]

abbrev TauCeti.ParabolicTime : Type

Real time with the parabolic half-power metric dist t s = |t - s| ^ (1 / 2).

@[reducible, inline]

abbrev TauCeti.ParabolicSpaceTime (E : Type u_1) : Type u_1

Space-time E × ℝ with the parabolic distance dist x y + √|t - s|: the L¹ product of E with the half-power snowflake of real time.

noncomputable def TauCeti.ParabolicSpaceTime.ofCoords {E : Type u_1} (x : E) (t : ℝ) : ParabolicSpaceTime E

The point of parabolic space-time with spatial position x and time t.

def TauCeti.ParabolicSpaceTime.space {E : Type u_1} (p : ParabolicSpaceTime E) : E

The spatial coordinate of a point of parabolic space-time.

noncomputable def TauCeti.ParabolicSpaceTime.time {E : Type u_1} (p : ParabolicSpaceTime E) : ℝ

The real time coordinate of a point of parabolic space-time.

@[simp]

theorem TauCeti.ParabolicSpaceTime.space_ofCoords {E : Type u_1} (x : E) (t : ℝ) : (ofCoords x t).space = x

@[simp]

theorem TauCeti.ParabolicSpaceTime.time_ofCoords {E : Type u_1} (x : E) (t : ℝ) : (ofCoords x t).time = t

@[simp]

theorem TauCeti.ParabolicSpaceTime.ofCoords_space_time {E : Type u_1} (p : ParabolicSpaceTime E) : ofCoords p.space p.time = p

theorem TauCeti.ParabolicSpaceTime.ext {E : Type u_1} {p q : ParabolicSpaceTime E} (hspace : p.space = q.space) (htime : p.time = q.time) : p = q

Points of parabolic space-time with the same coordinates are equal.

theorem TauCeti.ParabolicSpaceTime.ext_iff {E : Type u_1} {p q : ParabolicSpaceTime E} : p = q ↔ p.space = q.space ∧ p.time = q.time

Closed time slabs

noncomputable def TauCeti.ParabolicSpaceTime.slab {E : Type u_1} (a b : ℝ) : Set (ParabolicSpaceTime E)

The closed time slab E × [a, b] in parabolic space-time.

@[simp]

theorem TauCeti.ParabolicSpaceTime.mem_slab {E : Type u_1} {a b : ℝ} {p : ParabolicSpaceTime E} : p ∈ slab a b ↔ p.time ∈ Set.Icc a b

noncomputable def TauCeti.ParabolicSpaceTime.slabMk {E : Type u_1} {a b : ℝ} (x : E) (t : ↑(Set.Icc a b)) : ↑(slab a b)

The point of the slab E × [a, b] with spatial position x and time t ∈ [a, b].

@[simp]

theorem TauCeti.ParabolicSpaceTime.space_slabMk {E : Type u_1} {a b : ℝ} (x : E) (t : ↑(Set.Icc a b)) : (↑(slabMk x t)).space = x

@[simp]

theorem TauCeti.ParabolicSpaceTime.time_slabMk {E : Type u_1} {a b : ℝ} (x : E) (t : ↑(Set.Icc a b)) : (↑(slabMk x t)).time = ↑t

noncomputable def TauCeti.ParabolicSpaceTime.slabTime {E : Type u_1} {a b : ℝ} (p : ↑(slab a b)) : ↑(Set.Icc a b)

The time coordinate of a point of the slab E × [a, b], as an element of [a, b].

@[simp]

theorem TauCeti.ParabolicSpaceTime.coe_slabTime {E : Type u_1} {a b : ℝ} (p : ↑(slab a b)) : ↑(slabTime p) = (↑p).time

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabTime_slabMk {E : Type u_1} {a b : ℝ} (x : E) (t : ↑(Set.Icc a b)) : slabTime (slabMk x t) = t

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabMk_space_slabTime {E : Type u_1} {a b : ℝ} (p : ↑(slab a b)) : slabMk (↑p).space (slabTime p) = p

Every point of a slab is given by its coordinates.

theorem TauCeti.ParabolicSpaceTime.slab_subset_slab {E : Type u_1} {a b a' b' : ℝ} (ha : a ≤ a') (hb : b' ≤ b) : slab a' b' ⊆ slab a b

A slab over a smaller time interval is contained in the larger slab.

@[simp]

theorem TauCeti.ParabolicSpaceTime.inclusion_slabMk {E : Type u_1} {a b a' b' : ℝ} (h : slab a' b' ⊆ slab a b) (x : E) (t : ↑(Set.Icc a' b')) : Set.inclusion h (slabMk x t) = slabMk x ⟨↑t, ⋯⟩

Including a smaller slab into a larger one keeps the coordinates of a point.

noncomputable def TauCeti.ParabolicSpaceTime.slabSpaceMap {E : Type u_1} {E' : Type u_2} {a b : ℝ} (f : E → E') (p : ↑(slab a b)) : ↑(slab a b)

A spatial map f acting on the slab E × [a, b], by (x, t) ↦ (f x, t).

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabSpaceMap_slabMk {E : Type u_1} {E' : Type u_2} {a b : ℝ} (f : E → E') (x : E) (t : ↑(Set.Icc a b)) : slabSpaceMap f (slabMk x t) = slabMk (f x) t

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabSpaceMap_id {E : Type u_1} {a b : ℝ} : slabSpaceMap id = id

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabSpaceMap_slabSpaceMap {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} {a b : ℝ} (f : E' → E'') (g : E → E') (p : ↑(slab a b)) : slabSpaceMap f (slabSpaceMap g p) = slabSpaceMap (f ∘ g) p

theorem TauCeti.ParabolicSpaceTime.edist_ofCoords {E : Type u_1} [PseudoEMetricSpace E] (x y : E) (t s : ℝ) : edist (ofCoords x t) (ofCoords y s) = edist x y + edist t s ^ (1 / 2)

The extended parabolic distance in coordinates: edist x y + edist t s ^ (1 / 2).

theorem TauCeti.ParabolicSpaceTime.edist_eq {E : Type u_1} [PseudoEMetricSpace E] (p q : ParabolicSpaceTime E) : edist p q = edist p.space q.space + edist p.time q.time ^ (1 / 2)

The extended parabolic distance is the spatial distance plus the square root of the time distance.

theorem TauCeti.ParabolicSpaceTime.edist_slabMk {E : Type u_1} [PseudoEMetricSpace E] {a b : ℝ} (x y : E) (t s : ↑(Set.Icc a b)) : edist (slabMk x t) (slabMk y s) = edist x y + edist t s ^ (1 / 2)

The extended parabolic distance between two points of a slab, in coordinates.

theorem TauCeti.ParabolicSpaceTime.edist_slabMk_same_space_rpow {E : Type u_1} [PseudoEMetricSpace E] {a b : ℝ} (x : E) (t s : ↑(Set.Icc a b)) (α : NNReal) : edist (slabMk x t) (slabMk x s) ^ ↑α = edist t s ^ ↑(α / 2)

At a common position, the α-th power of the parabolic distance between two points of a slab is the α / 2-th power of the time distance.

theorem TauCeti.ParabolicSpaceTime.edist_space_le {E : Type u_1} [PseudoEMetricSpace E] (p q : ParabolicSpaceTime E) : edist p.space q.space ≤ edist p q

theorem TauCeti.ParabolicSpaceTime.edist_time_rpow_le {E : Type u_1} [PseudoEMetricSpace E] (p q : ParabolicSpaceTime E) : edist p.time q.time ^ (1 / 2) ≤ edist p q

theorem TauCeti.ParabolicSpaceTime.lipschitzWith_slabSpace {E : Type u_1} [PseudoEMetricSpace E] {a b : ℝ} : LipschitzWith 1 fun (p : ↑(slab a b)) => (↑p).space

The spatial position of a point of a slab is 1-Lipschitz for the parabolic distance.

theorem TauCeti.ParabolicSpaceTime.lipschitzWith_slabSpaceMap {E : Type u_1} [PseudoEMetricSpace E] {E' : Type u_2} [PseudoEMetricSpace E'] {a b : ℝ} {K : NNReal} {f : E → E'} (hf : LipschitzWith K f) : LipschitzWith (max K 1) (slabSpaceMap f)

A K-Lipschitz spatial map acts on a slab as a max K 1-Lipschitz map for the parabolic distance.

theorem TauCeti.ParabolicSpaceTime.dist_ofCoords {E : Type u_1} [PseudoMetricSpace E] (x y : E) (t s : ℝ) : dist (ofCoords x t) (ofCoords y s) = dist x y + √|t - s|

The parabolic distance formula d((x, t), (y, s)) = dist x y + √|t - s|.

theorem TauCeti.ParabolicSpaceTime.dist_eq {E : Type u_1} [PseudoMetricSpace E] (p q : ParabolicSpaceTime E) : dist p q = dist p.space q.space + √|p.time - q.time|

The parabolic distance is the spatial distance plus the square root of the time distance.

theorem TauCeti.ParabolicSpaceTime.dist_space_le {E : Type u_1} [PseudoMetricSpace E] (p q : ParabolicSpaceTime E) : dist p.space q.space ≤ dist p q

theorem TauCeti.ParabolicSpaceTime.sqrt_abs_time_sub_le_dist {E : Type u_1} [PseudoMetricSpace E] (p q : ParabolicSpaceTime E) : √|p.time - q.time| ≤ dist p q

theorem TauCeti.ParabolicSpaceTime.abs_time_sub_le_dist_of_dist_le_one {E : Type u_1} [PseudoMetricSpace E] (p q : ParabolicSpaceTime E) (h : dist p q ≤ 1) : |p.time - q.time| ≤ dist p q

At parabolic distance at most one, the time-coordinate difference is bounded by the parabolic distance.

@[simp]

theorem TauCeti.ParabolicSpaceTime.dist_ofCoords_ofCoords_same_time {E : Type u_1} [PseudoMetricSpace E] (x y : E) (t : ℝ) : dist (ofCoords x t) (ofCoords y t) = dist x y

At a common time, the parabolic distance is the spatial distance.

@[simp]

theorem TauCeti.ParabolicSpaceTime.dist_ofCoords_ofCoords_same_space {E : Type u_1} [PseudoMetricSpace E] (x : E) (t s : ℝ) : dist (ofCoords x t) (ofCoords x s) = √|t - s|

At a common spatial position, the parabolic distance is the square root of the time distance.

noncomputable def TauCeti.ParabolicSpaceTime.coordsHomeomorph {E : Type u_1} [PseudoMetricSpace E] : ParabolicSpaceTime E ≃ₜ E × ℝ

The homeomorphism between parabolic space-time and ordinary space-time E × ℝ. Functions on parabolic space-time are differentiated by transporting them along this map.

@[simp]

theorem TauCeti.ParabolicSpaceTime.coordsHomeomorph_apply {E : Type u_1} [PseudoMetricSpace E] (p : ParabolicSpaceTime E) : coordsHomeomorph p = (p.space, p.time)

@[simp]

theorem TauCeti.ParabolicSpaceTime.coordsHomeomorph_symm_apply {E : Type u_1} [PseudoMetricSpace E] (z : E × ℝ) : coordsHomeomorph.symm z = ofCoords z.1 z.2

theorem TauCeti.ParabolicSpaceTime.continuous_space {E : Type u_1} [PseudoMetricSpace E] : Continuous space

theorem TauCeti.ParabolicSpaceTime.continuous_time {E : Type u_1} [PseudoMetricSpace E] : Continuous time

theorem TauCeti.ParabolicSpaceTime.continuous_ofCoords {E : Type u_1} [PseudoMetricSpace E] : Continuous fun (z : E × ℝ) => ofCoords z.1 z.2

Building a point from its coordinates is jointly continuous in (x, t).

theorem TauCeti.ParabolicSpaceTime.continuous_slabMk {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} : Continuous fun (z : E × ↑(Set.Icc a b)) => slabMk z.1 z.2

Building a point of a slab from its coordinates is jointly continuous in (x, t).

theorem TauCeti.ParabolicSpaceTime.continuous_slabTime {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} : Continuous slabTime

noncomputable def TauCeti.ParabolicSpaceTime.spatialSlice {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} (t : ↑(Set.Icc a b)) : C(E, ↑(slab a b))

The spatial slice x ↦ (x, t) of a slab at the time t, as a continuous map.

@[simp]

theorem TauCeti.ParabolicSpaceTime.spatialSlice_apply {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} (t : ↑(Set.Icc a b)) (x : E) : (spatialSlice t) x = slabMk x t

noncomputable def TauCeti.ParabolicSpaceTime.timeSlice {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} (x : E) : C(↑(Set.Icc a b), ↑(slab a b))

The time slice t ↦ (x, t) of a slab at the position x, as a continuous map.

@[simp]

theorem TauCeti.ParabolicSpaceTime.timeSlice_apply {E : Type u_1} [PseudoMetricSpace E] {a b : ℝ} (x : E) (t : ↑(Set.Icc a b)) : (timeSlice x) t = slabMk x t

Time reversal

noncomputable def TauCeti.ParabolicSpaceTime.timeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) : ParabolicSpaceTime E ≃ᵢ ParabolicSpaceTime E

Reversal of time about T, (x, t) ↦ (x, T - t), an isometry of parabolic space-time.

@[simp]

theorem TauCeti.ParabolicSpaceTime.space_timeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) (p : ParabolicSpaceTime E) : ((timeReverse T) p).space = p.space

@[simp]

theorem TauCeti.ParabolicSpaceTime.time_timeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) (p : ParabolicSpaceTime E) : ((timeReverse T) p).time = T - p.time

@[simp]

theorem TauCeti.ParabolicSpaceTime.timeReverse_timeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) (p : ParabolicSpaceTime E) : (timeReverse T) ((timeReverse T) p) = p

Time reversal about T is an involution.

@[simp]

theorem TauCeti.ParabolicSpaceTime.timeReverse_symm {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) : (timeReverse T).symm = timeReverse T

theorem TauCeti.ParabolicSpaceTime.isClosed_slab {E : Type u_1} [PseudoMetricSpace E] (a b : ℝ) : IsClosed (slab a b)

theorem TauCeti.ParabolicSpaceTime.preimage_timeReverse_slab {E : Type u_1} [PseudoMetricSpace E] (T a b : ℝ) : ⇑(timeReverse T) ⁻¹' slab a b = slab (T - b) (T - a)

Reversal of time about T exchanges the slabs E × [a, b] and E × [T - b, T - a].

noncomputable def TauCeti.ParabolicSpaceTime.slabTimeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) {a b a' b' : ℝ} (ha : a' = T - b) (hb : b' = T - a) : ↑(slab a' b') ≃ᵢ ↑(slab a b)

Reversal of time about T, as an isometry from the slab E × [a', b'] onto the slab E × [a, b], where a' = T - b and b' = T - a.

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabTimeReverse_slabMk {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) {a b a' b' : ℝ} (ha : a' = T - b) (hb : b' = T - a) (x : E) (t : ↑(Set.Icc a' b')) : (slabTimeReverse T ha hb) (slabMk x t) = slabMk x ⟨T - ↑t, ⋯⟩

Time reversal between slabs sends (x, t) to (x, T - t).

@[simp]

theorem TauCeti.ParabolicSpaceTime.coe_slabTimeReverse {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) {a b a' b' : ℝ} (ha : a' = T - b) (hb : b' = T - a) (p : ↑(slab a' b')) : ↑((slabTimeReverse T ha hb) p) = (timeReverse T) ↑p

@[simp]

theorem TauCeti.ParabolicSpaceTime.slabTimeReverse_symm {E : Type u_1} [PseudoMetricSpace E] (T : ℝ) {a b a' b' : ℝ} (ha : a' = T - b) (hb : b' = T - a) : (slabTimeReverse T ha hb).symm = slabTimeReverse T ⋯ ⋯

The inverse of time reversal between slabs is time reversal in the opposite direction.