The parabolic ball and its volume

This file records the literal displays of paper/ckn.tex that describe the open parabolic ball 𝔅_r(z) of the metric dpar (equation eq:parabolic-ball and Lemma lem:parabolic-metric):

• 𝔅_r(z) = B_r(x) × (t - r², t + r²) for z = (x, t);
• C_r(z) ⊆ 𝔅_r(z) and 𝔅_r(z) ⊆ C_{2r}(x, t + r²), where C_r(z) is the parabolic cylinder B_r(x) × (t - r², t];
• |𝔅_r(z)| = (8π/3) r⁵.

The spatial ball vec3Ball x r uses the Euclidean norm on Fin 3 → ℝ (vec3EuclideanNorm), so its volume is computed by transporting Mathlib's volume of the Euclidean ball in EuclideanSpace ℝ (Fin 3) along the measure-preserving equivalence WithLp.toLp 2.

theorem CKN.Foundation.Parabolic.metricBall_eq_parabolicBall (z : ParabolicPoint) (r : ℝ) : Metric.ball z r = vec3Ball z.1 r ×ˢ Set.Ioo (z.2 - r ^ 2) (z.2 + r ^ 2)

Equation eq:parabolic-ball: the open parabolicDist-ball of radius r about z = (x, t) is the product of the Euclidean ball vec3Ball x r with the open time interval (t - r², t + r²).

theorem CKN.Foundation.Parabolic.parabolicCylinder_subset_metricBall_sameCenter (z : ParabolicPoint) {r : ℝ} (hr : 0 < r) : parabolicCylinder z.1 z.2 r ⊆ Metric.ball z r

Lemma lem:parabolic-metric: the parabolic cylinder C_r(z) is contained in the open ball 𝔅_r(z) of the same center and radius. Every point of the cylinder with time coordinate exactly t lies in the open time interval (t - r², t + r²) because r > 0.

theorem CKN.Foundation.Parabolic.metricBall_subset_parabolicCylinder_doubled (z : ParabolicPoint) {r : ℝ} (hr : 0 < r) : Metric.ball z r ⊆ parabolicCylinder z.1 (z.2 + r ^ 2) (2 * r)

Lemma lem:parabolic-metric: the open parabolic ball 𝔅_r(z) is contained in the cylinder of radius 2r based at (x, t + r²), i.e. 𝔅_r(z) ⊆ C_{2r}(x, t + r²).

theorem CKN.Foundation.Parabolic.volume_vec3Ball_zero (r : ℝ) : MeasureTheory.volume (vec3Ball 0 r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)

The volume of the open Euclidean ball of radius r centred at the origin of Vec3 = Fin 3 → ℝ, namely (4π/3) r³. The Euclidean norm on Fin 3 → ℝ is the L² norm, so this is Mathlib's EuclideanSpace.volume_ball_fin_three, transported along the measure-preserving equivalence WithLp.toLp 2.

theorem CKN.Foundation.Parabolic.volume_vec3Ball_eq (x : Vec3) (r : ℝ) : MeasureTheory.volume (vec3Ball x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)

The volume of the open Euclidean ball of radius r centred at any point of Vec3, namely (4π/3) r³; this is volume_vec3Ball_zero together with translation invariance of Lebesgue measure.

theorem CKN.Foundation.Parabolic.volume_metricBall (z : ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.volume (Metric.ball z r) = ENNReal.ofReal (8 * Real.pi / 3 * r ^ 5)

The volume of the parabolic ball: |𝔅_r(z)| = (8π/3) r⁵, the product of the spatial ball volume (4π/3) r³ and the time interval length 2r².