Oscillation Lin34

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

noncomputable def CKN.pressureChat (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

The velocity oscillation in eq:Chat, with the spatial mean taken at each time.

Equations

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

noncomputable def CKN.pressureD (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

The unrooted pressure quantity D used in the integrated Lin estimate.

Equations

• CKN.pressureD p z r = r⁻¹ ^ 2 * ∫ (w : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder z.1 z.2 r, |p w| ^ (3 / 2)

noncomputable def CKN.lin34Constant (C₁₁ : ℝ) : ℝ

Coefficient combining the singular-integral and harmonic pressure estimates.

Equations

• CKN.lin34Constant C₁₁ = (√2 + 2 * (Real.pi * 4 / 3) * CKN.Foundation.Heat.weakHarmonicInteriorSupConstant ^ (3 / 2)) * max 1 (C₁₁ ^ (3 / 2))

theorem CKN.pressure_oscillation_integral_of_components {p p₁ H : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {r I₁ IH C₁₁ E : ℝ} : 0 < r → 0 ≤ E → 0 ≤ C₁₁ → ∀ (hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hH : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hrep : p =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] p₁ + H) (hI₁ : ∫ (x : Vec 3) in euclideanBall x₀ r, |p₁ x| ^ (3 / 2) ≤ I₁) (hIH : ∫ (x : Vec 3) in euclideanBall x₀ r, |H x| ^ (3 / 2) ≤ IH), ∫ (x : Vec 3) in euclideanBall x₀ r, |p x| ^ (3 / 2) ≤ √2 * (I₁ + IH)

theorem CKN.pressure_oscillation_integral_of_components_force {p p₁ H J : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {r I₁ IH IJ : ℝ} (hr : 0 < r) (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hH : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hJ : MeasureTheory.MemLp J (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) (hrep : p =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] p₁ + H + J) (hI₁ : ∫ (x : Vec 3) in euclideanBall x₀ r, |p₁ x| ^ (3 / 2) ≤ I₁) (hIH : ∫ (x : Vec 3) in euclideanBall x₀ r, |H x| ^ (3 / 2) ≤ IH) (hIJ : ∫ (x : Vec 3) in euclideanBall x₀ r, |J x| ^ (3 / 2) ≤ IJ) : ∫ (x : Vec 3) in euclideanBall x₀ r, |p x| ^ (3 / 2) ≤ 2 * (I₁ + IH + IJ)

The harmonic contribution after the interior estimate and the named CZ input.

theorem CKN.pressureD_integrated_from_slices {p : Foundation.Parabolic.ParabolicPoint → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {r ρ C a b : ℝ} {F G H : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hF : MeasureTheory.Integrable F μ) (hG : MeasureTheory.Integrable G μ) (hH : MeasureTheory.Integrable H μ) (hpoint : ∀ᵐ (t : ℝ) ∂μ, F t ≤ C * (a * G t + b * H t)) (hDr : pressureD p z r = ∫ (t : ℝ), F t ∂μ) (hDρ : pressureD p z ρ = ∫ (t : ℝ), H t ∂μ) (hChat : pressureChat u z ρ = ∫ (t : ℝ), G t ∂μ) : pressureD p z r ≤ C * (a * pressureChat u z ρ + b * pressureD p z ρ)

noncomputable def CKN.lin34ForceConstant (C₁₃ : ℝ) : ℝ

Coefficient for the forcing term in the localized pressure estimate.

Equations

• CKN.lin34ForceConstant C₁₃ = √2 * (1 + C₁₃ ^ (3 / 2))

theorem CKN.pressureD_integrated_from_slices_force {p : Foundation.Parabolic.ParabolicPoint → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {r ρ C a b L : ℝ} {F G H J : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hC : 0 ≤ C) (hF : MeasureTheory.Integrable F μ) (hG : MeasureTheory.Integrable G μ) (hH : MeasureTheory.Integrable H μ) (hJ : MeasureTheory.Integrable J μ) (hpoint : ∀ᵐ (t : ℝ) ∂μ, F t ≤ C * (a * G t + b * H t + J t)) (hJbound : ∫ (t : ℝ), J t ∂μ ≤ L) (hDr : pressureD p z r = ∫ (t : ℝ), F t ∂μ) (hDρ : pressureD p z ρ = ∫ (t : ℝ), H t ∂μ) (hChat : pressureChat u z ρ = ∫ (t : ℝ), G t ∂μ) : pressureD p z r ≤ C * (a * pressureChat u z ρ + b * pressureD p z ρ + L)

theorem CKN.pressure_lin34_integrated_force {p : Foundation.Parabolic.ParabolicPoint → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {r ρ C₁₃ lam : ℝ} {F G H J : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hC₁₃ : 0 ≤ C₁₃) (hF : MeasureTheory.Integrable F μ) (hG : MeasureTheory.Integrable G μ) (hH : MeasureTheory.Integrable H μ) (hJ : MeasureTheory.Integrable J μ) (hpoint : ∀ᵐ (t : ℝ) ∂μ, F t ≤ lin34ForceConstant C₁₃ * ((ρ / r) ^ 2 * G t + r / ρ * H t + J t)) (hJbound : ∫ (t : ℝ), J t ∂μ ≤ (r / ρ) ^ (3 / 2) * lam ^ (3 / 2)) (hDr : pressureD p z r = ∫ (t : ℝ), F t ∂μ) (hDρ : pressureD p z ρ = ∫ (t : ℝ), H t ∂μ) (hChat : pressureChat u z ρ = ∫ (t : ℝ), G t ∂μ) : pressureD p z r ≤ lin34ForceConstant C₁₃ * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lam ^ (3 / 2))