Heat Critical Measurable

The smooth-data heat orbit extended to nonpositive times by its initial value, for use in lem:pv-heat-critical.

noncomputable def ESS.heatConvSmoothExt (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : ℝ

The smooth-data heat orbit extended to nonpositive times by its initial value, for use in lem:pv-heat-critical.

Equations

• ESS.heatConvSmoothExt f t x = if t ≤ 0 then f x else CKN.Foundation.Heat.heatConv t f x

theorem ESS.heatConvSmoothExt_joint_measurable {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : Measurable (Function.uncurry fun (t : ℝ) => heatConvSmoothExt f t)

The extended scalar heat orbit is jointly measurable, as used in lem:pv-heat-critical.

noncomputable def ESS.heatConvVec3SmoothExt (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The componentwise extended vector heat orbit is jointly measurable in space and time for smooth compact data in lem:pv-heat-critical.

Equations

• ESS.heatConvVec3SmoothExt b t x i = ESS.heatConvSmoothExt (fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) t x

theorem ESS.heatConvVec3SmoothExt_joint_measurable {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) : Measurable (Function.uncurry fun (t : ℝ) => heatConvVec3SmoothExt b t)

Joint measurability of the extended vector heat orbit in lem:pv-heat-critical.