Parabolic space-time geometry

The spatial geometry uses the Euclidean norm on Fin 3 → ℝ, defined from the finite sum of squares. This is deliberate: the ambient function space's default norm can be the sup norm, whereas the cylinders here are Euclidean.

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.Vec3 : Type

Native three-dimensional coordinate vectors.

Equations

• CKN.Foundation.Parabolic.Vec3 = (Fin 3 → ℝ)

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.L2Vec3 : Type

Three-dimensional coordinate vectors equipped with their Euclidean L² norm.

Equations

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

def CKN.Foundation.Parabolic.ParabolicPoint : Type

Space-time points, given the parabolic metric below rather than the product metric.

Equations

• CKN.Foundation.Parabolic.ParabolicPoint = (CKN.Foundation.Parabolic.Vec3 × ℝ)

theorem CKN.Foundation.Parabolic.half_pos : 0 < 1 / 2

theorem CKN.Foundation.Parabolic.half_le_one : 1 / 2 ≤ 1

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.SnowTime : Type

Time equipped with the square-root snowflake metric.

Equations

• CKN.Foundation.Parabolic.SnowTime = Metric.Snowflaking ℝ (1 / 2) CKN.Foundation.Parabolic.half_pos CKN.Foundation.Parabolic.half_le_one

noncomputable def CKN.Foundation.Parabolic.vec3EuclideanNorm (v : Vec3) : ℝ

Euclidean length of a native three-dimensional coordinate vector.

Equations

• CKN.Foundation.Parabolic.vec3EuclideanNorm v = √(∑ i : Fin 3, v i ^ 2)

@[instance_reducible]

instance CKN.Foundation.Parabolic.instMeasurableSpaceParabolicPoint : MeasurableSpace ParabolicPoint

Equations

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

@[instance_reducible]

noncomputable instance CKN.Foundation.Parabolic.instMeasurableSpaceSnowTime : MeasurableSpace SnowTime

Equations

• CKN.Foundation.Parabolic.instMeasurableSpaceSnowTime = borel CKN.Foundation.Parabolic.SnowTime

instance CKN.Foundation.Parabolic.instBorelSpaceSnowTime : BorelSpace SnowTime

noncomputable def CKN.Foundation.Parabolic.parabolicMeasurableEquiv : ParabolicPoint ≃ᵐ L2Vec3 × SnowTime

Measurable equivalence to Euclidean space times snowflaked time.

Equations

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

noncomputable def CKN.Foundation.Parabolic.parabolicMap (p : ParabolicPoint) : L2Vec3 × SnowTime

Coordinate map into the product carrying the parabolic metric.

Equations

• CKN.Foundation.Parabolic.parabolicMap p = CKN.Foundation.Parabolic.parabolicMeasurableEquiv p

theorem CKN.Foundation.Parabolic.parabolicMap_injective : Function.Injective parabolicMap

@[instance_reducible]

noncomputable instance CKN.Foundation.Parabolic.parabolicMetricSpace : MetricSpace ParabolicPoint

Equations

• CKN.Foundation.Parabolic.parabolicMetricSpace = MetricSpace.induced CKN.Foundation.Parabolic.parabolicMap CKN.Foundation.Parabolic.parabolicMap_injective inferInstance

@[reducible, inline]

noncomputable abbrev CKN.Foundation.Parabolic.parabolicPseudoMetricSpace : PseudoMetricSpace ParabolicPoint

Pseudometric presentation of the parabolic metric for explicit metric-space arguments.

Equations

• CKN.Foundation.Parabolic.parabolicPseudoMetricSpace = CKN.Foundation.Parabolic.parabolicMetricSpace.toPseudoMetricSpace

instance CKN.Foundation.Parabolic.instSecondCountableTopologyParabolicPoint : SecondCountableTopology ParabolicPoint

instance CKN.Foundation.Parabolic.instBorelSpaceParabolicPoint : BorelSpace ParabolicPoint

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_eq_l2 (v : Vec3) : vec3EuclideanNorm v = ‖WithLp.toLp 2 v‖

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_nonneg (v : Vec3) : 0 ≤ vec3EuclideanNorm v

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_zero : vec3EuclideanNorm 0 = 0

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_smul (a : ℝ) (v : Vec3) : vec3EuclideanNorm (a • v) = |a| * vec3EuclideanNorm v

noncomputable def CKN.Foundation.Parabolic.parabolicDist (p q : ParabolicPoint) : ℝ

Maximum of spatial Euclidean distance and square-root time separation.

Equations

• CKN.Foundation.Parabolic.parabolicDist p q = max (CKN.Foundation.Parabolic.vec3EuclideanNorm (p.1 - q.1)) √|p.2 - q.2|

theorem CKN.Foundation.Parabolic.dist_eq_parabolicDist (p q : ParabolicPoint) : dist p q = parabolicDist p q

def CKN.Foundation.Parabolic.vec3Ball (x : Vec3) (r : ℝ) : Set Vec3

Open Euclidean ball in native spatial coordinates.

Equations

• CKN.Foundation.Parabolic.vec3Ball x r = {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) < r}

def CKN.Foundation.Parabolic.parabolicCylinder (x : Vec3) (t r : ℝ) : Set ParabolicPoint

Backward parabolic cylinder with spatial radius r and time depth r ^ 2.

Equations

• CKN.Foundation.Parabolic.parabolicCylinder x t r = CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioc (t - r ^ 2) t

@[simp]

theorem CKN.Foundation.Parabolic.mem_vec3Ball {x y : Vec3} {r : ℝ} : y ∈ vec3Ball x r ↔ vec3EuclideanNorm (y - x) < r

@[simp]

theorem CKN.Foundation.Parabolic.mem_parabolicCylinder {x y : Vec3} {t s r : ℝ} : (y, s) ∈ parabolicCylinder x t r ↔ vec3EuclideanNorm (y - x) < r ∧ t - r ^ 2 < s ∧ s ≤ t

theorem CKN.Foundation.Parabolic.vec3Ball_mono {x : Vec3} {r₁ r₂ : ℝ} (hr : r₁ ≤ r₂) : vec3Ball x r₁ ⊆ vec3Ball x r₂

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

def CKN.Foundation.Parabolic.parabolicTranslate (a : Vec3) (τ : ℝ) (p : ParabolicPoint) : ParabolicPoint

Space-time translation by a spatial vector and time offset.

Equations

• CKN.Foundation.Parabolic.parabolicTranslate a τ p = (a + p.1, τ + p.2)

def CKN.Foundation.Parabolic.parabolicScale (a : ℝ) (p : ParabolicPoint) : ParabolicPoint

Parabolic scaling, linear in space and quadratic in time.

Equations

• CKN.Foundation.Parabolic.parabolicScale a p = (a • p.1, a ^ 2 * p.2)

theorem CKN.Foundation.Parabolic.parabolicCylinder_translate (a x : Vec3) (τ t r : ℝ) : parabolicTranslate a τ '' parabolicCylinder x t r = parabolicCylinder (a + x) (τ + t) r

theorem CKN.Foundation.Parabolic.parabolicCylinder_scale {x : Vec3} {t r a : ℝ} (ha : 0 < a) : parabolicScale a '' parabolicCylinder x t r = parabolicCylinder (a • x) (a ^ 2 * t) (a * r)

@[instance_reducible]

noncomputable instance CKN.Foundation.Parabolic.instMeasureSpaceParabolicPoint : MeasureTheory.MeasureSpace ParabolicPoint

Equations

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

theorem CKN.Foundation.Parabolic.vec3Ball_measurable (x : Vec3) (r : ℝ) : MeasurableSet (vec3Ball x r)

theorem CKN.Foundation.Parabolic.volume_vec3Ball (x : Vec3) (r : ℝ) : MeasureTheory.volume (vec3Ball x r) = MeasureTheory.volume (vec3Ball 0 r)

theorem CKN.Foundation.Parabolic.volume_parabolicCylinder (x : Vec3) (t r : ℝ) : MeasureTheory.volume (parabolicCylinder x t r) = MeasureTheory.volume (vec3Ball x r) * ENNReal.ofReal (r ^ 2)

theorem CKN.Foundation.Parabolic.volume_parabolicCylinder_zero (x : Vec3) (t r : ℝ) : MeasureTheory.volume (parabolicCylinder x t r) = MeasureTheory.volume (vec3Ball 0 r) * ENNReal.ofReal (r ^ 2)

noncomputable def CKN.Foundation.Parabolic.parabolicHausdorffMeasure (d : ENNReal) : MeasureTheory.Measure ParabolicPoint

Hausdorff measure computed using the parabolic metric and the real value of the exponent.

Equations

• CKN.Foundation.Parabolic.parabolicHausdorffMeasure d = MeasureTheory.Measure.hausdorffMeasure d.toReal

theorem CKN.Foundation.Parabolic.metricBall_subset_parabolicCylinder {x : Vec3} {t r : ℝ} (hr : 0 < r) : Metric.ball (x, t - r ^ 2 / 2) (r / 2) ⊆ parabolicCylinder x t r

theorem CKN.Foundation.Parabolic.parabolicCylinder_subset_metricBall {x : Vec3} {t r : ℝ} (hr : 0 < r) : parabolicCylinder x t r ⊆ Metric.ball (x, t - r ^ 2 / 2) r