Norm bounds for the cutoff solution and its source

The squared L²_t H^m_x norm of the cutoff ηz and the squared L²_t H^{m-1}_x norm of its source ηG + (∂ₜη - Δη) z - 2 ∇η · ∇z are bounded by the squared norms of z and G, with a factor L² for a bound L on the spatial derivatives of the cutoff (lem:local-heat-gain).

theorem ESS.integral_univ_prod_sq_eq {B K : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hIm : MeasurableSet I) (hKB : K ⊆ B) {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ K → F p = 0) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, F p ^ 2 = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, F p ^ 2

Integrals over ℝ³ × I of fields vanishing outside B × ℝ are integrals over B × I.

theorem ESS.localHeatGain_normBounds (m : ℕ) (hm1 : 1 ≤ m) : ∃ (Kc : ℝ), 0 ≤ Kc ∧ ∀ (B K : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (L : ℝ) (Dz DG : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasurableSet B → MeasurableSet I → IsLocalHeatCutoff B K η → (∀ (γ : 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) → IsSpaceTimeFamily m (B ×ˢ I) Dz → IsSpaceTimeFamily (m - 1) (B ×ˢ I) DG → ∑ α ∈ CKN.sobolevWords m, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, localHeatGainDw η Dz α p ^ 2 ≤ Kc * L ^ 2 * ∑ α ∈ CKN.sobolevWords m, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, Dz α p ^ 2 ∧ ∑ α ∈ CKN.sobolevWords (m - 1), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, localHeatGainDH η Dz DG α p ^ 2 ≤ Kc * L ^ 2 * ((∑ α ∈ CKN.sobolevWords m, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, Dz α p ^ 2) + ∑ α ∈ CKN.sobolevWords (m - 1), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, DG α p ^ 2)

The norm bounds for the cutoff solution and its source.