The forward heat representation of a compactly supported test function

For a smooth, compactly supported ζ : Vec3 × ℝ → ℝ, the value ζ (x, s) is recovered from the image of ζ under the forward heat operator ∂ₜ - Δ, convolved against the causal heat kernel run backward from (x, s): ζ (x, s) = ∫ Γ(x - z.1, s - z.2) (∂ₜζ - Δζ) z. Since heatKernel vanishes for a nonpositive second argument, the integral is effectively over the past {z | z.2 < s}. This is the base case of the pointwise heat-potential bound used for the interior estimates in the proof of lem:aniso:annulus.

The proof reduces to CKN's backwardTestPotential_heat_equation (which differentiates the potential of a compactly supported source) applied to the time-reflection of ζ, combined with the (heat-equation-free) fact that differentiation commutes with backwardTestPotential. This converts CKN's "potential of a derivative recovers a delta-tested value" statement about the future-integrating kernel into the forward, past-integrating representation stated here; no uniqueness argument for the heat equation is used anywhere.

def CIV.reflectTime (ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

Time-reflection of a space-time function.

Equations

• CIV.reflectTime ζ z = ζ (z.1, -z.2)

theorem CIV.contDiff_reflectTime {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hζ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => reflectTime ζ z

theorem CIV.hasCompactSupport_reflectTime {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hζc : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => reflectTime ζ z

theorem CIV.timePartial_reflectTime {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (reflectTime ζ) z = -CKN.timePartial ζ (z.1, -z.2)

theorem CIV.spatialPartial_reflectTime {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (reflectTime ζ) i z = CKN.spatialPartial ζ i (z.1, -z.2)

theorem CIV.spatialSecondPartial_reflectTime {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (i j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialSecondPartial (reflectTime ζ) i j z = CKN.spatialSecondPartial ζ i j (z.1, -z.2)

theorem CIV.measurePreserving_reflectShift (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : MeasureTheory.MeasurePreserving (fun (t : CKN.Foundation.Parabolic.Vec3 × ℝ) => (x - t.1, t.2 - r)) MeasureTheory.volume MeasureTheory.volume

The map t ↦ (x - t.1, t.2 - r) is measure preserving on Vec3 × ℝ.

theorem CIV.measurableEmbedding_reflectShift (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : MeasurableEmbedding fun (t : CKN.Foundation.Parabolic.Vec3 × ℝ) => (x - t.1, t.2 - r)

theorem CIV.backwardTestPotential_reflectTime_eq (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : CKN.Foundation.Heat.backwardTestPotential (reflectTime φ) (x, r) = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernel (x - z.1) (-r - z.2) * φ z

theorem CIV.integrable_reflectTime_potential {φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ z) (hφc : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ z) (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernel (x - z.1) (-r - z.2) * φ z) MeasureTheory.volume

theorem CIV.HB1_forward_representation {ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hζ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) (hζc : HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : ζ (x, s) = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.Foundation.Heat.heatKernel (x - z.1) (s - z.2) * (CKN.timePartial ζ z - ∑ i : Fin 3, CKN.spatialSecondPartial ζ i i z)