Oscillation Harmonic #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The weak-to-smooth pressure component used by the oscillation estimate.
theorem
CKN.pressure_harmonic_part_on_inner
{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₀ ρ))
theorem
CKN.pressure_harmonic_inner_integral_bound
{H : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r A : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
:
0 ≤ A →
∀ (hHmem : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r)))
(hHbound : ∀ x ∈ euclideanBall x₀ (ρ / 2), |H x| ≤ A),
∫ (x : Vec 3) in euclideanBall x₀ r, |H x| ^ (3 / 2) ≤ (MeasureTheory.volume (euclideanBall x₀ r)).toReal * A ^ (3 / 2)
theorem
CKN.pressureNewtonianPotential_weaklyHarmonicOn
{U : Set Foundation.Parabolic.Vec3}
{g : Foundation.Parabolic.Vec3 → ℝ}
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hgc : HasCompactSupport g)
(hzero : ∀ y ∈ U, g y = 0)
:
theorem
CKN.pressureNewtonianDerivativePotential_weaklyHarmonicOn
{U : Set Foundation.Parabolic.Vec3}
{g : Foundation.Parabolic.Vec3 → ℝ}
(i : Fin 3)
(hg : MeasureTheory.Integrable g MeasureTheory.volume)
(hgc : HasCompactSupport g)
(hzero : ∀ y ∈ U, g y = 0)
:
structure
CKN.PressureHarmonicPotentialData
(U : Set Foundation.Parabolic.Vec3)
(η : Foundation.Parabolic.Vec3 → ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(c : ℝ → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(s : ℝ)
:
Integrability, support, and inner-ball vanishing data for the annular pressure terms.
- p2_integrable (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) MeasureTheory.volume
- p2_compactSupport (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j
- p2_vanishes (i j : Fin 3) (y : Foundation.Parabolic.Vec3) : y ∈ U → mixedSecond η i j y * pressureUTensor u c (y, s) i j = 0
- p3_integrable (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume
- p3_compactSupport (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y
- p3_vanishes (i j : Fin 3) (y : Foundation.Parabolic.Vec3) : y ∈ U → pressureUTensor u c (y, s) i j * spatialDeriv η i y = 0
- p4_integrable (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume
- p4_compactSupport (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y
- p4_vanishes (i j : Fin 3) (y : Foundation.Parabolic.Vec3) : y ∈ U → pressureUTensor u c (y, s) i j * spatialDeriv η j y = 0
- p5_integrable : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) MeasureTheory.volume
- p5_compactSupport : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y
- p5_vanishes (y : Foundation.Parabolic.Vec3) : y ∈ U → p (y, s) * spatialLaplacian η y = 0
- p6_integrable (j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) MeasureTheory.volume
- p6_compactSupport (j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)
Instances For
theorem
CKN.pressure_harmonic_potentials_weaklyHarmonicOn
{U : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{s : ℝ}
(hP2Int :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j)
MeasureTheory.volume)
(hP2Supp :
∀ (i j : Fin 3),
HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j)
(hP2zero : ∀ (i j : Fin 3), ∀ y ∈ U, mixedSecond η i j y * pressureUTensor u c (y, s) i j = 0)
(hP3Int :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume)
(hP3Supp :
∀ (i j : Fin 3),
HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y)
(hP3zero : ∀ (i j : Fin 3), ∀ y ∈ U, pressureUTensor u c (y, s) i j * spatialDeriv η i y = 0)
(hP4Int :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume)
(hP4Supp :
∀ (i j : Fin 3),
HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y)
(hP4zero : ∀ (i j : Fin 3), ∀ y ∈ U, pressureUTensor u c (y, s) i j * spatialDeriv η j y = 0)
(hP5Int :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y)
MeasureTheory.volume)
(hP5Supp : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y)
(hP5zero : ∀ y ∈ U, p (y, s) * spatialLaplacian η y = 0)
(hP6Int :
∀ (j : Fin 3),
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s))
MeasureTheory.volume)
(hP6Supp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s))
(hP6zero : ∀ (j : Fin 3), ∀ y ∈ U, spatialDeriv η j y * p (y, s) = 0)
:
Foundation.Heat.WeaklyHarmonicOn U
(pressureP2 η u c s + pressureP3 η u c s + pressureP4 η u c s + pressureP5 η p s + pressureP6 η p s)
theorem
CKN.pressure_harmonic_potentials_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
(pressureP2 η u c s + pressureP3 η u c s + pressureP4 η u c s + pressureP5 η p s + pressureP6 η p s)
theorem
CKN.pressure_harmonic_potential_data_ae_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{η : Foundation.Parabolic.Vec3 → ℝ}
{c : ℝ → Foundation.Parabolic.Vec3}
{U : Set Foundation.Parabolic.Vec3}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
(hηΩ : tsupport η ⊆ Ω)
(hηd0 : ∀ (i : Fin 3), ∀ y ∈ U, spatialDeriv η i y = 0)
(hηm0 : ∀ (i j : Fin 3), ∀ y ∈ U, mixedSecond η i j y = 0)
(hηLap0 : ∀ y ∈ U, spatialLaplacian η y = 0)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, PressureHarmonicPotentialData U η u c p s