The space-time weak pressure gradient on a whole time interval

The measurable selection of a space-time weak spatial derivative from slice-wise weak derivatives is carried out on a product box whose time factor carries an integrable datum. The time set of a suitable weak solution is only an open interval, so the datum need not be integrable there; the selection is therefore made on each member of a countable increasing family of time windows and the resulting fields are assembled into a single one.

The assembled field is unambiguous because the slice-wise weak derivative is unique almost everywhere on the inner spatial set: two selections made on overlapping windows agree with the same slice derivative at almost every time. This module records the gluing construction and the geometric facts about the unit domain hypothesis of the one-sided pressure estimate.

theorem CKN.Core.Step4.OriginInstance.originUnitBall_subset_of_dom {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) : {y : Foundation.Parabolic.Vec3 | Foundation.Parabolic.vec3EuclideanNorm (y - 0) ≤ 1} ⊆ Ω ∧ Set.Icc (-1) 0 ⊆ I

The unit domain hypothesis gives the closed unit spatial ball inside Ω.

theorem CKN.Core.Step4.OriginInstance.originIsCompact_closure_vec3Ball {x : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : IsCompact (closure (Foundation.Parabolic.vec3Ball x r))

The closure of a Euclidean spatial ball of positive radius is compact.

theorem CKN.Core.Step4.OriginInstance.originLocalBox_of_time {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {R₀ : ℝ} (hR₀ : 0 < R₀) (hR₀one : R₀ < 1) (hΩ : {y : Foundation.Parabolic.Vec3 | Foundation.Parabolic.vec3EuclideanNorm (y - 0) ≤ 1} ⊆ Ω) {J : Set ℝ} (hJord : J.OrdConnected) (hJcompact : IsCompact J) (hJI : J ⊆ I) : localBox Ω I (Foundation.Parabolic.vec3Ball 0 R₀) J

The outer spatial ball of the origin construction is a local box together with any compact order-connected time set inside I.

noncomputable def CKN.Core.Step4.OriginInstance.timeGluedField (D : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (A : ℕ → Set ℝ) : Foundation.Parabolic.ParabolicPoint → ℝ

The space-time field assembled from a family of fields indexed by a pairwise disjoint decomposition of the time axis.

Equations

• CKN.Core.Step4.OriginInstance.timeGluedField D A z = if h : ∃ (n : ℕ), z.2 ∈ A n then D (Nat.find h) z else 0

theorem CKN.Core.Step4.OriginInstance.timeGluedField_eq_of_mem {D : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ} {A : ℕ → Set ℝ} (hdisj : Pairwise (Function.onFun Disjoint A)) {n : ℕ} {z : Foundation.Parabolic.ParabolicPoint} (hz : z.2 ∈ A n) : timeGluedField D A z = D n z

On the n-th piece of the decomposition the glued field is the n-th field.

theorem CKN.Core.Step4.OriginInstance.timeGluedField_eq_zero {D : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ} {A : ℕ → Set ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hz : ∀ (n : ℕ), z.2 ∉ A n) : timeGluedField D A z = 0

Off the decomposition the glued field vanishes.

theorem CKN.Core.Step4.OriginInstance.exists_spacetime_weak_gradient_on_time_union (k : Fin 3) {B B' : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hB : IsOpen B) (hB' : MeasurableSet B') (hB'c : IsCompact (closure B')) (hB'B : closure B' ⊆ B) {J : ℕ → Set ℝ} (hJmeas : ∀ (n : ℕ), MeasurableSet (J n)) (hJI : ⋃ (n : ℕ), J n = I) (hp : ∀ (n : ℕ), MeasureTheory.IntegrableOn p (B ×ˢ J n) MeasureTheory.volume) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, t)) g) : ∃ (D : Foundation.Parabolic.ParabolicPoint → ℝ), AEMeasurable D (MeasureTheory.volume.restrict (B' ×ˢ I)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume → HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, t)) g → (fun (x : Foundation.Parabolic.Vec3) => D (x, t)) =ᵐ[MeasureTheory.volume.restrict B'] g) ∧ (∀ (n : ℕ) (Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ → HasCompactSupport Ψ → tsupport Ψ ⊆ B' ×ˢ J n → ∫ (t : ℝ) in J n, ∫ (x : Foundation.Parabolic.Vec3) in B', p (x, t) * spatialPartial Ψ k (x, t) = -∫ (t : ℝ) in J n, ∫ (x : Foundation.Parabolic.Vec3) in B', D (x, t) * Ψ (x, t)) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ∉ I → D z = 0

The space-time weak spatial derivative on a countable increasing union of time windows. The three conclusions are joint measurability on the inner box, identification with every slice weak derivative at almost every time, and the iterated integration-by-parts identity on each window.