Pk Bounds Unconditional Core

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

theorem CKN.pressure_slice_integral_aemeasurable {Ω' B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} : MeasurableSet B → MeasurableSet J → ∀ (hsub : B ⊆ Ω') (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))), AEMeasurable (fun (s : ℝ) => ∫ (x : Foundation.Parabolic.Vec3) in B, g (x, s)) (MeasureTheory.volume.restrict J)

theorem CKN.pressure_box_geometry {Ω : 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) : ∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J ∧ Foundation.Parabolic.vec3Ball z.1 ρ ⊆ Ω' ∧ Set.Ioc (z.2 - ρ ^ 2) z.2 ⊆ J

theorem CKN.pressure_prod_lintegral_swap {B : Set Foundation.Parabolic.Vec3} {T : Set ℝ} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : AEMeasurable F ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict T))) : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ T, ENNReal.ofReal (F z) = ∫⁻ (s : ℝ) in T, ∫⁻ (x : Foundation.Parabolic.Vec3) in B, ENNReal.ofReal (F (x, s))

theorem CKN.pressure_time_norm_bound {B : Set Foundation.Parabolic.Vec3} {T : Set ℝ} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} {G : ℝ → ℝ} {D : ENNReal} {p₀ : ℝ} (hp : 0 < p₀) (hF : MeasureTheory.Integrable F ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict T))) : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict T) → ∀ (hGdef : ∀ (s : ℝ), G s = (∫ (x : Foundation.Parabolic.Vec3) in B, F (x, s)) ^ (1 / p₀)) (hFnonneg : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ F z) (hbound : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ T, ENNReal.ofReal (F z) ≤ D), MeasureTheory.eLpNorm' G p₀ (MeasureTheory.volume.restrict T) ≤ D ^ (1 / p₀)

theorem CKN.pressure_lift_time_ae {B : Set Foundation.Parabolic.Vec3} {T : Set ℝ} {P : ℝ → Prop} (h : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, P s) : ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (B ×ˢ T), P z.2

theorem CKN.pressure_gradient_integrable {Ω : 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) : MeasureTheory.Integrable (fun (w : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du w) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ))

theorem CKN.pressure_energy_bound {Ω : 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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) ^ (1 / 2) ≤ √ρ * alpha u z ρ

theorem CKN.pressureP56_fixed_bound {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {x₀ : Foundation.Parabolic.Vec3} {ρ r s : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hp : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hpm : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hηeq : η = mollifiedBallCutoff x₀ hρ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ) (x : Foundation.Parabolic.Vec3) : x ∈ Foundation.Parabolic.vec3Ball x₀ r → |pressureP5 η p s x| + |pressureP6 η p s x| ≤ (18 * cutoffSecondDerivativeConstant + 240 * cutoffGradientConstant) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)|

theorem CKN.pressureP234_fixed_slice_bound {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ r s : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hu : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (humeas : AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (x : Foundation.Parabolic.Vec3) : x ∈ Foundation.Parabolic.vec3Ball x₀ r → |pressureP2 (mollifiedBallCutoff x₀ hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, u (y, t) j) s x| + |pressureP3 (mollifiedBallCutoff x₀ hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, u (y, t) j) s x| + |pressureP4 (mollifiedBallCutoff x₀ hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, u (y, t) j) s x| ≤ (18 * cutoffSecondDerivativeConstant + 720 * cutoffGradientConstant) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, pressureUTensorNorm u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, u (y, t) j) s y

theorem CKN.pressureP8_fixed_bound {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ r s : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hf : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (f (y, s))) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hfm : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hηeq : η = mollifiedBallCutoff x₀ hρ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ) (x : Foundation.Parabolic.Vec3) : x ∈ Foundation.Parabolic.vec3Ball x₀ r → |pressureP8 η f s x| ≤ 6 * cutoffGradientConstant / ρ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (f (y, s))