Canonical pressure on a regularized mild interval

The interval pressure is the Riesz pressure of the same clamped velocity path that occurs in its mild identity.

noncomputable def CKN.Leray.regularisedIntervalMildCurve (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 ≤ T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) : ℝ → ↥RealVectorL2

The spatial L² path represented by a coordinate field on a closed regularized mild interval. Values outside the interval use its endpoint.

Equations

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

noncomputable def CKN.Leray.regularisedIntervalCanonicalPressure (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 ≤ T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) : Foundation.Parabolic.ParabolicPoint → ℝ

The canonical Riesz pressure on a finite interval, built from its own clamped velocity path.

Equations

• CKN.Leray.regularisedIntervalCanonicalPressure ρ ε hε u T hT hSlice = CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regularisedIntervalMildCurve u T hT hSlice)

theorem CKN.Leray.regularisedIntervalCanonicalPressure_slice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 ≤ T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : (fun (x : Foundation.Parabolic.Vec3) => regularisedIntervalCanonicalPressure ρ ε hε u T hT hSlice (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regularisedIntervalCanonicalPressure_slice._proof_1 (forcedPressureTensorLp (regularizedMildTensor ρ ε hε (realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯)))

On each interval time slice, the canonical interval pressure is the Riesz representative of the tensor from that same velocity slice.