The regularized quadratic term

The tensor-valued nonlinearity used in eq:reg-mild and lem:reg-local-mild.

def CKN.Leray.localScalarVectorActionLinear : ℝ →ₗ[ℝ] Foundation.Parabolic.L2Vec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3

The bilinear scalar multiplication map on the local Hilbert velocity space.

Equations

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

noncomputable def CKN.Leray.localScalarVectorAction : ℝ →L[ℝ] Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The continuous scalar multiplication map on local Hilbert velocities.

Equations

• CKN.Leray.localScalarVectorAction = CKN.Leray.localScalarVectorActionLinear.mkContinuous₂ 1 CKN.Leray.localScalarVectorAction._proof_1

theorem CKN.Leray.regMollifyVector_add (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f g : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : regMollifyVector ρ ε hε (f + g) = regMollifyVector ρ ε hε f + regMollifyVector ρ ε hε g

Regularized convolution is linear on vector L² inputs.

def CKN.Leray.regularizedTensorOuter (v u : Foundation.Parabolic.L2Vec3) : RealTensor3

The pointwise tensor product (v_i u_j)_{i,j} in the Euclidean three-component carriers of eq:reg-mild.

Equations

• CKN.Leray.regularizedTensorOuter v u = WithLp.toLp 2 fun (i : Fin 3) => WithLp.toLp 2 fun (j : Fin 3) => v.ofLp i * u.ofLp j

theorem CKN.Leray.regularizedTensorOuter_norm (v u : Foundation.Parabolic.L2Vec3) : ‖regularizedTensorOuter v u‖ = ‖v‖ * ‖u‖

The Euclidean tensor norm of a rank-one tensor is the product of the Euclidean vector norms.

def CKN.Leray.regularizedTensorOuterLinear : Foundation.Parabolic.L2Vec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3 →ₗ[ℝ] RealTensor3

The bilinear map sending two Hilbert vectors to their regularized componentwise tensor product.

Equations

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

noncomputable def CKN.Leray.regularizedTensorOuterCLM : Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3 →L[ℝ] RealTensor3

The continuous bilinear tensor product on Euclidean vector values.

Equations

• CKN.Leray.regularizedTensorOuterCLM = CKN.Leray.regularizedTensorOuterLinear.mkContinuous₂ 1 CKN.Leray.regularizedTensorOuterCLM._proof_1

noncomputable def CKN.Leray.regularizedMildTensorField (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : ↥RealVectorL2) : Foundation.Parabolic.L2Vec3 → RealTensor3

The raw tensor field in the regularized mild equation.

Equations

• CKN.Leray.regularizedMildTensorField ρ ε hε u x = CKN.Leray.regularizedTensorOuter (CKN.Leray.regMollifyVector ρ ε hε (↑↑u) x) (↑↑u x)

theorem CKN.Leray.regularizedMildTensorField_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : ↥RealVectorL2) : MeasureTheory.MemLp (regularizedMildTensorField ρ ε hε u) 2 MeasureTheory.volume

noncomputable def CKN.Leray.regularizedMildTensor (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : ↥RealVectorL2) : ↥RealTensorL2

The nonlinearity in eq:reg-mild belongs to tensor-valued L² and has the source's quadratic norm bound.

Equations

• CKN.Leray.regularizedMildTensor ρ ε hε u = MeasureTheory.MemLp.toLp (CKN.Leray.regularizedMildTensorField ρ ε hε u) ⋯

theorem CKN.Leray.regularizedMildTensor_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : ↥RealVectorL2) : ‖regularizedMildTensor ρ ε hε u‖ ≤ (ENNReal.ofReal (ε ^ (-(3 / 2))) * MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume).toReal * ‖u‖ ^ 2

The nonlinearity in eq:reg-mild is bounded quadratically in L².