Divergence free range of the mild Stokes integral

The closed Leray data space is preserved by the time-integrated Stokes term in lem:reg-local-mild.

theorem CKN.Leray.instFactNeENNRealOfNatTop_leanPool_1 : Fact (2 ≠ ⊤)

def CKN.Leray.mildIntegralCoordinateEquiv : Foundation.Parabolic.L2Vec3 ≃L[ℝ] Foundation.Parabolic.Vec3

The continuous identification of Hilbert vectors with coordinate triples for the mild integral.

Equations

• CKN.Leray.mildIntegralCoordinateEquiv = PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ

theorem CKN.Leray.mildIntegralWeakPairing_integrable (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsWeakDivFreeL2 a) (ψ : WeakTestFunction Set.univ) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, a x i * ψ.partialDeriv i x) MeasureTheory.volume

def CKN.Leray.mildIntegralJSubmodule : Submodule ℝ ↥RealVectorL2

The subspace of L² velocities satisfying the regularized mild integral J condition.

Equations

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

theorem CKN.Leray.regularizedMildJData_sub {u v : ↥RealVectorL2} (hu : RegularizedMildJData u) (hv : RegularizedMildJData v) : RegularizedMildJData (u - v)

The real Leray data used in the regularized mild flow are closed under subtraction.

theorem CKN.Leray.regularizedMildStokesIntegral_isInJ (F : ℝ → ↥RealTensorL2) (hF : Continuous F) (C T t : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (hT : 0 ≤ T) (hTpos : 0 < T) (ht : 0 ≤ t) (htT : t ≤ T) : RegularizedMildJData (regularizedMildStokesIntegral F t)

The Stokes time integral takes values in the closed divergence free space used for trajectories in lem:reg-local-mild.