Derivatives on the Gaussian cutoff plateau

The spatial factor is constant on the inner ball, and both time factors are constant away from their transition intervals.

theorem ESS.ucSpatialCutoff_spatialPartial_zero_on_inner {ρ : ℝ} (hρ : 0 < ρ) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 (ρ / 2)) (j : Fin 3) (s : ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) j (x, s) = 0

The first spatial derivative of the ball cutoff vanishes on its inner plateau.

theorem ESS.ucSpatialCutoff_spatialSecondPartial_zero_on_inner {ρ : ℝ} (hρ : 0 < ρ) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 (ρ / 2)) (j k : Fin 3) (s : ℝ) : CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) j k (x, s) = 0

The second spatial derivative of the ball cutoff vanishes on its inner plateau.

theorem ESS.ucGaussianCutoff_spatialPartial_zero_on_inner {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (j : Fin 3) : CKN.spatialPartial (ucGaussianCutoff ρ hρ ε) j z = 0

The Gaussian cutoff has no first spatial derivative on the inner ball.

theorem ESS.ucGaussianCutoff_spatialSecondPartial_zero_on_inner {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (j k : Fin 3) : CKN.spatialSecondPartial (ucGaussianCutoff ρ hρ ε) j k z = 0

The Gaussian cutoff has no second spatial derivative on the inner ball.

theorem ESS.ucFinalTimeCutoff_deriv_zero {s : ℝ} (hs : s < 3 / 2) : deriv ucFinalTimeCutoff s = 0

The final-time factor has zero derivative before its transition.

theorem ESS.ucInitialTimeCutoff_deriv_zero {ε s : ℝ} (hε : 0 < ε) (hs : 2 * ε < s) : deriv (ucInitialTimeCutoff ε) s = 0

The initial-time factor has zero derivative after its transition.

theorem ESS.ucGaussianCutoff_timePartial_zero_on_inner_late {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (hlate : 2 * ε < z.2) : CKN.timePartial (ucGaussianCutoff ρ hρ ε) z = 0

Away from the initial transition, the Gaussian cutoff has zero time derivative on the inner region.