I2

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

theorem CKN.caccioppoli_I2_mean_subtraction {X : Type} [TopologicalSpace X] {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (Ψ : X → Foundation.Parabolic.Vec3 → ℝ) (g₀ : Foundation.Parabolic.Vec3 → ℝ) (g₁ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (g₂ : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ) {D : Set X} (hDcount : D.Countable) (hD : Dense D) (hΨ₀ : Continuous fun (z : X × Foundation.Parabolic.Vec3) => Ψ z.1 z.2) (hΨ₁ : ∀ (i : Fin 3), Continuous fun (z : X × Foundation.Parabolic.Vec3) => spatialDeriv (Ψ z.1) i z.2) (hΨ₂ : ∀ (i j : Fin 3), Continuous fun (z : X × Foundation.Parabolic.Vec3) => mixedSecond (Ψ z.1) i j z.2) (hK₀ : ∀ (x : X), ∀ y ∉ K, Ψ x y = 0) (hK₁ : ∀ (x : X) (y : Foundation.Parabolic.Vec3) (i : Fin 3), y ∉ K → spatialDeriv (Ψ x) i y = 0) (hK₂ : ∀ (x : X) (y : Foundation.Parabolic.Vec3) (i j : Fin 3), y ∉ K → mixedSecond (Ψ x) i j y = 0) (hg₀ : MeasureTheory.IntegrableOn g₀ K MeasureTheory.volume) (hg₁ : MeasureTheory.IntegrableOn g₁ K MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ K MeasureTheory.volume) (hzero : ∀ x ∈ D, parametricPairing Ψ g₀ g₁ g₂ x = 0) (x : X) : parametricPairing Ψ g₀ g₁ g₂ x = 0

theorem CKN.caccioppoli_I2_slice_divfree_countable {Ω : 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) {C : Set (Foundation.Parabolic.Vec3 → ℝ)} (hC : C.Countable) (hCtest : ∀ ψ ∈ C, ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ Ω) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ ψ ∈ C, ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, u (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

theorem CKN.caccioppoli_I2_velocity_integral_identity {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 = ENNReal.ofReal (ρ ^ 2 * gamma u z ρ ^ 3)

theorem CKN.caccioppoli_I2_holder {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A B : α → ENNReal} {C : ENNReal} (hA : AEMeasurable A μ) (hB : AEMeasurable B μ) (hC : C ≠ ⊤) : ∫⁻ (x : α), C * A x * B x ∂μ ≤ C * (∫⁻ (x : α), A x ^ (3 / 2) ∂μ) ^ (2 / 3) * (∫⁻ (x : α), B x ^ 3 ∂μ) ^ (1 / 3)

theorem CKN.caccioppoli_I2_normalization {κ α β γ K C₂₅ I₂ : ℝ} (hκ : 0 < κ) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hγ : 0 ≤ γ) (hKbound : K ≤ C₂₅ ^ 2) (hraw : I₂ ≤ K * κ⁻¹ ^ 2 * α * β * γ) : I₂ ≤ (C₂₅ * κ⁻¹ * α ^ (1 / 2) * β ^ (1 / 2) * γ ^ (1 / 2)) ^ 2