Radial truncation of the regularized tensor

To solve eq:reg-mild-forced on a whole interval at once, the velocity in the regularized tensor is first retracted onto a ball of radius R. The retraction is a scalar multiple of the velocity with factor in [0, 1], it is 2-Lipschitz, and it is the identity inside the ball; the truncated tensor is therefore globally Lipschitz. The energy bound of lem:regularised-forced later shows that the truncation is inactive.

noncomputable def CKN.Leray.forcedTruncFactor (R : ℝ) (v : ↥RealVectorL2) : ℝ

The radial truncation factor min(1, R/‖v‖).

Equations

• CKN.Leray.forcedTruncFactor R v = if ‖v‖ ≤ R then 1 else R / ‖v‖

noncomputable def CKN.Leray.forcedTrunc (R : ℝ) (v : ↥RealVectorL2) : ↥RealVectorL2

The radial retraction onto the ball of radius R.

Equations

• CKN.Leray.forcedTrunc R v = CKN.Leray.forcedTruncFactor R v • v

theorem CKN.Leray.forcedTruncFactor_nonneg {R : ℝ} (hR : 0 ≤ R) (v : ↥RealVectorL2) : 0 ≤ forcedTruncFactor R v

theorem CKN.Leray.forcedTruncFactor_le_one (R : ℝ) (v : ↥RealVectorL2) : forcedTruncFactor R v ≤ 1

theorem CKN.Leray.forcedTrunc_of_norm_le {R : ℝ} {v : ↥RealVectorL2} (hv : ‖v‖ ≤ R) : forcedTrunc R v = v

theorem CKN.Leray.norm_forcedTrunc_le {R : ℝ} (hR : 0 ≤ R) (v : ↥RealVectorL2) : ‖forcedTrunc R v‖ ≤ R

theorem CKN.Leray.abs_forcedTruncFactor_sub_mul_le {R : ℝ} (hR : 0 ≤ R) (v w : ↥RealVectorL2) : |forcedTruncFactor R v - forcedTruncFactor R w| * ‖w‖ ≤ |‖v‖ - ‖w‖|

The truncation factors of two vectors differ, after multiplication by the second norm, by at most the difference of the norms.

theorem CKN.Leray.norm_forcedTrunc_sub_le {R : ℝ} (hR : 0 ≤ R) (v w : ↥RealVectorL2) : ‖forcedTrunc R v - forcedTrunc R w‖ ≤ 2 * ‖v - w‖

The radial retraction is 2-Lipschitz.

noncomputable def CKN.Leray.forcedTruncTensor (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (R : ℝ) (v : ↥RealVectorL2) : ↥RealTensorL2

The regularized tensor of the truncated velocity.

Equations

• CKN.Leray.forcedTruncTensor ρ ε hε R v = CKN.Leray.regularizedMildTensor ρ ε hε (CKN.Leray.forcedTrunc R v)

theorem CKN.Leray.norm_forcedTruncTensor_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (hR : 0 ≤ R) (v : ↥RealVectorL2) : ‖forcedTruncTensor ρ ε hε R v‖ ≤ regularizedMildMollifierConstant ρ ε * R ^ 2

theorem CKN.Leray.norm_forcedTruncTensor_sub_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (hR : 0 ≤ R) (v w : ↥RealVectorL2) : ‖forcedTruncTensor ρ ε hε R v - forcedTruncTensor ρ ε hε R w‖ ≤ 4 * regularizedMildMollifierConstant ρ ε * R * ‖v - w‖