The space-time cutoffs of lem:local-heat-gain #
For concentric balls B_r ⋐ B_R and a time gap σ > 0, the separated cutoff
η(x, t) = θ(t - a) χ(x - x₀) equals one on B_r × [a + σ, ∞), vanishes for
t < a + σ/2 and for x outside a compact subset of B_R, and its spatial
derivatives, those of ∂ₜη - Δη and those of ∇η are bounded through any
fixed order by a constant independent of the center x₀ and of a.
theorem
ESS.wordDeriv_eq_zero_of_eqOn
{W : Set CKN.Foundation.Parabolic.Vec3}
(hW : IsOpen W)
{g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hg : ∀ y ∈ W, g y = 0)
(γ : List (Fin 3))
(y : CKN.Foundation.Parabolic.Vec3)
:
y ∈ W → CKN.wordDeriv γ g y = 0
Word derivatives vanish on an open set where the function vanishes.
theorem
ESS.wordDeriv_eq_zero_of_eqOn_one
{W : Set CKN.Foundation.Parabolic.Vec3}
(hW : IsOpen W)
{g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hg : ∀ y ∈ W, g y = 1)
(γ : List (Fin 3))
(hγ : γ ≠ [])
(y : CKN.Foundation.Parabolic.Vec3)
:
y ∈ W → CKN.wordDeriv γ g y = 0
Word derivatives of positive length vanish on an open set where the function is constant one.
theorem
ESS.localHeatGain_cutoffs
(m : ℕ)
{r R σ : ℝ}
(hr : 0 < r)
(hrR : r < R)
(hσ : 0 < σ)
:
∃ (L : ℝ),
0 ≤ L ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a : ℝ),
∃ (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (K : Set CKN.Foundation.Parabolic.Vec3) (N :
Set CKN.Foundation.Parabolic.Vec3) (κ : CKN.Foundation.Parabolic.Vec3 → ℝ),
IsLocalHeatCutoff (CKN.Foundation.Parabolic.vec3Ball x₀ R) K η ∧ IsOpen N ∧ K ⊆ N ∧ ContDiff ℝ (↑⊤) κ ∧ HasCompactSupport κ ∧ tsupport κ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ R ∧ (∀ x ∈ N, κ x = 1) ∧ (∀ (γ : List (Fin 3)),
γ.length ≤ m → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ η p| ≤ L) ∧ (∀ (γ : List (Fin 3)),
γ.length ≤ m →
∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ),
|spaceTimeWord γ (localHeatGainZeta η) p| ≤ L) ∧ (∀ (j : Fin 3) (γ : List (Fin 3)),
γ.length ≤ m →
∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ),
|spaceTimeWord γ
(fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial η j q) p| ≤ L) ∧ (∀ (γ : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ),
p.2 ≤ a + σ / 2 → spaceTimeWord γ η p = 0) ∧ ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ),
p.1 ∈ CKN.Foundation.Parabolic.vec3Ball x₀ r →
a + σ ≤ p.2 →
spaceTimeWord [] η p = 1 ∧ ∀ (γ : List (Fin 3)), γ ≠ [] → spaceTimeWord γ η p = 0
The cutoffs of lem:local-heat-gain.