Closedness of the regularized mild data space

The divergence-free carrier used in lem:reg-local-mild is closed in the real spatial L² norm.

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

The continuous coordinate identification for the Hilbert vector space used by mild solutions.

Equations

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

theorem CKN.Leray.realVectorL2Representative_sub_eLpNorm_le (u v : ↥RealVectorL2) : MeasureTheory.eLpNorm (realVectorL2Representative u - realVectorL2Representative v) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (↑↑(u - v)) 2 MeasureTheory.volume

The coordinate representative is controlled by the L² distance used for the closed divergence-free carrier in lem:reg-local-mild.

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

def CKN.Leray.regularizedMildJSubmodule : Submodule ℝ ↥RealVectorL2

The subspace of real L² velocities satisfying the regularized mild-solution J condition.

Equations

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

theorem CKN.Leray.regularizedMildJData_isClosed : IsClosed {u : ↥RealVectorL2 | RegularizedMildJData u}

The set of real L² fields in J is a closed linear subspace, as needed for the fixed-point space in lem:reg-local-mild.