A jointly measurable force pressure

For a strongly measurable space-time force, apply the slice force pressure of lem:force-pressure at every time. Each spatial mollification of the result is continuous in space, and at a fixed point it is measurable in time, since it is the pairing of the slice pressure with a fixed test function and hence the L² pairing of the force slice with a fixed field. Such functions are jointly measurable, and their pointwise limit as the mollification radius shrinks is a jointly measurable function whose time slices are the slice pressures almost everywhere.

noncomputable def CKN.Leray.forcePressureSliceOfField (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (t : ℝ) : Foundation.Parabolic.Vec3 → ℝ

The slice force pressure of a space-time field at one time, set to zero when the time slice is not square integrable.

Equations

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

theorem CKN.Leray.forcePressureSliceOfField_locallyIntegrable (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (t : ℝ) : MeasureTheory.LocallyIntegrable (forcePressureSliceOfField F t) MeasureTheory.volume

The slice force pressure of a field is locally integrable in space.

theorem CKN.Leray.measurable_eLpNorm_two_slice {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) : Measurable fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume

The L² norm of the time slices of a strongly measurable field is measurable in time.

theorem CKN.Leray.measurableSet_memLp_slice {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) : MeasurableSet {t : ℝ | MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume}

The set of times at which a strongly measurable field has a square integrable slice is measurable.

theorem CKN.Leray.measurable_mollify_forcePressureSliceOfField {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) {ε : ℝ} (hε : 0 < ε) (x : Foundation.Parabolic.Vec3) : Measurable fun (t : ℝ) => mollify (forcePressureSliceOfField F t) ε hε x

At a fixed point, a mollification of the slice force pressure is measurable in time.

theorem CKN.Leray.measurable_mollify_forcePressureSliceOfField_spaceTime {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) {ε : ℝ} (hε : 0 < ε) : Measurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => mollify (forcePressureSliceOfField F z.2) ε hε z.1

A mollification of the slice force pressure is jointly measurable in space and time.

theorem CKN.Leray.forcePressure_radius_pos (n : ℕ) : 0 < 1 / (↑n + 1)

noncomputable def CKN.Leray.forcePressureOfField (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The jointly measurable force pressure of a space-time field: the limit of the spatial mollifications of its slice force pressures.

Equations

• CKN.Leray.forcePressureOfField F z = Filter.atTop.limUnder fun (n : ℕ) => CKN.mollify (CKN.Leray.forcePressureSliceOfField F z.2) (1 / (↑n + 1)) ⋯ z.1

theorem CKN.Leray.forcePressureOfField_stronglyMeasurable {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) : MeasureTheory.StronglyMeasurable (forcePressureOfField F)

The force pressure of a strongly measurable field is strongly measurable.

theorem CKN.Leray.forcePressureOfField_slice_ae_eq (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (t : ℝ) : (fun (x : Foundation.Parabolic.Vec3) => forcePressureOfField F (x, t)) =ᵐ[MeasureTheory.volume] forcePressureSliceOfField F t

Every time slice of the force pressure of a field agrees almost everywhere with the slice force pressure.