Interior Sup Smooth Bound Support

Supporting estimates for the Navier–Stokes development.

theorem CKN.Foundation.Heat.smooth_harmonic_annular_representation_on_tsupport {H : Parabolic.Vec3 → ℝ} (hH : ContDiff ℝ (↑⊤) H) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hHarm : ∀ y ∈ tsupport (mollifiedBallCutoff x₀ hρ), spatialLaplacian H y = 0) {x : Parabolic.Vec3} (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) : H x = (-∫ (y : Parabolic.Vec3), newtonianKernel (x - y) * (H y * spatialLaplacian (mollifiedBallCutoff x₀ hρ) y)) + 2 * ∑ i : Fin 3, ∫ (y : Parabolic.Vec3), H y * spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y

Represents a smooth harmonic function on the support of a cutoff by its Newtonian source and boundary terms.

theorem CKN.Foundation.Heat.exists_smooth_cutoff_one_near_compact {K U : Set Parabolic.Vec3} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (ξ : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ξ ∧ HasCompactSupport ξ ∧ (∀ (x : Parabolic.Vec3), 0 ≤ ξ x ∧ ξ x ≤ 1) ∧ tsupport ξ ⊆ U ∧ ∃ (W : Set Parabolic.Vec3), IsOpen W ∧ K ⊆ W ∧ W ⊆ U ∧ ∀ x ∈ W, ξ x = 1

Produces a smooth compactly supported cutoff equal to one near a compact set.

theorem CKN.Foundation.Heat.cutoff_annulus_norm_distance_for_three_quarters {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (3 * ρ / 4)) {y : Parabolic.Vec3} (hy : y ∈ cutoffAnnulus x₀ (4 * ρ / 3)) : ρ / 30 < ‖x - y‖

Bounds the cutoff annulus away from the three-quarter ball.

theorem CKN.Foundation.Heat.source_kernel_bound_scaled_three_quarters {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (3 * ρ / 4)) {y : Parabolic.Vec3} (hy : y ∈ cutoffAnnulus x₀ (4 * ρ / 3)) : |newtonianKernel (x - y) * spatialLaplacian (eta x₀ ⋯) y| ≤ harmonicInteriorSourceConstant * (ρ ^ 3)⁻¹

Bounds the Newtonian source kernel at the three-quarter scale.

theorem CKN.Foundation.Heat.kernel_cutoff_derivative_bound_scaled_three_quarters {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (3 * ρ / 4)) {y : Parabolic.Vec3} (hy : y ∈ cutoffAnnulus x₀ (4 * ρ / 3)) (i j : Fin 3) : |spatialDeriv (kernelCutoffDerivative x x₀ ⋯ i) j y| ≤ harmonicInteriorGradientConstant * (ρ ^ 3)⁻¹

Bounds the differentiated cutoff kernel at the three-quarter scale.

theorem CKN.Foundation.Heat.kernel_cutoff_derivative_zero_off_annulus_three_quarters {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (3 * ρ / 4)) {y : Parabolic.Vec3} (hy : y ∉ cutoffAnnulus x₀ (4 * ρ / 3)) (i j : Fin 3) : spatialDeriv (kernelCutoffDerivative x x₀ ⋯ i) j y = 0

The differentiated cutoff kernel vanishes outside its annular support.

theorem CKN.Foundation.Heat.spatialLaplacian_eq_of_eqOn_open {f g : Parabolic.Vec3 → ℝ} {U W : Set Parabolic.Vec3} (hU : IsOpen U) (hW : IsOpen W) (hWU : W ⊆ U) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiffOn ℝ (↑⊤) g U) (hfg : ∀ x ∈ W, f x = g x) (x : Parabolic.Vec3) : x ∈ W → spatialLaplacian f x = spatialLaplacian g x

Equality on an open set transfers the spatial Laplacian there for smooth functions.