Interior gradient bounds for the heat operator and the Laplacian

From the pointwise heat-potential bound of the Serrin estimates, applied to ∂_l v written as a divergence, one spatial derivative is gained on a backward window with the scaling C (ρ sup |∂_t v - Δv| + sup |v| / ρ). Freezing time gives the same bound for the Laplacian on a ball. These are the only analytic estimates in the derivative induction of thm:analytic:interior; the pressure is handled at every order by the second one.

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

Interior gradient bound for the heat operator: on a backward window B_bar(x, ρ) × [s - ρ², s] with ρ ≤ 1, |∂_l v(x, s)| ≤ C (ρ sup |∂_t v - Δv| + sup |v| / ρ).

theorem CIV.laplace_gradient_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (P : CKN.Foundation.Parabolic.Vec3 → ℝ) (Ω : Set CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (ρ Λ M : ℝ), IsOpen Ω → 0 < ρ → ρ ≤ 1 → {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ⊆ Ω → ContDiffOn ℝ (↑⊤) P Ω → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → |∑ j : Fin 3, axisDeriv j (axisDeriv j P) y| ≤ Λ) → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → |P y| ≤ M) → ∀ (l : Fin 3), |axisDeriv l P x| ≤ C * (ρ * Λ + M / ρ)

Interior gradient bound for the Laplacian on a closed ball B_bar(x, ρ), ρ ≤ 1: |∂_l P(x)| ≤ C (ρ sup |ΔP| + sup |P| / ρ).