Cutoff #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Fixed cutoff equal to one on the inner pressure ball and supported in the outer ball.
Equations
- CKN.fixedCutoff = CKN.canonicalBallCutoff 0 (13 / 20) (3 / 4)
Instances For
theorem
CKN.exists_cutoff :
∃ (C₁₀ : ℕ → ℝ),
∀ (x₀ : Foundation.Parabolic.Vec3) (ρ : ℝ),
0 < ρ →
∃ (η : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) η ∧ HasCompactSupport η ∧ (∀ (x : Foundation.Parabolic.Vec3), 0 ≤ η x ∧ η x ≤ 1) ∧ (∀ x ∈ Foundation.Parabolic.vec3Ball x₀ (13 * ρ / 20), η x = 1) ∧ tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4) ∧ ∀ (k : ℕ) (x : Foundation.Parabolic.Vec3), ‖iteratedFDeriv ℝ k η x‖ ≤ C₁₀ k * ρ ^ (-↑k)
theorem
CKN.cutoff_annulus_separation
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
{x₀ x y : Foundation.Parabolic.Vec3}
(hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r)
(hy : y ∈ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4) \ Foundation.Parabolic.vec3Ball x₀ (13 * ρ / 20))
: