Interior Estimates

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

noncomputable def CKN.Foundation.Heat.harmonicInteriorSupConstant : ℝ

Coefficient in the interior supremum estimate for a harmonic function.

Equations

• CKN.Foundation.Heat.harmonicInteriorSupConstant = (Real.pi * 4 / 3) ^ (1 / 3) * (CKN.Foundation.Heat.harmonicInteriorSourceConstant + 6 * CKN.Foundation.Heat.harmonicInteriorGradientConstant)

noncomputable def CKN.Foundation.Heat.harmonicInteriorGradientSupConstant : ℝ

Coefficient in the interior supremum estimate for the harmonic gradient.

Equations

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

theorem CKN.Foundation.Heat.harmonicInteriorGradientSupConstant_nonneg : 0 ≤ harmonicInteriorGradientSupConstant

theorem CKN.Foundation.Heat.smooth_harmonic_interior_gradient_bound {H : Parabolic.Vec3 → ℝ} (hH : ContDiff ℝ (↑⊤) H) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hHarm : ∀ y ∈ euclideanBall x₀ ρ, spatialLaplacian H y = 0) (hHmem : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) (x : Vec 3) : x ∈ euclideanBall x₀ (ρ / 2) → ∀ (j : Fin 3), |spatialDeriv H j x| ≤ harmonicInteriorGradientSupConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))