The forced heat response of a double-divergence-free tensor is divergence free

Let G ∈ L² be a tensor supported in the slab Q_τ = ℝ³ × (0, τ) with ∑_ij ∂_i ∂_j G_ij(·, s) = 0 in the sense of distributions for almost every time s. Then the forced heat response Z_i = ∑_j ∂_j W₊ ⋆ G_ij is weakly divergence free on almost every time slice of the slab. This is the divergence-free clause of the local solution in prop:pv-local-solution, where G = -(F + p I) with p the Riesz pressure of F.

The proof is by duality: at almost every time the kernel integrals converge absolutely against the weight forcedHeatWeight (kernel_weighted_lintegral_le), and forcedHeat_divergence_pairing_eq_zero evaluates the pairing with ∂_i ψ as zero. A general tensor is first replaced by a measurable modification, which does not change the response.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_3 : MeasureTheory.volume.IsAddHaarMeasure

theorem ESS.forcedHeat_weighted_slice_lintegral_lt_top {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hGm : ∀ (i j : Fin 3), Measurable (G i j)) (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), ∀ (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)‖ₑ < ⊤

For a measurable square-integrable tensor supported in the slab, the weighted kernel integrals defining its forced heat response are finite on almost every time slice of the slab.

theorem ESS.tensor_slice_memLp_two_ae {τ : ℝ} {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) : ∀ᵐ (s : ℝ), ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => G i j (y, s)) 2 MeasureTheory.volume

Almost every time slice of a square-integrable tensor supported in the slab is square integrable.

theorem ESS.forcedHeat_divFree_of_measurable {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hGm : ∀ (i j : Fin 3), Measurable (G i j)) (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) (hdd : ∀ᵐ (s : ℝ), ∀ (φ : 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) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), ∀ (ψ : CKN.WeakTestFunction Set.univ), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedHeat G (x, t) i * ψ.partialDeriv i x = 0

The divergence-free property of the forced heat response for a measurable double-divergence-free tensor in L² supported in the slab.

theorem ESS.forcedHeat_divFree {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) (hdd : ∀ᵐ (s : ℝ), ∀ (φ : 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) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), ∀ (ψ : CKN.WeakTestFunction Set.univ), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedHeat G (x, t) i * ψ.partialDeriv i x = 0

The forced heat response of a double-divergence-free tensor is divergence free: for G ∈ L² supported in Q_τ with ∑_ij ∂_i ∂_j G_ij(·, s) = 0 in the sense of distributions for almost every s, almost every time slice of Z = forcedHeat G in (0, τ) satisfies ∫ Z · ∇ψ = 0 for every test function ψ. This is the divergence-free clause of prop:pv-local-solution.