Interior Representative

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

The fixed-annulus representative used for weakly harmonic functions.

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorRepresentative (h : Parabolic.Vec3 → ℝ) (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (x : Parabolic.Vec3) : ℝ

Interior representative constructed from a weakly harmonic function by Newtonian integration.

Equations

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

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorSourceConstant : ℝ

Source coefficient in the weakly harmonic interior representation estimate.

Equations

• CKN.Foundation.Heat.weakHarmonicInteriorSourceConstant = (4 * Real.pi)⁻¹ * 60 * CKN.cutoffSecondDerivativeConstant

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorCutoffConstant : ℝ

Cutoff-derivative coefficient in the weakly harmonic representation estimate.

Equations

• CKN.Foundation.Heat.weakHarmonicInteriorCutoffConstant = (4 * Real.pi)⁻¹ * (400 * CKN.cutoffGradientConstant + 20 * CKN.cutoffSecondDerivativeConstant)

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorXGradientConstant : ℝ

Spatial-gradient coefficient for the cutoff part of the weak harmonic representation.

Equations

• CKN.Foundation.Heat.weakHarmonicInteriorXGradientConstant = (4 * Real.pi)⁻¹ * (32000 * CKN.cutoffGradientConstant + 400 * CKN.cutoffSecondDerivativeConstant)

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorSourceXGradientConstant : ℝ

Spatial-gradient coefficient for the source part of the weak harmonic representation.

Equations

• CKN.Foundation.Heat.weakHarmonicInteriorSourceXGradientConstant = (4 * Real.pi)⁻¹ * (1200 * CKN.cutoffSecondDerivativeConstant)

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorSupConstant : ℝ

Supremum coefficient for the weakly harmonic interior representative.

Equations

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

noncomputable def CKN.Foundation.Heat.weakHarmonicInteriorGradientConstant : ℝ

Gradient coefficient for the weakly harmonic interior representative.

Equations

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

theorem CKN.Foundation.Heat.weakHarmonicInteriorSourceConstant_nonneg : 0 ≤ weakHarmonicInteriorSourceConstant

theorem CKN.Foundation.Heat.weakHarmonicInteriorCutoffConstant_nonneg : 0 ≤ weakHarmonicInteriorCutoffConstant

theorem CKN.Foundation.Heat.weakHarmonicInteriorXGradientConstant_nonneg : 0 ≤ weakHarmonicInteriorXGradientConstant

theorem CKN.Foundation.Heat.weakHarmonicInteriorSupConstant_nonneg : 0 ≤ weakHarmonicInteriorSupConstant

theorem CKN.Foundation.Heat.weakHarmonicInteriorSourceXGradientConstant_nonneg : 0 ≤ weakHarmonicInteriorSourceXGradientConstant

theorem CKN.Foundation.Heat.weak_annulus_distance {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (ρ / 2)) {y : Parabolic.Vec3} (hy : y ∈ cutoffAnnulus x₀ ρ) : ρ / 20 < ‖x - y‖

theorem CKN.Foundation.Heat.weak_annulus_subset_outer {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : cutoffAnnulus x₀ ρ ⊆ euclideanBall x₀ ρ

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

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

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

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

theorem CKN.Foundation.Heat.weak_source_kernel_zero_off_annulus {x x₀ y : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hy : y ∉ cutoffAnnulus x₀ ρ) : newtonianKernel (x - y) * spatialLaplacian (eta x₀ hρ) y = 0

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

theorem CKN.Foundation.Heat.weak_annulus_isFinite {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.volume (cutoffAnnulus x₀ ρ) ≠ ⊤

theorem CKN.Foundation.Heat.weak_lp_kernel_bound {x₀ : Parabolic.Vec3} {ρ C : ℝ} (hρ : 0 < ρ) {k : Parabolic.Vec3 → ℝ} (hAmeas : MeasurableSet (cutoffAnnulus x₀ ρ)) (hkcont : ContinuousOn k (cutoffAnnulus x₀ ρ)) (hC : 0 ≤ C) (hkbound : ∀ y ∈ cutoffAnnulus x₀ ρ, |k y| ≤ C * (ρ ^ 3)⁻¹) : MeasureTheory.lpNorm k (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (cutoffAnnulus x₀ ρ)) ≤ C * (Real.pi * 4 / 3) ^ (1 / 3) * (ρ ^ 2)⁻¹

theorem CKN.Foundation.Heat.weak_source_kernel_continuousOn {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (ρ / 2)) : ContinuousOn (fun (y : Parabolic.Vec3) => newtonianKernel (x - y) * spatialLaplacian (eta x₀ hρ) y) (cutoffAnnulus x₀ ρ)

theorem CKN.Foundation.Heat.weak_cutoff_kernel_continuousOn {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (ρ / 2)) (i : Fin 3) : ContinuousOn (fun (y : Parabolic.Vec3) => spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y) (cutoffAnnulus x₀ ρ)