The rough forced heat response in the finite-energy class

For a tensor G ∈ L^{5/2} ∩ L² supported in the slab ℝ³ × (0, τ), the forced heat response Z = forcedHeat G has square integrable time slices with a uniform bound, lies in L² of the slab, and has a spatial gradient DZ ∈ L² of the slab which is the weak gradient of almost every time slice and with which Z solves ∂_t Z_i - ΔZ_i = ∑_j ∂_j G_ij weakly. These are the properties of the forced part of the Duhamel fixed point used in prop:pv-local-solution.

theorem ESS.memLp_two_iff_lintegral_enorm_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.MemLp f 2 μ ↔ ∫⁻ (x : α), ‖f x‖ₑ ^ 2 ∂μ < ⊤

Square integrability in terms of the integral of the squared norm.

theorem ESS.forcedHeat_rough_slice_energy {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG52 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) (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) : ∃ (K : ENNReal), K ≠ ⊤ ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => forcedHeat G (x, t)) 2 MeasureTheory.volume ∧ ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖forcedHeat G (x, t)‖ₑ ^ 2 ≤ K

The time slices of the rough forced heat response are square integrable, with a bound uniform in almost every time of the slab.

theorem ESS.forcedHeat_rough_memLp_two {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG52 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) (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) : MeasureTheory.MemLp (forcedHeat G) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))

The rough forced heat response is square integrable on the slab.

theorem ESS.forcedHeat_rough_solution {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG52 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) (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) : ∃ (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 τ)))) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 τ), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => forcedHeat G (x, s) i) fun (x : CKN.Vec 3) (j : Fin 3) => DZ i j (x, s)) ∧ ∀ (φ : 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 : 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 rough forced heat response has a square integrable spatial gradient on the slab, which is the weak gradient of almost every time slice, and with which it solves ∂_t Z_i - ΔZ_i = ∑_j ∂_j G_ij weakly on the slab.