Compact cutoffs for decaying Riesz potential tests

The cutoffs are taken from CKN's smooth ball cutoff API and are used to pass from compact to decaying tests in lem:riesz-duality.

def CKN.Leray.rieszPressurePotentialCutoffScale (n : ℕ) : ℝ

The spatial radius used by the compact approximations of a potential test.

Equations

• CKN.Leray.rieszPressurePotentialCutoffScale n = ↑n + 1

noncomputable def CKN.Leray.rieszPressurePotentialCutoffRadius (n : ℕ) : ℝ

The CKN cutoff radius whose inner ball has radius rieszPressurePotentialCutoffScale n.

Equations

• CKN.Leray.rieszPressurePotentialCutoffRadius n = 20 * CKN.Leray.rieszPressurePotentialCutoffScale n / 13

noncomputable def CKN.Leray.rieszPressurePotentialCutoff (n : ℕ) : Foundation.Parabolic.Vec3 → ℝ

The spatial cutoff in the compact approximation of a potential test.

Equations

• CKN.Leray.rieszPressurePotentialCutoff n = CKN.mollifiedBallCutoff 0 ⋯

noncomputable def CKN.Leray.rieszPressurePotentialCutoffTest (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (n : ℕ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The compactly supported approximation of a potential test.

Equations

• CKN.Leray.rieszPressurePotentialCutoffTest ψ n z = CKN.Leray.rieszPressurePotentialCutoff n z.1 * ψ z

theorem CKN.Leray.rieszPressurePotentialCutoffScale_ge_one (n : ℕ) : 1 ≤ rieszPressurePotentialCutoffScale n

The cutoff scales are uniformly bounded below by one, used by the noncompact-potential estimates.

theorem CKN.Leray.rieszPressurePotentialCutoffScale_pos (n : ℕ) : 0 < rieszPressurePotentialCutoffScale n

Every cutoff scale is positive, used by the noncompact-potential estimates.

theorem CKN.Leray.rieszPressurePotentialCutoffRadius_pos (n : ℕ) : 0 < rieszPressurePotentialCutoffRadius n

Every CKN cutoff radius is positive, used by the cutoff construction.

theorem CKN.Leray.rieszPressurePotentialCutoff_outer (n : ℕ) : 3 * rieszPressurePotentialCutoffRadius n / 4 = 15 * rieszPressurePotentialCutoffScale n / 13

The outer support radius of the cutoff is a fixed multiple of its scale, used by the noncompact-potential estimates.

theorem CKN.Leray.rieszPressurePotentialCutoff_eq_one (n : ℕ) {x : Foundation.Parabolic.Vec3} (hx : x ∈ euclideanBall 0 (rieszPressurePotentialCutoffScale n)) : rieszPressurePotentialCutoff n x = 1

The CKN spatial cutoff equals one on its growing inner ball.

theorem CKN.Leray.rieszPressurePotentialCutoff_bounds (n : ℕ) (x : Foundation.Parabolic.Vec3) : 0 ≤ rieszPressurePotentialCutoff n x ∧ rieszPressurePotentialCutoff n x ≤ 1

The CKN cutoff is between zero and one.

theorem CKN.Leray.rieszPressurePotentialCutoff_gradient_bound (n : ℕ) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : |spatialDeriv (rieszPressurePotentialCutoff n) i x| ≤ cutoffGradientConstant / rieszPressurePotentialCutoffScale n

The first coordinate derivatives of the cutoff have the scale bound needed for the noncompact-potential passage.

theorem CKN.Leray.rieszPressurePotentialCutoff_hessian_component_bound (n : ℕ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : |mixedSecond (rieszPressurePotentialCutoff n) i j x| ≤ cutoffSecondDerivativeConstant / rieszPressurePotentialCutoffScale n ^ 2

Every coordinate second derivative of the cutoff has the inverse-square scale bound needed by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialCutoff_derivatives_zero_on_inner (n : ℕ) {x : Foundation.Parabolic.Vec3} (hx : x ∈ euclideanClosedBall 0 (rieszPressurePotentialCutoffScale n)) : classicalGradient (rieszPressurePotentialCutoff n) x = 0 ∧ fderiv ℝ (classicalGradient (rieszPressurePotentialCutoff n)) x = 0

The first and second cutoff derivatives vanish on its inner ball.

theorem CKN.Leray.rieszPressurePotentialCutoffTest_contDiff {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (n : ℕ) : ContDiff ℝ (↑⊤) (rieszPressurePotentialCutoffTest ψ n)

The compact cutoff approximants are smooth whenever the potential test is smooth.

theorem CKN.Leray.rieszPressurePotentialCutoffTest_hasCompactSupport {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {K : Set ℝ} (hK : IsCompact K) (hzero : ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), ψ (x, t) = 0) (n : ℕ) : HasCompactSupport (rieszPressurePotentialCutoffTest ψ n)

The compact cutoff approximants have compact support when the test has compact time support.