The integral of the derivative of the cutoff-commutator kernel

Before the time s, the spatial derivative of the commutator kernel K₀ = Γ (∂ₜχ + Δχ) + 2 ∇Γ · ∇χ is bounded by C ρ⁻⁶ and supported in the window, so its integral is of size ρ⁻¹. This is the cutoff term of the pointwise heat bound in the interior estimates of the proof of lem:aniso:annulus.

theorem CIV.norm_iteratedFDeriv_fderiv_apply_le {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (v : CKN.Foundation.Parabolic.Vec3) (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3) : ‖iteratedFDeriv ℝ n (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ g y') v) y‖ ≤ ‖v‖ * ‖iteratedFDeriv ℝ (n + 1) g y‖

A directional derivative of a smooth function costs one order of its iterated derivative.

theorem CIV.abs_dir_deriv_le {B : CKN.Foundation.Parabolic.Vec3 → ℝ} (hB : ContDiff ℝ (↑⊤) B) (y : CKN.Foundation.Parabolic.Vec3) (i l m : Fin 3) : |(fderiv ℝ B y) (CKN.basisVec i)| ≤ ‖iteratedFDeriv ℝ 1 B y‖ ∧ |(fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ B y') (CKN.basisVec i)) y) (CKN.basisVec l)| ≤ ‖iteratedFDeriv ℝ 2 B y‖ ∧ |(fderiv ℝ (fun (y'' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ B y') (CKN.basisVec i)) y'') (CKN.basisVec l)) y) (CKN.basisVec m)| ≤ ‖iteratedFDeriv ℝ 3 B y‖

Iterated directional derivatives along unit basis vectors are bounded by the iterated derivative of the same order.

theorem CIV.spatialPartial_separated {B : CKN.Foundation.Parabolic.Vec3 → ℝ} (hB : Differentiable ℝ B) (T : ℝ → ℝ) (i : Fin 3) : (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => B w.1 * T w.2) i z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (fderiv ℝ B z.1) (CKN.basisVec i) * T z.2

The spatial partial of a separated product B(y) T(τ).

theorem CIV.timePartial_separated (B : CKN.Foundation.Parabolic.Vec3 → ℝ) {T : ℝ → ℝ} (hT : Differentiable ℝ T) : (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => B w.1 * T w.2) z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => B z.1 * deriv T z.2

The time partial of a separated product B(y) T(τ).

theorem CIV.fderiv_apply_eq_zero_of_eqOn_const {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {O : Set CKN.Foundation.Parabolic.Vec3} (hO : IsOpen O) {c : ℝ} (hg : ∀ y ∈ O, g y = c) (v y : CKN.Foundation.Parabolic.Vec3) : y ∈ O → (fderiv ℝ g y) v = 0

The directional derivative vanishes on an open set where the function is constant.

noncomputable def CIV.serrinTimeCut (s ρ r : ℝ) : ℝ

The time profile of the backward cutoff.

Equations

• CIV.serrinTimeCut s ρ r = CIV.serrinTimeBump ((r - s) / ρ ^ 2)

theorem CIV.serrinCutoff_eq_separated (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ) : serrinCutoff x s ρ = fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ w.1 * serrinTimeCut s ρ w.2

The backward cutoff is the ball cutoff times the time profile.

theorem CIV.contDiff_serrinTimeCut (s ρ : ℝ) : ContDiff ℝ (↑⊤) (serrinTimeCut s ρ)

The time profile is smooth.

theorem CIV.serrinTimeCut_bounds : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s ρ : ℝ), 0 < ρ → ∀ (r : ℝ), |serrinTimeCut s ρ r| ≤ 1 ∧ |deriv (serrinTimeCut s ρ) r| ≤ C / ρ ^ 2 ∧ (s - ρ ^ 2 / 2 < r → deriv (serrinTimeCut s ρ) r = 0)

Bounds for the time profile and its derivative, and the vanishing of the derivative after s - ρ²/2.

theorem CIV.serrinBallCutoff_dir_bounds : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ), 0 < ρ → ∀ (y : CKN.Foundation.Parabolic.Vec3) (i l m : Fin 3), |serrinBallCutoff x ρ y| ≤ 1 ∧ |(fderiv ℝ (serrinBallCutoff x ρ) y) (CKN.basisVec i)| ≤ C / ρ ∧ |(fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y') (CKN.basisVec i)) y) (CKN.basisVec l)| ≤ C / ρ ^ 2 ∧ |(fderiv ℝ (fun (y'' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y') (CKN.basisVec i)) y'') (CKN.basisVec l)) y) (CKN.basisVec m)| ≤ C / ρ ^ 3 ∧ (CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) < ρ / 2 → (fderiv ℝ (serrinBallCutoff x ρ) y) (CKN.basisVec i) = 0 ∧ (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y') (CKN.basisVec i)) y) (CKN.basisVec l) = 0 ∧ (fderiv ℝ (fun (y'' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y') (CKN.basisVec i)) y'') (CKN.basisVec l)) y) (CKN.basisVec m) = 0)

Bounds for the ball cutoff and its first three directional derivatives, and their vanishing on the inner half ball.

theorem CIV.spatialPartial_heatKernel_translate (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.2 < s) (i : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Heat.heatKernel (x - w.1) (s - w.2)) i z = -CKN.Foundation.Heat.heatKernelSpaceDerivative (x - z.1) (s - z.2) i

The spatial partial of the translated heat kernel before the pole.

theorem CIV.fderiv_heatKernelSpaceDerivative_apply {t : ℝ} (ht : 0 < t) (y₀ : CKN.Foundation.Parabolic.Vec3) (i l : Fin 3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernelSpaceDerivative y t i) y₀) (CKN.basisVec l) = -CKN.basisVec l i / (2 * t) * CKN.Foundation.Heat.heatKernel y₀ t + -y₀ i / (2 * t) * CKN.Foundation.Heat.heatKernelSpaceDerivative y₀ t l

The directional derivative of the space derivative of the heat kernel.

theorem CIV.heatKernel_window_bounds : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ρ : ℝ), 0 < ρ → ∀ (y : CKN.Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → t ≤ ρ ^ 2 → CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ ρ → ρ / 2 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∨ ρ ^ 2 / 2 ≤ t → CKN.Foundation.Heat.heatKernel y t ≤ C / ρ ^ 3 ∧ (∀ (i : Fin 3), |CKN.Foundation.Heat.heatKernelSpaceDerivative y t i| ≤ C / ρ ^ 4) ∧ ∀ (i l : Fin 3), |(fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernelSpaceDerivative y' t i) y) (CKN.basisVec l)| ≤ C / ρ ^ 5

In the region of the window away from the pole, the heat kernel and its first two spatial derivatives have the parabolic sizes ρ⁻³, ρ⁻⁴, ρ⁻⁵.

theorem CIV.contDiff_heatKernelSpaceDerivative {t : ℝ} (ht : 0 < t) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernelSpaceDerivative y t i

The space derivative of the heat kernel is smooth in space at positive times.

theorem CIV.contDiff_heatKernel_space {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t

The heat kernel is smooth in space at positive times.

theorem CIV.fderiv_comp_sub_left_apply {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (x y : CKN.Foundation.Parabolic.Vec3) (hg : DifferentiableAt ℝ g (x - y)) (v : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => g (x - y')) y) v = -(fderiv ℝ g (x - y)) v

The directional derivative of y ↦ g (x - y) is minus the directional derivative of g.

theorem CIV.serrinCutoff_partials (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) : ((fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial (serrinCutoff x s ρ) z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1 * deriv (serrinTimeCut s ρ) z.2) ∧ ((fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinCutoff x s ρ) i z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (fderiv ℝ (serrinBallCutoff x ρ) z.1) (CKN.basisVec i) * serrinTimeCut s ρ z.2) ∧ (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialSecondPartial (serrinCutoff x s ρ) i i z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y) (CKN.basisVec i)) z.1) (CKN.basisVec i) * serrinTimeCut s ρ z.2

The partials of the backward cutoff, in separated form.

theorem CIV.spatialPartial_serrinCutoffKernel_eq_fderiv (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.2 < s) (l : Fin 3) : CKN.spatialPartial (serrinCutoffKernel x s ρ) l z = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel (x - y) (s - z.2) * (serrinBallCutoff x ρ y * deriv (serrinTimeCut s ρ) z.2 + (∑ i : Fin 3, (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (serrinBallCutoff x ρ) y') (CKN.basisVec i)) y) (CKN.basisVec i)) * serrinTimeCut s ρ z.2) + 2 * ∑ i : Fin 3, -CKN.Foundation.Heat.heatKernelSpaceDerivative (x - y) (s - z.2) i * ((fderiv ℝ (serrinBallCutoff x ρ) y) (CKN.basisVec i) * serrinTimeCut s ρ z.2)) z.1) (CKN.basisVec l)

Before the time s, the slice of the commutator kernel is an explicit smooth function of the space variable.

theorem CIV.abs_spatialPartial_serrinCutoffKernel_le : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ), 0 < ρ → ∀ (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 → ∀ (l : Fin 3), |CKN.spatialPartial (serrinCutoffKernel x s ρ) l z| ≤ C / ρ ^ 6

Pointwise bound for the spatial derivative of the commutator kernel in the window.

theorem CIV.contDiffOn_serrinCutoffKernel (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => serrinCutoffKernel x s ρ z) (CKN.spaceTimeSet Set.univ (Set.Iio s))

The commutator kernel is smooth before the time s.

theorem CIV.serrinCutoffKernel_spatialPartial_integral : ∃ (C : ℝ), 0 < C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ), 0 < ρ → ρ ≤ 1 → ∀ (l : Fin 3), MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinCutoffKernel x s ρ) l z) {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s} MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s}, |CKN.spatialPartial (serrinCutoffKernel x s ρ) l z| ≤ C / ρ

The spatial derivative of the commutator kernel is integrable before the time s, with integral of size ρ⁻¹.