The heat kernel gradient against a fixed test field

For a smooth compactly supported test field ψ, the pairing K_ij(y, r) = ∫ ψ_i(x) ∂_jΓ(x - y, r) dx is, after an integration by parts, minus the heat semigroup applied to ∂_jψ_i. It is therefore bounded by a multiple of (1 + |y|)^{-3} uniformly in r, continuous in r ≠ 0, and vanishes for r ≤ 0. Without the integration by parts, the absolute pairing is bounded by r^{-1/2} (1 + |y|)^{-3}. These are the kernel estimates behind the time continuity of the forced heat response in prop:pv-local-solution.

theorem ESS.heatKernel_shift_abs_integral_le {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : Continuous φ) (hφc : HasCompactSupport φ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : CKN.Foundation.Parabolic.Vec3) (r : ℝ), 0 < r → ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Heat.heatKernel (x - y) r * |φ x| ≤ M * (1 + ‖y‖) ^ (-3)

The heat semigroup applied to |φ|, for a continuous compactly supported φ, decays like (1 + |y|)^{-3} uniformly in time.

theorem ESS.heatKernelSpaceDerivative_abs_le_doubled {z : CKN.Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (j : Fin 3) : |CKN.Foundation.Heat.heatKernelSpaceDerivative z r j| ≤ 400 * (√r)⁻¹ * CKN.Foundation.Heat.heatKernel z (2 * r)

Each spatial derivative of the heat kernel is bounded by r^{-1/2} times the heat kernel at the doubled time.

noncomputable def ESS.testKernelPairing (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (r : ℝ) : ℝ

The pairing K_ij(y, r) = ∫ ψ_i(x) ∂_jΓ(x - y, r) dx of the spatial derivative of the heat kernel, centred at y, with a component of a test field.

Equations

• ESS.testKernelPairing ψ i j y r = ∫ (x : CKN.Foundation.Parabolic.Vec3), ψ x i * CKN.Foundation.Heat.heatKernelSpaceDerivative (x - y) r j

theorem ESS.testKernelPairing_of_nonpos (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : r ≤ 0) : testKernelPairing ψ i j y r = 0

The test pairing vanishes at nonpositive times.

theorem ESS.testKernelPairing_measurable (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hψ : Continuous ψ) (i j : Fin 3) : Measurable fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => testKernelPairing ψ i j q.1 q.2

The test pairing is jointly measurable in the centre and the time.

theorem ESS.testKernelPairing_eq_neg_heatConv {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) : testKernelPairing ψ i j y r = -CKN.Foundation.Heat.heatConv r (fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (w : CKN.Foundation.Parabolic.Vec3) => ψ w i) x) (CKN.basisVec j)) y

Integration by parts: at positive times the test pairing is minus the heat semigroup applied to ∂_jψ_i.

theorem ESS.testKernelPairing_abs_le {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i j : Fin 3) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : CKN.Foundation.Parabolic.Vec3) (r : ℝ), |testKernelPairing ψ i j y r| ≤ M * (1 + ‖y‖) ^ (-3)

The test pairing is bounded by a multiple of (1 + |y|)^{-3}, uniformly in time.

theorem ESS.testKernelPairing_continuousAt {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) {r₀ : ℝ} (hr₀ : r₀ ≠ 0) : ContinuousAt (fun (r : ℝ) => testKernelPairing ψ i j y r) r₀

The test pairing is continuous in time away from r = 0.

theorem ESS.testKernelPairing_lintegral_le {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (i j : Fin 3) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : CKN.Foundation.Parabolic.Vec3) (r : ℝ), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖ψ x i * CKN.Foundation.Heat.heatKernelSpaceDerivative (x - y) r j‖ₑ ≤ ENNReal.ofReal (M * (√r)⁻¹ * (1 + ‖y‖) ^ (-3))

Without integration by parts, the absolute test pairing is bounded by r^{-1/2} (1 + |y|)^{-3}.