The divergence pairing of the forced heat response at a fixed time

Fix a time t at which the weighted kernel integrals of a measurable tensor G are finite. Pairing the forced heat response Z_i = ∑_j ∂_j W₊ ⋆ G_ij at time t with ∂_i ψ for a test function ψ and exchanging the integrals writes the pairing as an integral over the kernel variable (y, r); at every kernel time r > 0 for which the slice G(·, t - r) is square integrable and double-divergence free, the inner integral vanishes by kernel_translate_pairing_sum_eq_zero. This is the fixed-time step of the divergence-free property of the forced heat response in prop:pv-local-solution.

theorem ESS.abs_le_mul_forcedHeatWeight_of_vec3 {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : Continuous φ) (hφc : HasCompactSupport φ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), |φ x| ≤ c * forcedHeatWeight x

A continuous compactly supported function on Vec3 is dominated by a multiple of the weight forcedHeatWeight.

theorem ESS.forcedHeat_divergence_pairing_eq_zero {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hGm : ∀ (i j : Fin 3), Measurable (G i j)) {t : ℝ} (hfin : ∀ (i j : Fin 3), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (forcedHeatWeight x) * ∫⁻ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ‖CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * G i j (x - p.1, t - p.2)‖ₑ < ⊤) (hslice : ∀ᵐ (s : ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => G i j (y, s)) 2 MeasureTheory.volume) ∧ ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : CKN.Foundation.Parabolic.Vec3), G i j (y, s) * CKN.mixedSecond φ i j y = 0) (ψ : CKN.WeakTestFunction Set.univ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedHeat G (x, t) i * ψ.partialDeriv i x = 0

At a time t where the weighted kernel integrals of a measurable tensor are finite, and for which almost every earlier slice is square integrable and double-divergence free, the forced heat response at time t is weakly divergence free.