Documentation

LeanPool.EscauriazaSereginSverak.PartV.HeatOrbitSolutionKernel

Kernel bounds for the heat orbit of an L² datum #

At positive times the Gaussian kernel and its spatial derivatives are square integrable, uniformly for times bounded away from zero. By the Cauchy–Schwarz inequality the heat orbit of an L² datum and the convolution of the datum with a kernel derivative are therefore bounded pointwise, Lipschitz in the datum, and jointly measurable in space and time. These are the kernel facts behind the heat-orbit clauses of prop:pv-local-solution.

source
noncomputable def ESS.heatConvGrad (t : ℝ) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) :
ℝ

Convolution of a scalar datum with the jth spatial derivative of the Gaussian kernel at time t; for t > 0 it is the classical jth derivative of the heat orbit.

Equations
Instances For
    source
    theorem ESS.heatKernel_vecTime_measurable :
    Measurable fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernel p.1 p.2

    The Gaussian kernel is jointly measurable in space and time.

    source
    theorem ESS.one_add_norm_inv_cube_memLp_two (C : ℝ) :
    MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => C * ((1 + ‖y‖) ^ 3)⁻¹) 2 MeasureTheory.volume

    The weight C (1 + |y|)⁻³ is square integrable on ℝ³.

    source
    theorem ESS.heatKernel_eLpNorm_two_uniform {δ : ℝ} (hδ : 0 < δ) :
    ∃ B < ⊤, ∀ (t : ℝ), δ ≤ t → MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) 2 MeasureTheory.volume ≤ B ∧ ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernelSpaceDerivative y t j) 2 MeasureTheory.volume ≤ B

    For times bounded away from zero, the Gaussian kernel and its spatial derivatives are bounded in L² uniformly in time.

    source
    theorem ESS.heatKernel_memLp_two {t : ℝ} (ht : 0 < t) :
    MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) 2 MeasureTheory.volume ∧ ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernelSpaceDerivative y t j) 2 MeasureTheory.volume

    At a positive time the Gaussian kernel and its spatial derivatives are square integrable.

    source
    theorem ESS.lintegral_enorm_mul_sub_le {k f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : MeasureTheory.AEStronglyMeasurable k MeasureTheory.volume) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) :
    ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ‖k y‖ₑ * ‖f (x - y)‖ₑ ≤ MeasureTheory.eLpNorm k 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

    The Cauchy–Schwarz inequality for a convolution integral at one point.

    source
    theorem ESS.integrable_mul_sub_enorm_le {k f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : MeasureTheory.MemLp k 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) :
    MeasureTheory.Integrable (fun (y : CKN.Foundation.Parabolic.Vec3) => k y * f (x - y)) MeasureTheory.volume ∧ ‖∫ (y : CKN.Foundation.Parabolic.Vec3), k y * f (x - y)‖ₑ ≤ MeasureTheory.eLpNorm k 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

    A convolution integral of two L² functions converges absolutely at every point and is bounded by the product of the L² norms.

    source
    theorem ESS.integral_mul_sub_sub_enorm_le {k f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : MeasureTheory.MemLp k 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) :
    ‖(∫ (y : CKN.Foundation.Parabolic.Vec3), k y * f (x - y)) - ∫ (y : CKN.Foundation.Parabolic.Vec3), k y * g (x - y)‖ₑ ≤ MeasureTheory.eLpNorm k 2 MeasureTheory.volume * MeasureTheory.eLpNorm (f - g) 2 MeasureTheory.volume

    The convolution integral is Lipschitz in the datum for the L² norm.

    source
    theorem ESS.stronglyMeasurable_integral_kernel_mul_sub {k : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hk : Measurable k) {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
    MeasureTheory.StronglyMeasurable fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∫ (y : CKN.Foundation.Parabolic.Vec3), k (y, z.2) * f (z.1 - y)

    A convolution integral in space whose kernel depends measurably on time is jointly strongly measurable in space and time.

    source
    theorem ESS.heatConv_heatConvGrad_bound {δ : ℝ} (hδ : 0 < δ) {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
    ∃ (M : ℝ), 0 ≤ M ∧ ∀ (t : ℝ), δ ≤ t → ∀ (x : CKN.Foundation.Parabolic.Vec3), |CKN.Foundation.Heat.heatConv t f x| ≤ M ∧ ∀ (j : Fin 3), |heatConvGrad t f j x| ≤ M

    The heat orbit of an L² datum is bounded pointwise, uniformly for times bounded away from zero, and so is its convolution with a kernel derivative.