Slice identities behind the pressure gauge invariance

This file collects the measure-theoretic slice identities used in the proof of the pressure gauge invariance of rem:two-means in paper/ckn.tex: a suitable weak solution stays one when an arbitrary function of time is added to the pressure.

The two facts that carry the analytic content are

• gauge_divergence_pairing: the gauge pairs integrably with the divergence of a space-time test field and the pairing vanishes, because the spatial integral of a divergence vanishes on every time slice;
• gauge_velocity_pairing: the gauge pairs integrably with u · ∇ψ and the pairing vanishes, because the divergence-free clause (S2) of def:sws, tested against θ(t)ψ(x,t), forces the spatial pairing of the slice u(·,t) with ∇ψ(·,t) to vanish for almost every time.

The uniform time-slice bound of the velocity comes from the essential supremum of the slice energies in def:sws together with x ≤ 1 + x²; no Gagliardo-Nirenberg input is needed.

theorem CKN.memLp_gauge_on_box {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) {c : ℝ → ℝ} (hc : MeasureTheory.MemLp c (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict J)) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => c z.2) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

A time-dependent gauge in L^{3/2}(J) lies in L^{3/2} of the space-time box.

theorem CKN.spatialPartial_eq_zero_off_tsupport {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) (i : Fin 3) : spatialPartial ψ i z = 0

A spatial partial derivative vanishes off the topological support.

theorem CKN.tsupport_parabolic_eq {V : Type} [Zero V] (f : Foundation.Parabolic.Vec3 × ℝ → V) : tsupport (have this := f; this) = tsupport f

The parabolic topology and the product topology have the same closed supports: the identity is a homeomorphism between them.

theorem CKN.tsupport_spatialPartial_subset {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (i : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial ψ i z) ⊆ tsupport ψ

The support of a spatial partial derivative lies in the support of the function.

theorem CKN.timePartial_eq_zero_off_tsupport {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : timePartial ψ z = 0

A time partial derivative vanishes off the topological support.

theorem CKN.tsupport_component_subset {ι : Type} (φ : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ) (i : ι) (hzero : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), φ z = 0 → φ z i = 0) : (tsupport fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w i) ⊆ tsupport φ

A component of a vector-valued test function has support inside the support of the test function.

theorem CKN.gauge_divergence_pairing {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {c : ℝ → ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hIord : I.OrdConnected) (hc : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → MeasureTheory.MemLp c (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict J)) {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => c z.2 * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.Vec3 × ℝ), c z.2 * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z = 0

The gauge pairs integrably with the divergence of a vector test function, and the pairing vanishes.

theorem CKN.gauge_velocity_pairing {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hIord : I.OrdConnected) (hc : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → MeasureTheory.MemLp c (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict J)) (humeas : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hessSup : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J → essSup (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict J) < ⊤) (hS2 : ∀ χ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * spatialPartial χ i z) (tsupport χ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial χ i z = 0) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => c z.2 * ∑ i : Fin 3, u z i * spatialPartial ψ i z) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.Vec3 × ℝ), c z.2 * ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0

The gauge pairs integrably with the velocity paired against a spatial gradient, and the pairing vanishes.