Weak gradients on time slices of the rough forced heat response #
For almost every time, the L²(Q_τ) limit of the spatial gradients of smooth
forced heat responses is the weak spatial gradient of the time slice of the
rough response. This is the slicewise weak gradient clause of the
finite-energy class used in prop:pv-local-solution.
theorem
ESS.forcedHeat_slice_weakGradient_of_approx
{τ : ℝ}
(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))
(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))
:
Slicewise weak gradients of the rough forced heat response along a smooth
approximation whose spatial gradients converge in L²(Q_τ).