The weak heat equation for the heat orbit of a datum in J #
At each positive time the spatial gradient of the heat orbit is a weak
gradient, so the gradient pairing ∫ ∇h : ∇φ equals -∫ h · Δφ slice by
slice. The remaining space-time pairing ∫∫ h · (-∂ₜφ - Δφ) vanishes by
heatConv_backwardHeatOp_integral_eq_zero. This is the weak heat equation
clause of the heat orbit in prop:pv-local-solution.
theorem
ESS.integral_spaceTimeSet_univ_eq
{I : Set ℝ}
{G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I)))
:
Fubini on a slab ℝ³ × I: the space-time integral of an integrable
function is the time integral of its spatial integrals.
theorem
ESS.heatOrbit_weak_heat_equation
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(ha : CKN.IsInJ a)
{τ : ℝ}
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hφmem : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 τ))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), -∑ i : Fin 3, heatOrbit a z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z + ∑ i : Fin 3,
∑ j : Fin 3,
CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, z.2) i) j z.1 * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0
(h6) The heat orbit of a datum in J solves the heat equation weakly on
every slab ℝ³ × (0, τ).