Zero extensions of the all-time trace representative

The jointly measurable representative can be zero-extended from its closed source cylinder and then rescaled as a measurable field on all of space-time.

noncomputable def ESS.blowupLimitTraceZeroExtension {a b : ℝ} (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc a b) → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The all-time trace representative, extended by zero outside its closed source cylinder.

Equations

• ESS.blowupLimitTraceZeroExtension W z = if hz : z.1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4) ∧ z.2 ∈ Set.Icc a b then W (z.1, ⟨z.2, ⋯⟩) else 0

theorem ESS.measurable_blowupLimitTraceZeroExtension {a b : ℝ} (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc a b) → CKN.Foundation.Parabolic.Vec3) (hW : Measurable W) : Measurable (blowupLimitTraceZeroExtension W)

The zero extension of a jointly measurable trace representative is measurable on the full space-time carrier.

noncomputable def ESS.blowupLimitTraceRescaling {a b : ℝ} (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc a b) → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

Parabolically rescale the measurable, zero-extended all-time trace.

Equations

• ESS.blowupLimitTraceRescaling W x₀ t₀ r z = r • ESS.blowupLimitTraceZeroExtension W (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

theorem ESS.measurable_blowupLimitTraceRescaling {a b : ℝ} (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc a b) → CKN.Foundation.Parabolic.Vec3) (hW : Measurable W) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) : Measurable (blowupLimitTraceRescaling W x₀ t₀ r)

Every rescaling of the zero-extended trace is jointly measurable.