Topology of parabolic space-time

The parabolic metric of CKN.Foundation.Parabolic.Basic is obtained by pulling back the product metric of L²(ℝ³) × ℝ (the time factor being snowflaked) along parabolicMap. This file identifies the resulting topology with the product topology of the spatial variable and time. It is the bridge that lets openness and closure of the paper's space-time carriers be read off from the corresponding statements on Vec3 × ℝ: in particular the space-time set def:sws, whose carrier is Ω × I, is open for open Ω and I, and the interior and closure of a parabolic cylinder are computed from the Euclidean ball and the intervals Ioo and Icc.

theorem CKN.Foundation.Parabolic.isInducing_parabolicMap : Topology.IsInducing parabolicMap

The topology on ParabolicPoint is the one induced by parabolicMap, i.e. the pullback of the product topology on L²(ℝ³) × ℝ.

theorem CKN.Foundation.Parabolic.continuous_fst_parabolicPoint : Continuous fun (p : ParabolicPoint) => p.1

The spatial coordinate is continuous for the parabolic topology: the first factor of parabolicMap is WithLp.toLp 2, which is continuous for the L² product topology.

theorem CKN.Foundation.Parabolic.continuous_snd_parabolicPoint : Continuous fun (p : ParabolicPoint) => p.2

The time coordinate is continuous for the parabolic topology: the second factor of parabolicMap is the snowflaking equivalence, which carries the same topology as ℝ.

theorem CKN.Foundation.Parabolic.continuous_parabolicMap_prod : Continuous fun (q : Vec3 × ℝ) => parabolicMap q

parabolicMap, read on the product Vec3 × ℝ with its product topology, is continuous: both WithLp.toLp 2 and the snowflaking equivalence are.

theorem CKN.Foundation.Parabolic.continuous_parabolicPoint_to_prod : Continuous fun (p : ParabolicPoint) => (p.1, p.2)

The identity map from the parabolic space-time to Vec3 × ℝ with the product topology is continuous.

theorem CKN.Foundation.Parabolic.continuous_prod_to_parabolicPoint : Continuous (have this := fun (q : Vec3 × ℝ) => (q.1, q.2); this)

The identity map from Vec3 × ℝ with the product topology to the parabolic space-time is continuous; equivalently, the product topology is finer than the parabolic topology.

def CKN.Foundation.Parabolic.parabolicHomeomorph : ParabolicPoint ≃ₜ Vec3 × ℝ

The identity, viewed as a homeomorphism from the parabolic space-time to Vec3 × ℝ with the product topology. This is the topology bridge: set-theoretic operations on space-time sets may be performed on the product instead.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CKN.Foundation.Parabolic.parabolicHomeomorph_apply (p : ParabolicPoint) : parabolicHomeomorph p = (p.1, p.2)

@[simp]

theorem CKN.Foundation.Parabolic.parabolicHomeomorph_symm_apply (q : Vec3 × ℝ) : parabolicHomeomorph.symm q = (q.1, q.2)

@[simp]

theorem CKN.Foundation.Parabolic.parabolicHomeomorph_preimage (s : Set (Vec3 × ℝ)) : ⇑parabolicHomeomorph ⁻¹' s = s

The topology bridge, as a statement about preimages: the homeomorphism is the identity on points, so preimages of product sets are the sets themselves.

theorem CKN.Foundation.Parabolic.topologicalSpace_eq_induced_prod : inferInstance = TopologicalSpace.induced (fun (p : ParabolicPoint) => (p.1, p.2)) instTopologicalSpaceProd

The instance topology on ParabolicPoint equals the product topology on Vec3 × ℝ transported along the identity.

def CKN.Foundation.Parabolic.vec3Homeomorph : Vec3 ≃ₜ L2Vec3

The identification of Vec3 (with its product-of-coordinates topology) with L²(ℝ³), under which vec3EuclideanNorm is the L² norm.

Equations

• CKN.Foundation.Parabolic.vec3Homeomorph = (PiLp.homeomorph 2 fun (x : Fin 3) => ℝ).symm

@[simp]

theorem CKN.Foundation.Parabolic.vec3Homeomorph_apply (v : Vec3) : vec3Homeomorph v = WithLp.toLp 2 v

theorem CKN.Foundation.Parabolic.isOpen_vec3Ball (x : Vec3) (r : ℝ) : IsOpen (vec3Ball x r)

Under the identification of Vec3 with L²(ℝ³), the Euclidean ball vec3Ball is a metric ball, hence open.

theorem CKN.Foundation.Parabolic.closure_vec3Ball {x : Vec3} {r : ℝ} (hr : 0 < r) : closure (vec3Ball x r) = {y : Vec3 | vec3EuclideanNorm (y - x) ≤ r}

The closure of the Euclidean open ball of positive radius is the corresponding closed set {y | vec3EuclideanNorm (y - x) ≤ r}.

theorem CKN.Foundation.Parabolic.isOpen_spaceTimeSet (Ω : Set Vec3) (I : Set ℝ) (hΩ : IsOpen Ω) (hI : IsOpen I) : IsOpen (spaceTimeSet Ω I)

The space-time carrier def:sws is open when both Ω and I are open.

theorem CKN.Foundation.Parabolic.interior_parabolicCylinder (x : Vec3) (t r : ℝ) : interior (parabolicCylinder x t r) = vec3Ball x r ×ˢ Set.Ioo (t - r ^ 2) t

The interior of a parabolic cylinder is the product of the Euclidean open ball and the open time interval: Ioc is not open, so its interior is Ioo.

theorem CKN.Foundation.Parabolic.closure_parabolicCylinder {x : Vec3} {t r : ℝ} (hr : 0 < r) : closure (parabolicCylinder x t r) = {y : Vec3 | vec3EuclideanNorm (y - x) ≤ r} ×ˢ Set.Icc (t - r ^ 2) t

The closure of a parabolic cylinder of positive radius is the product of the Euclidean closed ball and the closed time interval.

theorem CKN.Foundation.Parabolic.parabolicCylinder_subset_closure (x : Vec3) (t r : ℝ) : parabolicCylinder x t r ⊆ closure (parabolicCylinder x t r)

Every parabolic cylinder is contained in its closure.

theorem CKN.Foundation.Parabolic.closure_parabolicCylinder_mono {x : Vec3} {t r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hr : r₁ ≤ r₂) : closure (parabolicCylinder x t r₁) ⊆ closure (parabolicCylinder x t r₂)

Closures of parabolic cylinders are monotone in the radius.