Uniform derivatives of fixed and domain-adapted cutoffs

A fixed smooth compactly supported function has one numerical bound for its value, time derivative, spatial first derivatives, and spatial Laplacian. Equality of germs transports these bounds without imposing smoothness or support assumptions on the second function. In particular the negative-time bounds of a domain-adapted cutoff retain the fixed function's constants.

theorem CKN.Core.Endgame.cutoff_derivatives_eq_of_eventuallyEq {φ ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (h : φ =ᶠ[nhds z] ψ) : φ z = ψ z ∧ timePartial φ z = timePartial ψ z ∧ (∀ (i : Fin 3), spatialPartial φ i z = spatialPartial ψ i z) ∧ spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1 = spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => ψ (x, z.2)) z.1

Equality near a space-time point preserves all derivatives entering the localized heat equation, including the spatial Laplacian.

theorem CKN.Core.Endgame.exists_cutoff_derivative_bound {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : ∃ (C : ℝ), 0 < C ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |ψ z| ≤ C ∧ |timePartial ψ z| ≤ C ∧ (∀ (i : Fin 3), |spatialPartial ψ i z| ≤ C) ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => ψ (x, z.2)) z.1| ≤ C

A smooth compactly supported cutoff has a single finite numerical bound for all scalar coefficients in the localized equation.

theorem CKN.Core.Endgame.cutoff_derivative_bound_on_past_of_eventuallyEq {φ ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {C : ℝ} (hbound : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |ψ z| ≤ C ∧ |timePartial ψ z| ≤ C ∧ (∀ (i : Fin 3), |spatialPartial ψ i z| ≤ C) ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => ψ (x, z.2)) z.1| ≤ C) (hagree : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → φ =ᶠ[nhds z] ψ) (z : Foundation.Parabolic.Vec3 × ℝ) : z.2 ≤ 0 → |φ z| ≤ C ∧ |timePartial φ z| ≤ C ∧ (∀ (i : Fin 3), |spatialPartial φ i z| ≤ C) ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1| ≤ C

Negative-time germ agreement transfers a fixed numerical derivative bound, with no dependence on the domain of the adapted cutoff.