Harmonic Part Derivatives #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.harmonicPressurePart
(η : Foundation.Parabolic.Vec3 → ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(c : ℝ → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(s : ℝ)
:
The harmonic pressure part appearing in the local decomposition.
Equations
- CKN.harmonicPressurePart η u c p s = CKN.pressureP2 η u c s + CKN.pressureP3 η u c s + CKN.pressureP4 η u c s + CKN.pressureP5 η p s + CKN.pressureP6 η p s
Instances For
theorem
CKN.harmonicPressurePart_weaklyHarmonicOn_of_data
{U : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{s : ℝ}
(hdata : PressureHarmonicPotentialData U η u c p s)
:
Foundation.Heat.WeaklyHarmonicOn U (harmonicPressurePart η u c p s)
The annular pressure terms are weakly harmonic wherever their source data vanish.
theorem
CKN.harmonicPressurePart_inner_representative
{h : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
(hweak : Foundation.Heat.WeaklyHarmonicOn (euclideanBall x₀ ρ) h)
:
∃ (H : Foundation.Parabolic.Vec3 → ℝ),
ContDiffOn ℝ (↑1) H (euclideanBall x₀ (ρ / 2)) ∧ h =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))] H ∧ (∀ x ∈ euclideanBall x₀ (ρ / 2),
|H x| ≤ Foundation.Heat.weakHarmonicInteriorSupConstant * (ρ ^ 2)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))) ∧ ∀ x ∈ euclideanBall x₀ (ρ / 2),
Foundation.Parabolic.vec3EuclideanNorm (classicalGradient H x) ≤ 1728 * Foundation.Heat.harmonicInteriorGradientSupConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))
A weakly harmonic pressure part has the available smooth inner representative together with its value and gradient estimates.