Difference bounds for the regularized quadratic term

These estimates supply the contraction constant in lem:reg-local-mild.

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

The bilinear scalar multiplication map on the Hilbert velocity space.

Equations

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

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

The continuous bilinear scalar multiplication map on Hilbert velocities.

Equations

• CKN.Leray.mildScalarVectorAction = CKN.Leray.mildScalarVectorActionLinear.mkContinuous₂ 1 CKN.Leray.mildScalarVectorAction._proof_1

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

The bilinear map forming the componentwise tensor product of two Hilbert vectors.

Equations

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

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

The continuous bilinear tensor-product map on Hilbert vectors.

Equations

• CKN.Leray.mildTensorOuterCLM = CKN.Leray.mildTensorOuterLinear.mkContinuous₂ 1 CKN.Leray.mildTensorOuterCLM._proof_1

noncomputable def CKN.Leray.regularizedMildMollifierConstant (ρ : RegMollifierProfile) (ε : ℝ) : ℝ

The scale-dependent L² to L∞ constant of convolution by the regularizing kernel. It is used in the quadratic estimate for eq:reg-mild.

Equations

• CKN.Leray.regularizedMildMollifierConstant ρ ε = (ENNReal.ofReal (ε ^ (-(3 / 2))) * MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume).toReal

def CKN.Leray.mildTensorProductField (f g : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) : Foundation.Parabolic.L2Vec3 → RealTensor3

The pointwise tensor product of two Hilbert-valued vector fields.

Equations

• CKN.Leray.mildTensorProductField f g x = CKN.Leray.regularizedTensorOuter (f x) (g x)

theorem CKN.Leray.regularizedMildTensor_sub_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u v : ↥RealVectorL2) : ‖regularizedMildTensor ρ ε hε u - regularizedMildTensor ρ ε hε v‖ ≤ regularizedMildMollifierConstant ρ ε * (‖u‖ + ‖v‖) * ‖u - v‖

The regularized quadratic tensor is locally Lipschitz from velocity L² to tensor L², with the constant used in lem:reg-local-mild.