The quadratic pressure of the forced regularized solution

The pressure p_ε = P[J_ε u_ε ⊗ u_ε] + p_f of lem:regularised-forced: at each time the quadratic part is the Riesz pressure of the regularized tensor of the solution. Since the tensor depends continuously on the solution curve, the Riesz pressure is a continuous curve in L², and the limit of its spatial mollifications is a jointly measurable space-time pressure whose slices are the Riesz pressures.

theorem CKN.Leray.instFactLeENNRealOfNatOfRealReal_leanPool_1 : Fact (1 ≤ ENNReal.ofReal 2)

noncomputable def CKN.Leray.forcedTensorComp (T : ↥RealTensorL2) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : ℝ

A coordinate entry of a real tensor L² field, in physical coordinates.

Equations

• CKN.Leray.forcedTensorComp T i j x = ((↑↑T (WithLp.toLp 2 x)).ofLp i).ofLp j

theorem CKN.Leray.ofReal_two_eq : ENNReal.ofReal 2 = 2

theorem CKN.Leray.norm_forcedTensorComp_le (T : ↥RealTensorL2) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : ‖forcedTensorComp T i j x‖ ≤ ‖↑↑T (WithLp.toLp 2 x)‖

theorem CKN.Leray.memLp_forcedTensorComp (T : ↥RealTensorL2) (i j : Fin 3) : MeasureTheory.MemLp (forcedTensorComp T i j) (ENNReal.ofReal 2) MeasureTheory.volume

theorem CKN.Leray.eLpNorm_forcedTensorComp_sub_le (T T' : ↥RealTensorL2) (i j : Fin 3) : MeasureTheory.eLpNorm (forcedTensorComp T i j - forcedTensorComp T' i j) (ENNReal.ofReal 2) MeasureTheory.volume ≤ ENNReal.ofReal ‖T - T'‖

noncomputable def CKN.Leray.forcedPressureTensorLp (T : ↥RealTensorL2) : PressureTensorLp 2

The pressure tensor of a real tensor L² field, in physical coordinates.

Equations

• CKN.Leray.forcedPressureTensorLp T i j = MeasureTheory.MemLp.toLp (CKN.Leray.forcedTensorComp T i j) ⋯

theorem CKN.Leray.rieszPressureSlice_two_sub (F G : PressureTensorLp 2) : rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 F - rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 G = rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 (F - G)

theorem CKN.Leray.norm_forcedPressureTensorLp_sub_le (T T' : ↥RealTensorL2) (i j : Fin 3) : ‖(forcedPressureTensorLp T - forcedPressureTensorLp T') i j‖ ≤ ‖T - T'‖

theorem CKN.Leray.norm_forcedPressure_sub_le (T T' : ↥RealTensorL2) : ‖rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 (forcedPressureTensorLp T) - rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 (forcedPressureTensorLp T')‖ ≤ rieszPressureOperatorBound 2 rieszPressureSlice_two_sub._proof_1 * (9 * ‖T - T'‖)

The Riesz pressure of the tensor field is Lipschitz in the tensor.

theorem CKN.Leray.abs_mollify_sub_le {g g' : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hg' : MeasureTheory.MemLp g' 2 MeasureTheory.volume) {δ : ℝ} (hδ : 0 < δ) (x : Foundation.Parabolic.Vec3) : |mollify g δ hδ x - mollify g' δ hδ x| ≤ (MeasureTheory.eLpNorm (mollifier δ hδ) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (g - g') 2 MeasureTheory.volume).toReal

Mollifications of two square-integrable functions differ pointwise by at most the kernel norm times the L² distance.

noncomputable def CKN.Leray.forcedPressureCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (U : ℝ → ↥RealVectorL2) (t : ℝ) : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal 2) MeasureTheory.volume)

The Riesz pressure curve of the regularized tensor of a velocity curve.

Equations

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

theorem CKN.Leray.continuous_forcedPressureCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {U : ℝ → ↥RealVectorL2} (hU : Continuous U) : Continuous (forcedPressureCurve ρ ε hε U)

noncomputable def CKN.Leray.forcedQuadPressure (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (U : ℝ → ↥RealVectorL2) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The quadratic pressure field: the limit of the spatial mollifications of the Riesz pressure slices.

Equations

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

theorem CKN.Leray.memLp_rieszPressureSliceRepresentative_two (F : PressureTensorLp 2) : MeasureTheory.MemLp (rieszPressureSliceRepresentative 2 rieszPressureSlice_two_sub._proof_1 F) 2 MeasureTheory.volume

theorem CKN.Leray.forcedQuadPressure_slice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (U : ℝ → ↥RealVectorL2) (t : ℝ) : (fun (x : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε U (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 rieszPressureSlice_two_sub._proof_1 (forcedPressureTensorLp (regularizedMildTensor ρ ε hε (U t)))

theorem CKN.Leray.eLpNorm_rieszRep_sub (F G : PressureTensorLp 2) : MeasureTheory.eLpNorm (rieszPressureSliceRepresentative 2 rieszPressureSlice_two_sub._proof_1 F - rieszPressureSliceRepresentative 2 rieszPressureSlice_two_sub._proof_1 G) 2 MeasureTheory.volume = ENNReal.ofReal ‖rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 F - rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 G‖

theorem CKN.Leray.forcedQuadPressure_stronglyMeasurable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {U : ℝ → ↥RealVectorL2} (hU : Continuous U) : MeasureTheory.StronglyMeasurable (forcedQuadPressure ρ ε hε U)

The quadratic pressure field of a continuous velocity curve is jointly measurable.

theorem CKN.Leray.eLpNorm_rieszRep (F : PressureTensorLp 2) : MeasureTheory.eLpNorm (rieszPressureSliceRepresentative 2 rieszPressureSlice_two_sub._proof_1 F) 2 MeasureTheory.volume = ENNReal.ofReal ‖rieszPressureSlice 2 rieszPressureSlice_two_sub._proof_1 F‖

theorem CKN.Leray.lintegral_eLpNorm_real_slice_sq {μt : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μt] {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.StronglyMeasurable F) : ∫⁻ (t : ℝ), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume ^ 2 ∂μt = MeasureTheory.eLpNorm F 2 (MeasureTheory.volume.prod μt) ^ 2

Tonelli's formula for the squared L² norm of a real field on a product with a time measure.

theorem CKN.Leray.memLp_forcedQuadPressure_slab (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {U : ℝ → ↥RealVectorL2} (hU : Continuous U) (T : ℝ) : MeasureTheory.MemLp (forcedQuadPressure ρ ε hε U) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

The quadratic pressure field of a continuous velocity curve is square integrable on every bounded slab.

theorem CKN.Leray.regUniformVelocitySlice_ae_eq {U : ℝ → ↥RealVectorL2} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)) : regUniformVelocitySlice u t =ᵐ[MeasureTheory.volume] ↑↑(U t)

The velocity slice of a representative agrees almost everywhere with the curve on the Euclidean carrier.

theorem CKN.Leray.regMollifyVector_velocitySlice_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {U : ℝ → ↥RealVectorL2} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)) : regMollifyVector ρ ε hε (regUniformVelocitySlice u t) = regMollifyVector ρ ε hε ↑↑(U t)

theorem CKN.Leray.regPressureTensorSlice_ae_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {U : ℝ → ↥RealVectorL2} {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)) (i j : Fin 3) : regPressureTensorSlice ρ ε hε u t i j =ᵐ[MeasureTheory.volume] forcedTensorComp (regularizedMildTensor ρ ε hε (U t)) i j

The pressure tensor slice of a representative is the coordinate entry of the regularized tensor of the curve.