Geometry of the symmetric parabolic window

Display eq:parabolic-ball of paper/ckn.tex presents the parabolic ball of radius R about z₀ = (x₀, t₀) as the product of the spatial Euclidean ball B_R(x₀) with the symmetric time interval (t₀ - R², t₀ + R²), written 𝔅_R(z₀).

This file records the elementary spatial facts needed to rewrite membership between the one-sided and symmetric carriers: the explicit round ball euclideanBall is the norm ball vec3Ball, and the closure of a smaller norm ball lies inside any larger one, so the boundary of an inner carrier is absorbed by the slightly larger open window used in display (3.5).

The module contains no analytic content: it is pure parabolic geometry, and its statements are used only to rewrite membership between the one-sided and symmetric carriers.

theorem CKN.Core.Step4.euclideanBall_eq_vec3Ball_of_pos {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : euclideanBall x₀ r = Foundation.Parabolic.vec3Ball x₀ r

The explicit round ball euclideanBall x₀ r of CKN/Foundation/Sobolev and the norm ball vec3Ball x₀ r of CKN/Foundation/Parabolic describe the same subset of Vec3 whenever r > 0, because both are cut out by the strict inequality vecEuclideanNorm (x - x₀) < r.

theorem CKN.Core.Step4.closure_vec3Ball_subset_vec3Ball {x : Foundation.Parabolic.Vec3} {r s : ℝ} (hr : 0 < r) (hrs : r < s) : closure (Foundation.Parabolic.vec3Ball x r) ⊆ Foundation.Parabolic.vec3Ball x s

The closed ball of radius r is contained in the open ball of any larger radius s, so the closure of vec3Ball x r is a subset of vec3Ball x s when 0 < r < s. This lets the boundary of an inner carrier be absorbed into the slightly larger open window used in display (3.5).