Boundary values from shrinking Gaussian boxes

Continuity turns decay of the parabolic box averages in thm:uc into vanishing of the initial trace.

theorem ESS.uc_squared_norm_integrable_on_subset (S B : Set CKN.Foundation.Parabolic.ParabolicPoint) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hweak : MeasureTheory.LocallyIntegrableOn w S MeasureTheory.volume) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖w z‖ₑ ^ 2 < ⊤) (hsub : B ⊆ S) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) B MeasureTheory.volume

Finite quadratic vector energy controls the Euclidean square on every measurable subregion.

theorem ESS.uc_box_normalized_measure (x : CKN.Foundation.Parabolic.Vec3) {t : ℝ} (ht : 0 < t) : t.rpow (-(5 / 2)) * MeasureTheory.volume.real (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t))) = √2 ^ 3 * (Real.pi * 4 / 3)

The shrinking box has a fixed volume after parabolic normalization.

theorem ESS.uc_box_measure_lt_top (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : MeasureTheory.volume (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t))) < ⊤

Every shrinking box has finite space-time volume.

theorem ESS.uc_shrinking_average_to_trace (x : CKN.Foundation.Parabolic.Vec3) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (τ : ℝ) (hτ : 0 < τ) (hcont : ContinuousWithinAt w S (x, 0)) (hB : ∀ (t : ℝ), 0 < t → t < τ → CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t)) ⊆ S) (hInt : ∀ (t : ℝ), 0 < t → t < τ → MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t))) MeasureTheory.volume) (havg : Filter.Tendsto (fun (t : ℝ) => t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : w (x, 0) = 0

Decay of integrable box averages and continuity give a zero boundary value (thm:uc).

theorem ESS.uc_shrinking_average_to_trace_on_cylinder (R T : ℝ) (hT : 0 < T) (x₀ x : CKN.Foundation.Parabolic.Vec3) (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ico 0 T))) (hwloc : MeasureTheory.LocallyIntegrableOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)) MeasureTheory.volume) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 < ⊤) (havg : Filter.Tendsto (fun (t : ℝ) => t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : w (x, 0) = 0

The source continuity and quadratic-integrability hypotheses supply the shrinking-box trace argument on a spatial cylinder (thm:uc).