A weighted L¹ bound for the spatial-gradient heat kernel

On a slab ℝ³ × (0,τ), the kernel ∂_j W₊ restricted to (0,τ) is integrable, and against the weight (1 + ‖x‖)^{-2} its convolution with a source in L² supported in (0,τ) is bounded in L¹ by the L² norm of the source. This identifies limits of forced heat responses of smooth approximants with the kernel formula of lem:pv-stokes for rough tensors.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_2 : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def ESS.forcedHeatWeight (x : CKN.Foundation.Parabolic.Vec3) : ℝ

The spatial weight (1 + ‖x‖)^{-2} used to localize the rough forced heat response.

Equations

• ESS.forcedHeatWeight x = ((1 + ‖x‖) ^ 2)⁻¹

theorem ESS.forcedHeatWeight_pos (x : CKN.Foundation.Parabolic.Vec3) : 0 < forcedHeatWeight x

theorem ESS.forcedHeatWeight_continuous : Continuous forcedHeatWeight

theorem ESS.forcedHeatWeight_sq_lintegral_lt_top (τ : ℝ) : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 τ, ENNReal.ofReal (forcedHeatWeight z.1) ^ 2 < ⊤

The squared weight has finite integral over the slab.

theorem ESS.heatKernelSpaceDerivative_window_lintegral_lt_top {τ : ℝ} (hτ : 0 < τ) (j : Fin 3) : ∫⁻ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioc 0 τ, ‖CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j‖ₑ < ⊤

The kernel ∂_j W₊ has finite mass on ℝ³ × (0,τ].

theorem ESS.kernel_weighted_lintegral_le {τ : ℝ} (hτ : 0 < τ) (j : Fin 3) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (H : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.AEStronglyMeasurable H MeasureTheory.volume → (∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), H z ≠ 0 → 0 < z.2) → ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 τ, ENNReal.ofReal (forcedHeatWeight z.1) * ∫⁻ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ‖CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * H (z - p)‖ₑ ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm H 2 MeasureTheory.volume

The weighted L¹ bound: for a source H ∈ L² vanishing at nonpositive times, ∫_{ℝ³×(0,τ)} w(x) ∫ |∂_j W₊(p) H(z - p)| dp dz ≤ C ‖H‖₂ with C depending only on τ.