Localized Equation Basics

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

These are the divergence-form sources obtained directly from the tested equation.

noncomputable def CKN.Core.Step3.localizedDivergenceG (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (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) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Non-divergence source in the localized momentum equation, including pressure and forcing.

Equations

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

noncomputable def CKN.Core.Step3.localizedDivergenceH (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Tensor divergence source in the localized momentum equation.

Equations

• CKN.Core.Step3.localizedDivergenceH φ u p j z i = φ z * u z i * u z j + u z i * CKN.spatialPartial φ j z + if i = j then p z * φ z else 0

theorem CKN.Core.Step3.timePartial_mul_full {a b : Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hb : ContDiff ℝ (↑⊤) b) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => a w * b w) z = timePartial a z * b z + a z * timePartial b z

theorem CKN.Core.Step3.spatialPartial_mul_full {a b : Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hb : ContDiff ℝ (↑⊤) b) (j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => a w * b w) j z = spatialPartial a j z * b z + a z * spatialPartial b j z

theorem CKN.Core.Step3.timePartial_contDiff_full {a : Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial a z

theorem CKN.Core.Step3.spatialSecondPartial_contDiff_full {a : Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (i j : Fin 3) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialSecondPartial a i j z

theorem CKN.Core.Step3.local_box_isFiniteMeasure {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsCompact (closure Ω')) (hJ : IsCompact (closure J)) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

theorem CKN.Core.Step3.local_memLp_two_of_energy {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))} {hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))} (henergy : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

theorem CKN.Core.Step3.compact_factor_integrable {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {a : Foundation.Parabolic.ParabolicPoint → ℝ} {b : Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : MeasureTheory.Integrable a (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hb : Continuous b) (hbc : HasCompactSupport b) (hbs : tsupport b ⊆ spaceTimeSet Ω' J) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => a z * b z) MeasureTheory.volume

theorem CKN.Core.Step3.global_integral_eq_box_slices {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hzero : ∀ z ∉ spaceTimeSet Ω' J, F z = 0) : ∫ (z : Foundation.Parabolic.ParabolicPoint), F z = ∫ (t : ℝ), ∫ (x : Foundation.Parabolic.Vec3) in Ω', F (x, t)

theorem CKN.Core.Step3.box_slice_zero_of_time_not_mem {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hzero : ∀ z ∉ spaceTimeSet Ω' J, F z = 0) {t : ℝ} (ht : t ∉ J) : ∫ (x : Foundation.Parabolic.Vec3) in Ω', F (x, t) = 0

theorem CKN.Core.Step3.global_integral_transfer {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {B A C : Foundation.Parabolic.ParabolicPoint → ℝ} (hB : MeasureTheory.Integrable B MeasureTheory.volume) (hA : MeasureTheory.Integrable A MeasureTheory.volume) (hC : MeasureTheory.Integrable C MeasureTheory.volume) (hBzero : ∀ z ∉ spaceTimeSet Ω' J, B z = 0) (hAzero : ∀ z ∉ spaceTimeSet Ω' J, A z = 0) (hCzero : ∀ z ∉ spaceTimeSet Ω' J, C z = 0) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∫ (x : Foundation.Parabolic.Vec3) in Ω', B (x, t) = (-∫ (x : Foundation.Parabolic.Vec3) in Ω', A (x, t)) - ∫ (x : Foundation.Parabolic.Vec3) in Ω', C (x, t)) : ∫ (z : Foundation.Parabolic.ParabolicPoint), B z = (-∫ (z : Foundation.Parabolic.ParabolicPoint), A z) - ∫ (z : Foundation.Parabolic.ParabolicPoint), C z

theorem CKN.Core.Step3.zero_outside_box_of_tsupport_subset {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {b : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hbs : tsupport b ⊆ spaceTimeSet Ω' J) (z : Foundation.Parabolic.ParabolicPoint) : z ∉ spaceTimeSet Ω' J → b (z.1, z.2) = 0