The zero-data forced heat response of a rough tensor

For a tensor G ∈ L^{5/2}(Q_τ) ∩ L²(Q_τ) vanishing outside the slab Q_τ = ℝ³ × (0,τ), the forced heat response Z = forcedHeat G (the kernel formula) has a weak spatial gradient in L²(Q_τ) with the energy bound, and satisfies the weak componentwise heat equation ∫∫ -Z_i ∂_t φ + ∑_j ∂_j Z_i ∂_j φ + ∑_j G_ij ∂_j φ = 0 against smooth tests compactly supported in the slab. With forcedHeat_rough_bounds this is the analytic core of lem:pv-stokes.

theorem ESS.forcedHeat_rough_weak_of_gradient {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hGsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) {Gs : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {DZ : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hGs : ∀ (k : ℕ) (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p) (hGsc : ∀ (k : ℕ) (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p) (hGspos : ∀ (k : ℕ) (i j : Fin 3), (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) (hGsconv : ∀ (i j : Fin 3), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p - G i j p) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (hDZsmem : ∀ (k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat (Gs k) w i) j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) (hDZmem : ∀ (i j : Fin 3), MeasureTheory.MemLp (DZ i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) (hDZlim : ∀ (i j : Fin 3), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat (Gs k) w i) j z) - DZ i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) Filter.atTop (nhds 0)) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hφ : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφc : HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφQ : (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) ⊆ Set.univ ×ˢ Set.Ioo 0 τ) : (∀ (i j : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), forcedHeat G z i * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), DZ i j z * φ z) ∧ ∀ (i : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), -(forcedHeat G z i * CKN.timePartial φ z) + ∑ j : Fin 3, DZ i j z * CKN.spatialPartial φ j z + ∑ j : Fin 3, G i j z * CKN.spatialPartial φ j z = 0

The weak identities of the rough forced heat response along a smooth approximation whose spatial gradients converge in L²(Q_τ): for every smooth test φ compactly supported in Q_τ, ∫ Z_i ∂_j φ = -∫ DZ_ij φ and ∫ -Z_i ∂_t φ + ∑_j DZ_ij ∂_j φ + ∑_j G_ij ∂_j φ = 0 on Q_τ.

theorem ESS.forcedHeat_rough_weak : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (τ : ℝ), 0 < τ → ∀ (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) → (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) → (∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) → ∃ (DZ : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (DZ i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => DZ i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ ∀ (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) → (HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) → (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) ⊆ Set.univ ×ˢ Set.Ioo 0 τ → (∀ (i j : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), forcedHeat G z i * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), DZ i j z * φ z) ∧ ∀ (i : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), -(forcedHeat G z i * CKN.timePartial φ z) + ∑ j : Fin 3, DZ i j z * CKN.spatialPartial φ j z + ∑ j : Fin 3, G i j z * CKN.spatialPartial φ j z = 0

The weak spatial gradient and the weak heat equation for the forced heat response of a tensor in L^{5/2} ∩ L² supported in Q_τ: the gradient lies in L²(Q_τ) with ‖∇Z‖_{L²(Q_τ)} ≤ C ‖G‖_{L²(Q_τ)}, and for every smooth test φ compactly supported in Q_τ, ∫ Z_i ∂_j φ = -∫ ∂_j Z_i φ and ∫ -Z_i ∂_t φ + ∑_j ∂_j Z_i ∂_j φ + ∑_j G_ij ∂_j φ = 0 on Q_τ.

theorem ESS.forcedHeat_rough_estimates : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (τ : ℝ), 0 < τ → ∀ (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) → (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) → (∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) → MeasureTheory.MemLp (forcedHeat G) 5 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ MeasureTheory.MemLp (forcedHeat G) 4 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ MeasureTheory.eLpNorm (forcedHeat G) 5 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ MeasureTheory.eLpNorm (forcedHeat G) 4 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) + MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => forcedHeat G (x, t)) 3 MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => forcedHeat G (x, t)) 2 MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ ∃ (DZ : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (DZ i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => DZ i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ ∀ (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) → (HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) → (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) ⊆ Set.univ ×ˢ Set.Ioo 0 τ → (∀ (i j : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), forcedHeat G z i * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), DZ i j z * φ z) ∧ ∀ (i : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), -(forcedHeat G z i * CKN.timePartial φ z) + ∑ j : Fin 3, DZ i j z * CKN.spatialPartial φ j z + ∑ j : Fin 3, G i j z * CKN.spatialPartial φ j z = 0

The zero-data forced heat estimates for a tensor G ∈ L^{5/2} ∩ L² supported in Q_τ, with one absolute constant C: the kernel response Z = forcedHeat G lies in L⁵(Q_τ) ∩ L⁴(Q_τ) with ‖Z‖₅ ≤ C ‖G‖_{5/2} and ‖Z‖₄ ≤ C (‖G‖_{5/2} + ‖G‖₂); for almost every t ∈ (0,τ), ‖Z(t)‖₃ ≤ C ‖G‖_{5/2} and ‖Z(t)‖₂ ≤ C ‖G‖₂; and Z has a weak spatial gradient in L²(Q_τ) with ‖∇Z‖₂ ≤ C ‖G‖₂ for which the weak componentwise heat equation holds against smooth tests compactly supported in Q_τ. This is the analytic core of lem:pv-stokes.