The heat orbit of an L² datum against the backward heat operator

Writing the heat orbit as ∫ Γ(x - y, t) f(y) dy and exchanging the order of integration, its pairing with -∂ₜφ - Δφ for a smooth compactly supported φ living in positive times becomes ∫ f(y) φ(y, 0) dy, because the causal heat kernel is a fundamental solution of the heat operator (heatKernelPlus_backward_heat_pairing). Since φ vanishes at time zero, the pairing is zero. This is the core of the weak heat equation for the heat orbit in prop:pv-local-solution.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_2 : MeasureTheory.volume.IsAddHaarMeasure

theorem ESS.hasCompactSupport_time_slice {G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hG : HasCompactSupport G) (t : ℝ) : HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => G (x, t)

A space-time function with compact support has compactly supported time slices.

theorem ESS.exists_pos_le_snd_of_isCompact {K : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact K) (hpos : K ⊆ {z : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < z.2}) : ∃ (δ : ℝ), 0 < δ ∧ ∀ z ∈ K, δ ≤ z.2

A compact set of space-time points with positive times lies above a positive time.

noncomputable def ESS.backwardHeatOp (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The backward heat operator -∂ₜφ - Δφ of a space-time function, written with directional derivatives on Vec3 × ℝ.

Equations

• ESS.backwardHeatOp φ z = -(fderiv ℝ φ z) (0, 1) - ∑ j : Fin 3, (fderiv ℝ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ φ q) (CKN.basisVec j, 0)) z) (CKN.basisVec j, 0)

theorem ESS.backwardHeatOp_eq_zero_of_notMem {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport φ) : backwardHeatOp φ z = 0

The backward heat operator of a function vanishes outside its support.

theorem ESS.backwardHeatOp_continuous {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : Continuous (backwardHeatOp φ)

The backward heat operator of a smooth function is continuous.

theorem ESS.integral_norm_kernel_le {k f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : MeasureTheory.MemLp k 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) : ∫ (y : CKN.Foundation.Parabolic.Vec3), ‖k (x - y) * f y‖ ≤ (MeasureTheory.eLpNorm k 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

The absolute convolution integral of two L² functions is bounded by the product of their L² norms.

theorem ESS.heatConv_eq_integral_sub (t : ℝ) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Heat.heatConv t f x = ∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Heat.heatKernel (x - y) t * f y

The Gaussian convolution with the kernel evaluated at x - y.

theorem ESS.heatConv_backwardHeatOp_integral_eq_zero {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hpos : tsupport φ ⊆ {z : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < z.2}) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatConv z.2 f z.1 * backwardHeatOp φ z = 0

The heat orbit of an L² datum is annihilated by the backward heat operator of every smooth compactly supported function supported in positive times.