Interior Estimates Basic

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Heat.eta_spatialDeriv_bound_global (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : Parabolic.Vec3) (i : Fin 3) : |spatialDeriv (eta x₀ hρ) i y| ≤ cutoffGradientConstant / ρ

theorem CKN.Foundation.Heat.eta_spatialSecond_bound_global (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : Parabolic.Vec3) (i j : Fin 3) : |spatialDeriv (spatialDeriv (eta x₀ hρ) i) j y| ≤ cutoffSecondDerivativeConstant / ρ ^ 2

def CKN.Foundation.Heat.cutoffAnnulus (x₀ : Parabolic.Vec3) (ρ : ℝ) : Set Parabolic.Vec3

Annulus containing the derivatives of the interior harmonic cutoff.

Equations

• CKN.Foundation.Heat.cutoffAnnulus x₀ ρ = CKN.euclideanBall x₀ (3 * ρ / 4) \ CKN.euclideanClosedBall x₀ (13 * ρ / 20)

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

theorem CKN.Foundation.Heat.eta_derivatives_zero_off_cutoff_annulus {x₀ y : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hy : y ∉ cutoffAnnulus x₀ ρ) (i j : Fin 3) : spatialDeriv (eta x₀ hρ) i y = 0 ∧ spatialDeriv (spatialDeriv (eta x₀ hρ) i) j y = 0

theorem CKN.Foundation.Heat.eta_spatialDeriv_zero_off_annulus {x₀ y : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hy : y ∉ cutoffAnnulus x₀ ρ) (i : Fin 3) : spatialDeriv (eta x₀ hρ) i y = 0

theorem CKN.Foundation.Heat.eta_spatialSecond_zero_off_annulus {x₀ y : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hy : y ∉ cutoffAnnulus x₀ ρ) (i j : Fin 3) : spatialDeriv (spatialDeriv (eta x₀ hρ) i) j y = 0

noncomputable def CKN.Foundation.Heat.harmonicInteriorValueConstant : ℝ

Coefficient for the cutoff contribution to the interior harmonic value bound.

Equations

• CKN.Foundation.Heat.harmonicInteriorValueConstant = (4 * Real.pi)⁻¹ * 30 * (3 / 4) * CKN.cutoffGradientConstant

noncomputable def CKN.Foundation.Heat.harmonicInteriorGradientConstant : ℝ

Coefficient for first-derivative terms in the interior harmonic representation.

Equations

• CKN.Foundation.Heat.harmonicInteriorGradientConstant = (4 * Real.pi)⁻¹ * 900 * (3 / 4) * CKN.cutoffGradientConstant + (4 * Real.pi)⁻¹ * 30 * (9 / 16) * CKN.cutoffSecondDerivativeConstant

noncomputable def CKN.Foundation.Heat.harmonicInteriorSourceConstant : ℝ

Coefficient for the Laplacian-cutoff source in the harmonic representation.

Equations

• CKN.Foundation.Heat.harmonicInteriorSourceConstant = (4 * Real.pi)⁻¹ * 30 * (27 / 16) * CKN.cutoffSecondDerivativeConstant

noncomputable def CKN.Foundation.Heat.harmonicInteriorSourceGradientConstant : ℝ

Coefficient for the gradient of the Laplacian-cutoff source term.

Equations

• CKN.Foundation.Heat.harmonicInteriorSourceGradientConstant = (4 * Real.pi)⁻¹ * 900 * (27 / 16) * CKN.cutoffSecondDerivativeConstant

noncomputable def CKN.Foundation.Heat.harmonicInteriorKernelXGradientConstant : ℝ

Coefficient for spatial differentiation of the harmonic representation kernel.

Equations

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

theorem CKN.Foundation.Heat.cutoffGradientConstant_nonneg_global : 0 ≤ cutoffGradientConstant

theorem CKN.Foundation.Heat.cutoffSecondDerivativeConstant_nonneg_global : 0 ≤ cutoffSecondDerivativeConstant

theorem CKN.Foundation.Heat.harmonicInteriorGradientConstant_nonneg : 0 ≤ harmonicInteriorGradientConstant

theorem CKN.Foundation.Heat.harmonicInteriorSourceConstant_nonneg : 0 ≤ harmonicInteriorSourceConstant

theorem CKN.Foundation.Heat.harmonicInteriorSourceGradientConstant_nonneg : 0 ≤ harmonicInteriorSourceGradientConstant

theorem CKN.Foundation.Heat.harmonicInteriorKernelXGradientConstant_nonneg : 0 ≤ harmonicInteriorKernelXGradientConstant

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

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

theorem CKN.Foundation.Heat.eta_laplacian_bound_global (x₀ : Parabolic.Vec3) {R : ℝ} (hR : 0 < R) (y : Parabolic.Vec3) : |spatialLaplacian (eta x₀ hR) y| ≤ 3 * cutoffSecondDerivativeConstant / R ^ 2

theorem CKN.Foundation.Heat.eta_laplacian_zero_off_annulus {x₀ y : Parabolic.Vec3} {R : ℝ} (hR : 0 < R) (hy : y ∉ cutoffAnnulus x₀ R) : spatialLaplacian (eta x₀ hR) y = 0

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

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

theorem CKN.Foundation.Heat.kernel_cutoff_x_derivative_bound_scaled {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (ρ / 2)) {y : Parabolic.Vec3} (hy : y ∈ cutoffAnnulus x₀ (4 * ρ / 3)) (i j : Fin 3) : |-spatialDeriv (spatialDeriv newtonianKernel i) j (x - y) * spatialDeriv (eta x₀ ⋯) i y + spatialDeriv newtonianKernel j (x - y) * spatialDeriv (spatialDeriv (eta x₀ ⋯) i) i y| ≤ harmonicInteriorKernelXGradientConstant * (ρ ^ 4)⁻¹

theorem CKN.Foundation.Heat.cutoffAnnulus_measurable {x₀ : Parabolic.Vec3} {R : ℝ} : 0 < R → MeasurableSet (cutoffAnnulus x₀ R)

theorem CKN.Foundation.Heat.cutoffAnnulus_subset_outer_ball {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : cutoffAnnulus x₀ (4 * ρ / 3) ⊆ euclideanBall x₀ ρ

theorem CKN.Foundation.Heat.memLp_of_continuousOn_bound {s : Set Parabolic.Vec3} (hs : MeasurableSet s) {f : Parabolic.Vec3 → ℝ} (hf : ContinuousOn f s) (C : ℝ) (hbound : ∀ x ∈ s, |f x| ≤ C) (p : ENNReal) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict s)] : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict s)

theorem CKN.Foundation.Heat.lpNorm_bound_on {s : Set Parabolic.Vec3} (hs : MeasurableSet s) {f : Parabolic.Vec3 → ℝ} {p : ENNReal} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict s)] (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ x ∈ s, ‖f x‖ ≤ C) : MeasureTheory.lpNorm f p (MeasureTheory.volume.restrict s) ≤ C * (MeasureTheory.volume s).toReal ^ p.toReal⁻¹

theorem CKN.Foundation.Heat.volume_root_bound {s : Set Parabolic.Vec3} {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hs : s ⊆ euclideanBall x₀ ρ) : (MeasureTheory.volume s).toReal ^ (1 / 3) ≤ ρ * (Real.pi * 4 / 3) ^ (1 / 3)

theorem CKN.Foundation.Heat.integral_mul_memLp_bound_on {A : Set Parabolic.Vec3} (hAmeas : MeasurableSet A) {f k : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict A)) (hk : MeasureTheory.MemLp k (ENNReal.ofReal 3) (MeasureTheory.volume.restrict A)) (hk_zero : ∀ y ∉ A, k y = 0) : |∫ (y : Parabolic.Vec3), f y * k y| ≤ MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict A) * MeasureTheory.lpNorm k (ENNReal.ofReal 3) (MeasureTheory.volume.restrict A)