Separated cutoffs and their spatial derivatives

For a separated field c(t) g(x - x₀) with g smooth, the spatial word derivatives are c(t) (∂^γ g)(x - x₀). For compactly supported g and bounded c they are bounded independently of the center x₀ and of c beyond its bound. These are the cutoff bounds of lem:local-heat-gain.

theorem ESS.spatialPartial_separated {c : ℝ → ℝ} {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : Differentiable ℝ g) (x₀ : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c q.2 * g (q.1 - x₀)) j p = c p.2 * CKN.spatialDeriv g j (p.1 - x₀)

theorem ESS.spaceTimeWord_separated (γ : List (Fin 3)) (c : ℝ → ℝ) {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (x₀ : CKN.Foundation.Parabolic.Vec3) : (spaceTimeWord γ fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c q.2 * g (q.1 - x₀)) = fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c p.2 * CKN.wordDeriv γ g (p.1 - x₀)

Spatial word derivatives of separated fields.

theorem ESS.contDiff_wordDeriv_of_contDiff {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (γ : List (Fin 3)) : ContDiff ℝ (↑⊤) (CKN.wordDeriv γ g)

theorem ESS.hasCompactSupport_wordDeriv {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hgc : HasCompactSupport g) (γ : List (Fin 3)) : HasCompactSupport (CKN.wordDeriv γ g)

theorem ESS.spaceTimeWord_separated_bound {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (Cc : ℝ) (γ : List (Fin 3)) : ∃ (L : ℝ), ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (c : ℝ → ℝ), (∀ (t : ℝ), |c t| ≤ Cc) → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c q.2 * g (q.1 - x₀)) p| ≤ L

Word derivatives of separated fields with compactly supported spatial factor are bounded uniformly in the center and in the time factor.