Norm bookkeeping for the forced heat response

Conversions between the real integrals used in the smooth-data estimates of lem:pv-stokes and eLpNorm on the space-time slab Q_τ, and the identification of the forced heat response of a smooth tensor with the response vector of the energy estimates.

theorem ESS.eLpNorm_eq_ofReal_integral_rpow {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {h : α → ℝ} {r : ℝ} (hr : 0 < r) (hm : MeasureTheory.AEStronglyMeasurable h μ) (h0 : ∀ (a : α), 0 ≤ h a) (hint : MeasureTheory.Integrable (fun (a : α) => h a ^ r) μ) : MeasureTheory.eLpNorm h (ENNReal.ofReal r) μ = ENNReal.ofReal ((∫ (a : α), h a ^ r ∂μ) ^ (1 / r))

The L^r norm of a nonnegative function whose r-th power is integrable.

theorem ESS.eLpNorm_spaceTimeSet_eq_window {E : Type u_1} [NormedAddCommGroup E] (f : CKN.Foundation.Parabolic.ParabolicPoint → E) (p : ENNReal) (τ : ℝ) : MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) = MeasureTheory.eLpNorm (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => f q) p (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)))

The slab Q_τ = ℝ³ × (0,τ) carries the product of Lebesgue measure with Lebesgue measure on (0,τ].

theorem ESS.eLpNorm_eq_ofReal_of_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : CKN.Foundation.Parabolic.Vec3 × ℝ → E} (hf : Continuous f) (hfc : HasCompactSupport f) {r : ℝ} (hr : 0 < r) : MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ‖f q‖ ^ r) μ ∧ MeasureTheory.eLpNorm f (ENNReal.ofReal r) μ = ENNReal.ofReal ((∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), ‖f q‖ ^ r ∂μ) ^ (1 / r))

A continuous compactly supported function has ofReal form for its L^r norm.

theorem ESS.forcedHeat_eq_responseVec {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) (z : CKN.Foundation.Parabolic.ParabolicPoint) : forcedHeat G z = responseVec (fun (i j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) z

For a smooth compactly supported tensor, the forced heat response is the response vector of the energy estimates.

theorem ESS.spatialPartial_forcedHeat_eq {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) (i j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w i) j z = responseGrad (fun (i j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) j z i

The spatial derivatives of the forced heat response of a smooth compactly supported tensor are the response gradient of the energy estimates.

theorem ESS.norm_le_sqrt_sum_sq (v : CKN.Foundation.Parabolic.Vec3) : ‖v‖ ≤ (∑ i : Fin 3, v i ^ 2) ^ (1 / 2)

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

theorem ESS.tensor_sum_sq_le (T : Fin 3 → Fin 3 → ℝ) : ∑ i : Fin 3, ∑ j : Fin 3, T i j ^ 2 ≤ 9 * ‖T‖ ^ 2

The sum of squares of a 3 × 3 tensor is at most nine times its squared sup norm.