The cut-off heat kernels of the backward windows

For a point (x, s) and a scale ρ, the backward window is B_bar(x, ρ) × [s - ρ², s]. The cutoff χ is the ball cutoff times the time cutoff; the heat weight is Ψ = Γ(x - ·, s - ·) χ, and the cutoff commutator kernel is K₀ = Γ (∂ₜχ + Δχ) + 2 ∇Γ · ∇χ. Before the time s, both kernels and their spatial partials vanish off the window. These are the kernels of the heat representation used for the interior estimates in the proof of lem:aniso:annulus.

noncomputable def CIV.serrinCutoff (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Backward parabolic cutoff at (x, s) of scale ρ.

Equations

• CIV.serrinCutoff x s ρ z = CIV.serrinBallCutoff x ρ z.1 * CIV.serrinTimeBump ((z.2 - s) / ρ ^ 2)

noncomputable def CIV.serrinHeatWeight (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The cut-off backward heat weight Ψ(z) = Γ(x - z.1, s - z.2) χ(z).

Equations

• CIV.serrinHeatWeight x s ρ z = CKN.Foundation.Heat.heatKernel (x - z.1) (s - z.2) * CIV.serrinCutoff x s ρ z

noncomputable def CIV.serrinCutoffKernel (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The cutoff-commutator kernel K₀ = Γ (∂ₜχ + Δχ) + 2 ∇_zΓ · ∇χ.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.timePartial_eq_zero_of_eventually_eq_zero {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hF : ∀ᶠ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in nhds z, F w = 0) : CKN.timePartial F z = 0

The time partial vanishes where the function vanishes on a neighbourhood.

theorem CIV.contDiff_serrinCutoff (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => serrinCutoff x s ρ z

The backward cutoff is smooth.

theorem CIV.serrinCutoff_eventually_eq_zero (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hout : z ∉ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s) (hz : z.2 < s) : ∀ᶠ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in nhds z, serrinCutoff x s ρ w = 0

Before the time s and off the window, the backward cutoff vanishes on a neighbourhood.

theorem CIV.spatialPartial_serrinKernels_eq_zero (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z.2 < s) (hout : z ∉ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s) (j : Fin 3) : CKN.spatialPartial (serrinHeatWeight x s ρ) j z = 0 ∧ CKN.spatialPartial (serrinCutoffKernel x s ρ) j z = 0

Before the time s, the spatial partials of the heat weight and of the commutator kernel vanish off the window.