The critical and L⁴ bounds for rough tensors #
For a tensor in L^{5/2} ∩ L² supported in the slab Q_τ, the forced heat
response (the kernel formula) inherits the smooth-data bounds of
forcedHeat_smooth_estimates by Fatou's lemma along the almost everywhere
convergent smooth approximation: the L⁵ and L⁴ bounds on Q_τ and, for
almost every time, the L³ and L² slice bounds. This is the rough-data form
of eq:pv-stokes-l5 and eq:pv-stokes-l4 in lem:pv-stokes.
theorem
ESS.eLpNorm_tensor_le_sum
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
(hp : 1 ≤ p)
(T : α → Fin 3 → Fin 3 → ℝ)
(hT : ∀ (i j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (a : α) => T a i j) μ)
:
MeasureTheory.eLpNorm T p μ ≤ ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.eLpNorm (fun (a : α) => T a i j) p μ
The L^p norm of a 3 × 3 tensor field is at most the sum of the norms of
its entries.
theorem
ESS.forcedHeat_rough_bounds :
∃ (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.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 τ)))
The rough-data critical and L⁴ bounds for the forced heat response of a
tensor in L^{5/2} ∩ L² supported in Q_τ, with the absolute constant of
forcedHeat_smooth_estimates.