The pointwise heat bound of the interior estimates

serrin_heat_pointwise_bound is the final assembly of the cut-off heat representation: it chains HB2_cutoff_decomposition into heat_pointwise_bound_of_decomposition to give |w (x, s)| ≤ C (ρ Λ + M / ρ) from the hypotheses that w = div U and (∂ₜ − Δ) w = div Y on an open set containing the backward parabolic window, with Y bounded by Λ and U bounded by M on the window. This is the pointwise heat bound of the interior estimates in the proof of lem:aniso:annulus.

theorem CIV.serrin_heat_pointwise_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (U Y : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (O : Set CKN.Foundation.Parabolic.ParabolicPoint) (x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ M : ℝ), IsOpen O → 0 < ρ → ρ ≤ 1 → {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s ⊆ O → ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => w z) O → (∀ (l : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U l z) O) → (∀ (j : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Y j z) O) → (∀ z ∈ O, w z = ∑ l : Fin 3, CKN.spatialPartial (U l) l z) → (∀ z ∈ O, CKN.timePartial w z - ∑ j : Fin 3, CKN.spatialSecondPartial w j j z = ∑ j : Fin 3, CKN.spatialPartial (Y j) j z) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s, ∀ (j : Fin 3), |Y j z| ≤ Λ) → (∀ z ∈ {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s, ∀ (l : Fin 3), |U l z| ≤ M) → |w (x, s)| ≤ C * (ρ * Λ + M / ρ)