The energy-level space-time bound for smooth heat data

For smooth compactly supported data the heat energy bound and the Gagliardo–Nirenberg inequality eq:gn-ten-thirds of the CKN manuscript, applied at each time, give ‖S(·)b‖_{L^{10/3}(Q_τ)} ≤ C ‖b‖₂ with C independent of τ. This is the L² input of the second estimate in lem:pv-heat-critical.

theorem ESS.heatConvVec3SmoothExt_of_pos {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (x : CKN.Foundation.Parabolic.Vec3) : heatConvVec3SmoothExt b t x = heatConvVec3 t b x

On positive times the extended smooth heat orbit is the heat orbit.

theorem ESS.heatOrbit_aestronglyMeasurable_smooth {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (τ : ℝ) : MeasureTheory.AEStronglyMeasurable (heatOrbit b) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))

The heat orbit of smooth compact data is almost everywhere strongly measurable on every slab of positive times, as used in lem:pv-heat-critical.

theorem ESS.lintegral_spaceTimeSet_univ_eq {I : Set ℝ} {F : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal} (hF : AEMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ I, F z = ∫⁻ (t : ℝ) in I, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), F (x, t)

Tonelli on a slab ℝ³ × I: the space-time integral is the time integral of the spatial integrals.

theorem ESS.eLpNorm_two_rpow_two_eq_ofReal_integral {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ 2 = ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2)

The squared L² norm of a square-integrable real function is the extended real of its square integral.

noncomputable def ESS.heatComponentH1 {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {t : ℝ} (ht : 0 < t) (i : Fin 3) : CKN.H1Function Set.univ

The H¹ slice of one component of a smooth compact heat orbit.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.eLpNorm_ofReal_le_of_lintegral_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p : ℝ} (hp : 0 < p) (hf : MeasureTheory.AEStronglyMeasurable f μ) {K Y : ENNReal} (h : ∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ ≤ K * Y ^ p) : MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ ≤ K ^ (1 / p) * Y

A bound on the p-th power integral converts into an Lᵖ bound.

theorem ESS.heatComponent_tenThirds_slice {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {t : ℝ} (ht : 0 < t) (i : Fin 3) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖heatConvVec3 t b x i‖ₑ ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant ^ 2 * ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), heatConvVec3 t b x i ^ 2) ^ (2 / 3) * ENNReal.ofReal (∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x ^ 2)

The Gagliardo–Nirenberg inequality eq:gn-ten-thirds of the CKN manuscript for one component of a smooth compact heat orbit at a positive time.

theorem ESS.lintegral_enorm_rpow_eq_eLpNorm_rpow {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p : ℝ} (hp : 0 < p) (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ = MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ ^ p

The extended power integral is the corresponding power of the Lᵖ norm.

theorem ESS.ofReal_integral_sum_sq_le_eLpNorm_two {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) : ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2) ≤ 3 * MeasureTheory.eLpNorm b 2 MeasureTheory.volume ^ 2

The sum of squared components of a smooth compact field is bounded by three times the squared L² norm.

theorem ESS.heatOrbit_tenThirds_lintegral_smooth {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {τ : ℝ} (hτ : 0 < τ) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), ‖heatOrbit b z‖ₑ ^ (10 / 3) ≤ 3 * CKN.gagliardoNirenbergSobolevConstant ^ 2 * ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2) ^ (5 / 3)

The energy-level space-time bound for smooth compact data: the L^{10/3}(Q_τ) integral is controlled by the initial energy, uniformly in τ, as used in lem:pv-heat-critical.

theorem ESS.heatOrbit_tenThirds_smooth : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) → (∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) → ∀ (τ : ℝ), 0 < τ → MeasureTheory.eLpNorm (heatOrbit b) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm b 2 MeasureTheory.volume

The energy-level space-time estimate ‖S(·)b‖_{L^{10/3}(Q_τ)} ≤ C‖b‖₂ for smooth compact data, with C independent of τ, as used in lem:pv-heat-critical.