Linearity of the forced heat response

The forced heat response is linear in the tensor wherever the defining kernel integrals converge absolutely; for smooth compactly supported tensors they always do. This is the linearity used for the bilinear response of lem:pv-stokes.

theorem ESS.forcedHeat_smul (c : ℝ) (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : forcedHeat (c • G) z = c • forcedHeat G z

The forced heat response is homogeneous.

theorem ESS.forcedHeat_add {G G' : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * G i j (z.1 - p.1, z.2 - p.2)) MeasureTheory.volume) (hG' : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * G' i j (z.1 - p.1, z.2 - p.2)) MeasureTheory.volume) : forcedHeat (G + G') z = forcedHeat G z + forcedHeat G' z

The forced heat response is additive at every point where the kernel integrals of both tensors converge absolutely.

theorem ESS.forcedHeat_integrand_integrable {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * G i j (z.1 - p.1, z.2 - p.2)) MeasureTheory.volume

For a smooth compactly supported tensor the kernel integrals defining the forced heat response converge absolutely at every point.