Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegTailsCutoff

Exterior cutoffs for the regularized velocity tail #

The compact cutoffs approximate a smooth exterior weight whose gradient is bounded by the inverse width of its transition annulus.

source
noncomputable def CKN.Leray.regTailsExteriorWeight (R1 R2 : ℝ) :
Foundation.Parabolic.Vec3 → ℝ

A smooth weight that vanishes on the inner ball and equals one outside the outer ball.

Equations
Instances For
    source
    theorem CKN.Leray.regTailsExteriorWeight_smooth {R1 R2 : ℝ} (hR1 : 0 < R1) (hR12 : R1 < R2) :
    ContDiff ℝ (↑⊤) (regTailsExteriorWeight R1 R2)

    The exterior weight is smooth.

    source
    theorem CKN.Leray.regTailsExteriorWeight_unit {R1 R2 : ℝ} (x : Foundation.Parabolic.Vec3) :
    0 ≤ regTailsExteriorWeight R1 R2 x ∧ regTailsExteriorWeight R1 R2 x ≤ 1

    The exterior weight lies in the unit interval.

    source
    theorem CKN.Leray.regTailsExteriorWeight_zero_inner {R1 R2 : ℝ} (hR1 : 0 < R1) (hR12 : R1 < R2) {x : Foundation.Parabolic.Vec3} (hx : Foundation.Parabolic.vec3EuclideanNorm x ≤ R1) :
    regTailsExteriorWeight R1 R2 x = 0

    The exterior weight vanishes through the inner ball.

    source
    theorem CKN.Leray.regTailsExteriorWeight_one_outer {R1 R2 : ℝ} (hR1 : 0 ≤ R1) (hR12 : R1 < R2) {x : Foundation.Parabolic.Vec3} (hx : R2 ≤ Foundation.Parabolic.vec3EuclideanNorm x) :
    regTailsExteriorWeight R1 R2 x = 1

    The exterior weight equals one outside the outer ball.

    source
    theorem CKN.Leray.regTailsExteriorWeight_derivative_bound {R1 R2 : ℝ} (hR1 : 0 ≤ R1) (hR12 : R1 < R2) (i : Fin 3) (x : Foundation.Parabolic.Vec3) :
    |spatialDeriv (regTailsExteriorWeight R1 R2) i x| ≤ 64 / (R2 - R1)

    Each coordinate derivative of the exterior weight is controlled by the inverse width of its transition annulus.

    source
    theorem CKN.Leray.regTails_compact_exterior_cutoffs {R1 R2 : ℝ} (hR1 : 0 < R1) (hR12 : R1 < R2) :
    ∃ (f : Foundation.Parabolic.Vec3 → ℝ), f = regTailsExteriorWeight R1 R2 ∧ (∀ (x : Foundation.Parabolic.Vec3), 0 ≤ f x ∧ f x ≤ 1) ∧ (∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm x ≤ R1 → f x = 0) ∧ (∀ (x : Foundation.Parabolic.Vec3), R2 ≤ Foundation.Parabolic.vec3EuclideanNorm x → f x = 1) ∧ (∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), |spatialDeriv f i x| ≤ 64 / (R2 - R1)) ∧ ∀ (N : ℝ), R2 ≤ N → ∃ (q : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) q ∧ HasCompactSupport q ∧ (∀ (x : Foundation.Parabolic.Vec3), 0 ≤ q x ∧ q x ≤ 1) ∧ (∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm x < N → q x = f x) ∧ (∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), spatialDeriv q i x = spatialDeriv f i x * regularisedEnergyCutoff N x + f x * spatialDeriv (regularisedEnergyCutoff N) i x) ∧ ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), |spatialDeriv (regularisedEnergyCutoff N) i x| ≤ 32 / N

    Compact cutoffs of the exterior weight. Their extra derivative is the vanishing outer-boundary error used when the compact support expands.