Cutoffs for whole-space transport pairings

The spatial cutoff used in the energy calculation has compact support, equals one on the inner ball, and has a derivative bounded by the inverse radius.

noncomputable def CKN.Leray.regularisedEnergyCutoff (R : ℝ) : Foundation.Parabolic.Vec3 → ℝ

A cutoff equal to one on the radius R ball and supported within the radius 2R ball.

Equations

• CKN.Leray.regularisedEnergyCutoff R = CKN.canonicalBallCutoff 0 R (2 * R)

theorem CKN.Leray.regularisedEnergyCutoff_eq_one_of_mem_ball (R : ℝ) (hR : 0 < R) (x : Foundation.Parabolic.Vec3) (hx : x ∈ euclideanBall 0 R) : regularisedEnergyCutoff R x = 1

The energy cutoff is one in its inner ball.

theorem CKN.Leray.regularisedEnergyCutoff_mem_unitInterval (R : ℝ) (x : Foundation.Parabolic.Vec3) : 0 ≤ regularisedEnergyCutoff R x ∧ regularisedEnergyCutoff R x ≤ 1

The energy cutoff takes values in the unit interval.

theorem CKN.Leray.regularisedEnergyCutoff_smooth (R : ℝ) (hR : 0 < R) : ContDiff ℝ (↑⊤) (regularisedEnergyCutoff R)

The energy cutoff is smooth for positive radius.

theorem CKN.Leray.regularisedEnergyCutoff_compact (R : ℝ) (hR : 0 < R) : HasCompactSupport (regularisedEnergyCutoff R)

The energy cutoff has compact support for positive radius.

theorem CKN.Leray.regularisedEnergyCutoff_derivative_bound (R : ℝ) (hR : 0 < R) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : |(fderiv ℝ (regularisedEnergyCutoff R) x) (basisVec i)| ≤ 32 / R

Each coordinate derivative of the energy cutoff is bounded by the inverse cutoff radius.