The cutoff solution and its derivative families

For a local solution z of ∂ₜ z - Δ z = G on B × I with derivative families Dz and DG, and a smooth cutoff η vanishing for x outside a compact subset of B, the cutoff w = ηz and its source H = ηG + (∂ₜη - Δη) z - 2 ∇η · ∇z have explicit Leibniz derivative families localHeatGainDw and localHeatGainDH on ℝ³ × I, and w solves ∂ₜ w - Δ w = H there (lem:local-heat-gain).

noncomputable def ESS.localHeatGainZeta (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The multiplier ∂ₜη - Δη.

Equations

• ESS.localHeatGainZeta η p = CKN.timePartial η p - ∑ k : Fin 3, CKN.spatialSecondPartial η k k p

noncomputable def ESS.localHeatGainDw (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dz : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The derivative family of the cutoff ηz.

Equations

• ESS.localHeatGainDw η Dz α = ESS.stLeibniz α (fun (γ : List (Fin 3)) => ESS.spaceTimeWord γ η) Dz

noncomputable def ESS.localHeatGainDH (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dz DG : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The derivative family of the source ηG + (∂ₜη - Δη) z - 2 ∇η · ∇z.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.isSpaceTimeFamily_zero (n : ℕ) (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) : IsSpaceTimeFamily n V fun (x : List (Fin 3)) (x_1 : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0

The zero family.

theorem ESS.IsSpaceTimeFamily.finset_sum {ι : Type u_1} (s : Finset ι) {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : ι → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : ∀ i ∈ s, IsSpaceTimeFamily n V (B i)) : IsSpaceTimeFamily n V fun (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i ∈ s, B i α p

Finite sums of space-time derivative families.

structure ESS.IsLocalHeatCutoff (B K : Set CKN.Foundation.Parabolic.Vec3) (η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

The hypotheses on a cutoff: smoothness, compact spatial support inside B, and all spatial word derivatives of η, ∂ₜη - Δη and ∂_j η bounded.

• smooth : ContDiff ℝ (↑⊤) η
• compact : IsCompact K
• subset : K ⊆ B
• zero (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), η (x, t) = 0
• bound (γ : List (Fin 3)) : ∃ (L : ℝ), ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ η p| ≤ L
• boundZeta (γ : List (Fin 3)) : ∃ (L : ℝ), ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ (localHeatGainZeta η) p| ≤ L
• boundGrad (j : Fin 3) (γ : List (Fin 3)) : ∃ (L : ℝ), ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial η j q) p| ≤ L

theorem ESS.IsLocalHeatCutoff.smooth_zeta {B K : Set CKN.Foundation.Parabolic.Vec3} {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsLocalHeatCutoff B K η) : ContDiff ℝ (↑⊤) (localHeatGainZeta η)

theorem ESS.IsLocalHeatCutoff.smooth_grad {B K : Set CKN.Foundation.Parabolic.Vec3} {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsLocalHeatCutoff B K η) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial η j q

theorem ESS.IsLocalHeatCutoff.zeta_zero {B K : Set CKN.Foundation.Parabolic.Vec3} {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsLocalHeatCutoff B K η) (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), localHeatGainZeta η (x, t) = 0

theorem ESS.IsLocalHeatCutoff.grad_zero {B K : Set CKN.Foundation.Parabolic.Vec3} {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsLocalHeatCutoff B K η) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), CKN.spatialPartial η j (x, t) = 0

theorem ESS.localHeatGain_families {m : ℕ} (hm1 : 1 ≤ m) {B K N : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hBm : MeasurableSet B) (hIm : MeasurableSet I) {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hη : IsLocalHeatCutoff B K η) (hN : IsOpen N) (hKN : K ⊆ N) {κ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hκB : tsupport κ ⊆ B) (hκN : ∀ x ∈ N, κ x = 1) {Dz DG : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hDz : IsSpaceTimeFamily m (B ×ˢ I) Dz) (hDG : IsSpaceTimeFamily (m - 1) (B ×ˢ I) DG) : IsSpaceTimeFamily m (Set.univ ×ˢ I) (localHeatGainDw η Dz) ∧ IsSpaceTimeFamily (m - 1) (Set.univ ×ˢ I) (localHeatGainDH η Dz DG) ∧ (∀ (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ K → localHeatGainDw η Dz α p = 0) ∧ ∀ (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ K → localHeatGainDH η Dz DG α p = 0

The families of the cutoff solution and of its source.

theorem ESS.localHeatGain_heat {B K : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hIm : MeasurableSet I) {η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hη : IsLocalHeatCutoff B K η) {m : ℕ} (hm1 : 1 ≤ m) {Dz DG : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hDz : IsSpaceTimeFamily m (B ×ˢ I) Dz) (hDG : IsSpaceTimeFamily (m - 1) (B ×ˢ I) DG) (hheat : CKN.IsHeatSolutionOn B I (Dz []) (DG [])) : CKN.IsHeatSolutionOn Set.univ I (localHeatGainDw η Dz []) (localHeatGainDH η Dz DG [])

The heat equation for the cutoff solution.