The regularized momentum equation on a finite interval: the core

(R3) of thm:regularised on [0, T]: a velocity that satisfies the regularized mild equation eq:reg-mild on [0, T], and has continuous slices and classical regularity on (0, T], solves the regularized momentum equation pointwise on (0, T). This holds in divergence form and, since J_ε u is divergence free, in transport form. The pressure is the canonical Riesz pressure of each slice, as in (R4). The interval weak momentum identity is tested against scalar components. After integration by parts, the continuous residual vanishes.

@[reducible, inline]

noncomputable abbrev CKN.Leray.regularisedR3FinalBaseTopology : TopologicalSpace Foundation.Parabolic.ParabolicPoint

The product topology on parabolic space-time points used in this weak identity.

Equations

• CKN.Leray.regularisedR3FinalBaseTopology = inferInstance

@[instance_reducible]

def CKN.Leray.regularisedR3FinalProductNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group used for spatial and temporal regularity.

Equations

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

@[instance_reducible]

noncomputable def CKN.Leray.regularisedR3FinalProductNormedSpace : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The product real normed space used for spatial and temporal derivatives.

Equations

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

theorem CKN.Leray.regularisedR3Final_core (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (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) (hL2Continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hDivFree : ∀ t ∈ Set.Icc 0 T, IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hMild : ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ⋯ (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε (regularisedIntervalMildCurve u T ⋯ hSlice)) t) (hUcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDcontinuous : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDDcontinuous : ∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDtcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hPcontinuous : ContinuousOn (regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDpcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hUjoint : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioc 0 T), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, z.2)) z.1) (hPdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioc 0 T), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice (x, z.2)) z.1) : (∀ z ∈ spaceTimeSet Set.univ (Set.Ioo 0 T), ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) j z + ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u y j * u y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z = 0) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioo 0 T), ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) j z + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z = 0) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), (fun (x : Foundation.Parabolic.Vec3) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regularisedR3Final_core._proof_55 (forcedPressureTensorLp (regularizedMildTensor ρ ε hε (realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯)))

The interval weak momentum identity determines the pointwise equation and the canonical pressure of the regularized mild path (thm:regularised).