The data part of a suitable weak solution

CKN.IsSuitableWeakSolutionIntegrable from paper label def:sws is a conjunction of two very different kinds of clauses. The first six record that the fields are measurable and have the stated local integrability; the last three record the divergence-free identity, the weak momentum identity and the local energy inequality, each of them paired with an integrability side condition on the integrand it tests.

This file names the first six clauses CKN.IsSuitableWeakSolutionData. The body below is a character-for-character copy of the corresponding part of the definition, so CKN.IsSuitableWeakSolutionIntegrable.toData is a plain projection of the anonymous constructor and needs no tactic; that is the proof that the predicate defined here is exactly those six clauses and nothing more.

Everything downstream that only needs measurability and local integrability should take IsSuitableWeakSolutionData rather than the full class. A lemma stated that way can be used while the identity clauses of the class are still being established, which a lemma stated with the full class cannot.

def CKN.IsSuitableWeakSolutionData (Ω : 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) : Prop

The measurability and local-integrability clauses of def:sws: the first six conjuncts of CKN.IsSuitableWeakSolutionIntegrable, copied verbatim.

Equations

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

theorem CKN.IsSuitableWeakSolutionIntegrable.toData {Ω : 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} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) : IsSuitableWeakSolutionData Ω I q u Du p f

A suitable weak solution carries the data clauses of def:sws. The proof is the projection of the first six components, with no tactic: this is what certifies that IsSuitableWeakSolutionData is the data part of the class.

theorem CKN.IsSuitableWeakSolutionData.isOpen_space {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) : IsOpen Ω

The spatial carrier is open.

theorem CKN.IsSuitableWeakSolutionData.isOpen_time {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) : IsOpen I

The time carrier is open.

theorem CKN.IsSuitableWeakSolutionData.ordConnected_time {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) : I.OrdConnected

The time carrier is order connected, hence an interval.

theorem CKN.IsSuitableWeakSolutionData.five_halves_lt_exponent {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) : 5 / 2 < q

The force exponent exceeds 5 / 2.

theorem CKN.IsSuitableWeakSolutionData.force_localVecLp {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : localVecLp (spaceTimeSet Ω' J) q f

The force is componentwise L^q on every local box.

theorem CKN.IsSuitableWeakSolutionData.aestronglyMeasurable_velocity {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The velocity is measurable on every local box.

theorem CKN.IsSuitableWeakSolutionData.aestronglyMeasurable_gradient {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The velocity gradient is measurable on every local box.

theorem CKN.IsSuitableWeakSolutionData.aestronglyMeasurable_pressure {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The pressure is measurable on every local box.

theorem CKN.IsSuitableWeakSolutionData.aestronglyMeasurable_force {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The force is measurable on every local box.

theorem CKN.IsSuitableWeakSolutionData.essSup_sliceEnergy_lt_top {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : essSup (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict J) < ⊤

The spatial slice energies of the velocity are essentially bounded in time on every local box.

theorem CKN.IsSuitableWeakSolutionData.energy_lintegral_lt_top {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤

The velocity and its gradient have finite joint energy on every local box.

theorem CKN.IsSuitableWeakSolutionData.memLp_pressure {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The pressure is L^{3/2} on every local box.

theorem CKN.IsSuitableWeakSolutionData.memLp_force {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.MemLp f (ENNReal.ofReal q) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The force is L^q on every local box.

theorem CKN.IsSuitableWeakSolutionData.hasWeakGradientOn_slice {Ω : 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} (h : IsSuitableWeakSolutionData Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) (i : Fin 3) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakGradientOn Ω' (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => Du (x, s) i

For almost every time, the spatial slice of the velocity has the corresponding slice of Du as its weak gradient on the box.