The zero-data forced heat estimates for smooth tensors

For a smooth compactly supported tensor G supported in positive times, the forced heat response Z = forcedHeat G satisfies on every slab Q_τ = ℝ³ × (0,τ), with an absolute constant C:

• ‖Z(t)‖₂ ≤ C ‖G‖_{L²(Q_τ)} for 0 ≤ t ≤ τ and ‖∇Z‖_{L²(Q_τ)} ≤ C ‖G‖_{L²(Q_τ)};
• ‖Z(t)‖₃ ≤ C ‖G‖_{L^{5/2}(Q_τ)} for 0 ≤ t ≤ τ and ‖Z‖_{L⁵(Q_τ)} ≤ C ‖G‖_{L^{5/2}(Q_τ)};
• ‖Z‖_{L⁴(Q_τ)} ≤ C (‖G‖_{L^{5/2}(Q_τ)} + ‖G‖_{L²(Q_τ)}).

These are the smooth-data forms of eq:pv-stokes-energy, eq:pv-stokes-l5 and eq:pv-stokes-l4 in lem:pv-stokes, for the scalar heat reformulation with the pressure folded into the tensor.

theorem ESS.tensor_window_norms {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (τ : ℝ) : ∃ (a₂ : ℝ) (a₅₂ : ℝ), 0 ≤ a₂ ∧ 0 ≤ a₅₂ ∧ MeasureTheory.eLpNorm (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => G i j p) (ENNReal.ofReal 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) = ENNReal.ofReal a₂ ∧ MeasureTheory.eLpNorm (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => G i j p) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) = ENNReal.ofReal a₅₂ ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, G i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ 9 * a₂ ^ 2 ∧ (∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), (∑ i : Fin 3, ∑ j : Fin 3, G i j p ^ 2) ^ (5 / 4) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ^ (2 / 5) ≤ 3 * a₅₂

Real forms of the L² and L^{5/2} norms of a smooth compactly supported tensor on a time window, and their comparison with the Frobenius integrals used in the smooth-data estimates.

theorem ESS.tensor_norm_le_sqrt_sum_sq (T : Fin 3 → Fin 3 → ℝ) : ‖T‖ ≤ (∑ i : Fin 3, ∑ j : Fin 3, T i j ^ 2) ^ (1 / 2)

The sup norm of a tensor is at most the square root of its sum of squares.

theorem ESS.eLpNorm_le_of_norm_le_sqrt {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {Q : α → ℝ} {r : ℝ} (hr : 0 < r) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hQm : MeasureTheory.AEStronglyMeasurable Q μ) (hQ0 : ∀ (a : α), 0 ≤ Q a) (hfQ : ∀ (a : α), ‖f a‖ ≤ Q a ^ (1 / 2)) (hint : MeasureTheory.Integrable (fun (a : α) => Q a ^ (r / 2)) μ) : MeasureTheory.eLpNorm f (ENNReal.ofReal r) μ ≤ ENNReal.ofReal ((∫ (a : α), Q a ^ (r / 2) ∂μ) ^ (1 / r))

An L^r bound from a pointwise bound by a square root: if ‖f‖ ≤ Q^{1/2} with Q ≥ 0 and Q^{r/2} integrable, then ‖f‖_r ≤ (∫ Q^{r/2})^{1/r}.

theorem ESS.forcedHeat_smooth_estimates : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) → (∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) → (∀ (i j : Fin 3), (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) → ∀ (τ : ℝ), 0 < τ → (∀ t ∈ Set.Icc 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 τ)))) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w 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 τ))) ∧ (∀ t ∈ Set.Icc 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 τ)))) ∧ 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 τ))))

The zero-data forced heat estimates for smooth compactly supported tensors supported in positive times, with an absolute constant: the smooth-data form of lem:pv-stokes for the componentwise heat reformulation.