The terminal slice of the blow-up limit #
The pairing modulus of prop:blowup-limit is uniform up to time zero and the
rescaled terminal slices vanish in local L². Together with the
convergence of every negative-time slice this gives the zero distributional
terminal trace of the limit (the terminal-slice step).
theorem
ESS.blowupLimitAssembly_pairing_tendsto_zero_of_unit_balls
(g : ℕ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hg : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (g k) MeasureTheory.volume)
(hloc :
∀ (c : CKN.Foundation.Parabolic.Vec3),
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm (g k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1)))
Filter.atTop (nhds 0))
(ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hψ : Continuous ψ)
(hψc : HasCompactSupport ψ)
:
Filter.Tendsto (fun (k : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, g k x i * ψ x i) Filter.atTop
(nhds 0)
Fields vanishing in L² on every unit ball have vanishing pairings with every compactly supported continuous test.
theorem
ESS.blowupLimitAssembly_zero_trace
(U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(V : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hslices :
∀ t < 0,
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, U (x, t) i * ψ x i)
MeasureTheory.volume ∧ Filter.Tendsto (fun (k : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, V k (x, t) i * ψ x i)
Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * ψ x i)))
(hmod :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∃ (A : ℝ) (B : ℝ) (θ : ℝ),
0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (s t : ℝ),
s ∈ Set.Icc (-1) 0 →
t ∈ Set.Icc (-1) 0 →
|(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, V k (x, t) i * ψ x i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, V k (x, s) i * ψ x i| ≤ A * dist t s + B * dist t s ^ θ)
(hterm :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
Filter.Tendsto (fun (k : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, V k (x, 0) i * ψ x i)
Filter.atTop (nhds 0))
:
Convergence of every negative-time slice pairing, a uniform modulus up to time zero, and vanishing terminal pairings give a zero distributional terminal trace.