The weak spatial gradient of the rough forced heat response #
Along a fast smooth approximation of a tensor in L^{5/2} ∩ L² supported in
Q_τ, the spatial gradients of the smooth forced heat responses form a Cauchy
sequence in L²(Q_τ) by the energy estimate applied to differences; their limit
is the weak spatial gradient of the rough response, with the energy bound of
eq:pv-stokes-energy in lem:pv-stokes.
theorem
ESS.forcedHeat_rough_gradient :
∃ (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) →
∃ (Gs : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (DZ :
Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ),
(∀ (k : ℕ) (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p) ∧ (∀ (k : ℕ) (i j : Fin 3),
HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gs k i j p) ∧ (∀ (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}) ∧ (∀ (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)) ∧ (∀ (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 τ)))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (DZ i j) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) ∧ (∀ (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)) ∧ 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 τ)))
The L²(Q_τ) limit of the spatial gradients of smooth responses along a fast
smooth approximation of a rough tensor, with the energy bound.