The pointwise heat bound from the cut-off representation #
If w(x, s) is given by the cut-off heat representation, with the flux Y bounded by Λ and
the potential U bounded by M on the backward window, then |w(x, s)| ≤ C (ρΛ + M/ρ): the
main term gains the factor ρ from the integral of the kernel gradient and the cutoff term costs
ρ⁻¹. This is the final step of the pointwise heat bound of the interior estimates in the proof
of lem:aniso:annulus.
theorem
CIV.abs_integral_kernel_mul_le
{K F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{x : CKN.Foundation.Parabolic.Vec3}
{s ρ Λ : ℝ}
(hK :
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => K z)
{z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s} MeasureTheory.volume)
(hsupp :
∀ (z : CKN.Foundation.Parabolic.ParabolicPoint),
z.2 < s →
z ∉
{y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s →
K z = 0)
(hF :
∀
z ∈
{y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s,
|F z| ≤ Λ)
:
A kernel supported in the window, integrable before s, against a function bounded by Λ
on the window.
theorem
CIV.heat_pointwise_bound_of_decomposition :
∃ (C : ℝ),
0 < C ∧ ∀ (w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (U Y : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ M : ℝ),
0 < ρ →
ρ ≤ 1 →
(∀
z ∈
{y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s,
∀ (j : Fin 3), |Y j z| ≤ Λ) →
(∀
z ∈
{y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s,
∀ (l : Fin 3), |U l z| ≤ M) →
w (x, s) = (-∑ j : Fin 3,
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s}, CKN.spatialPartial (serrinHeatWeight x s ρ) j z * Y j z) - ∑ l : Fin 3,
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s}, U l z * CKN.spatialPartial (serrinCutoffKernel x s ρ) l z →
|w (x, s)| ≤ C * (ρ * Λ + M / ρ)
The pointwise heat bound, given the cut-off heat representation of w(x, s).