The weak momentum identity on a finite mild interval

The zero-force regularized momentum identity transfers to a coordinate velocity satisfying the same mild equation on a finite interval.

@[reducible, inline]

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

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

Equations

• CKN.Leray.regularisedEquationIntervalWeakParabolicTopology = inferInstance

@[instance_reducible]

def CKN.Leray.regularisedIntervalWeakNormedAddCommGroup : 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.regularisedIntervalWeakNormedSpace : 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.regularisedInterval_weakMomentum (ρ : 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)) ⋯) (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))) (hPcontinuous : ContinuousOn (regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice) (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))) (φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * u z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

A same-velocity mild path satisfies the forced weak momentum identity on its finite regularity interval.