I4 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_I4_holder
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{F U : α → ENNReal}
{q C : ℝ}
(hq : 5 / 2 < q)
(hF : AEMeasurable F μ)
(hU : AEMeasurable U μ)
(hC : ENNReal.ofReal C ≠ ⊤)
:
theorem
CKN.caccioppoli_I4_force_integral_identity
{Ω : 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)
(z : Foundation.Parabolic.ParabolicPoint)
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q = ENNReal.ofReal ((ρ ^ (5 / q - 3) * lambda q f z ρ) ^ q)
theorem
CKN.caccioppoli_I4_space_time_bound
{q ρ r : ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ : ℝ}
(hq : 5 / 2 < q)
(hr : 0 < r)
{u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{φ : Foundation.Parabolic.ParabolicPoint → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)))
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hf :
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)))
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hφ : ∀ w ∈ Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, φ w ≤ 1000 / r)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, 2 * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) * ENNReal.ofReal (φ w) ≤ ENNReal.ofReal (2000 / r) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q) ^ (1 / q) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3) ^ (1 / 3) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ^ (1 / (q / (q - 1)) - 1 / 3)
theorem
CKN.caccioppoli_I4_normalization
{q ρ r γ ell : ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ : ℝ}
(hq : 5 / 2 < q)
(hρ : 0 < ρ)
(hr : 0 < r)
(hγ : 0 ≤ γ)
(hell : 0 ≤ ell)
{u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{φ : Foundation.Parabolic.ParabolicPoint → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)))
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hf :
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)))
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hφ : ∀ w ∈ Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, φ w ≤ 1000 / r)
(hforce :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q = ENNReal.ofReal ((ρ ^ (5 / q - 3) * ell) ^ q))
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 = ENNReal.ofReal (ρ ^ 2 * γ ^ 3))
:
(∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, 2 * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) * ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) * ENNReal.ofReal (φ w)).toReal ≤ 2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3) * (r / ρ)⁻¹ * γ * ell