Cutoff

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.caccioppoli_spatial_cutoff_gradient_bound (x₀ : Foundation.Parabolic.Vec3) (ρ : ℝ) (hρ : 0 < ρ) (x : Foundation.Parabolic.Vec3) : vecEuclideanNorm (classicalGradient (mollifiedBallCutoff x₀ hρ) x) ≤ cutoffGradientConstant / ρ

theorem CKN.caccioppoli_spatial_cutoff_second_derivative_bound (x₀ : Foundation.Parabolic.Vec3) (ρ : ℝ) (hρ : 0 < ρ) (x : Foundation.Parabolic.Vec3) (i j : Fin 3) : |(fderiv ℝ (classicalGradient (mollifiedBallCutoff x₀ hρ)) x) (basisVec j) i| ≤ cutoffSecondDerivativeConstant / ρ ^ 2

theorem CKN.caccioppoli_cutoff_spatial_partial_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) : |spatialPartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) i z| ≤ cutoffGradientConstant / ρ

theorem CKN.caccioppoli_cutoff_time_partial_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : |timePartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) z| ≤ 32 / (R ^ 2 - (ρ / 2) ^ 2)

theorem CKN.caccioppoli_cutoff_second_spatial_partial_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) : |spatialSecondPartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) i j z| ≤ cutoffSecondDerivativeConstant / ρ ^ 2

theorem CKN.caccioppoli_cutoff_laplacian_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : |∑ i : Fin 3, spatialSecondPartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) i i z| ≤ 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)

theorem CKN.caccioppoli_cutoff_time_plus_laplacian_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : |timePartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) z + ∑ i : Fin 3, spatialSecondPartial (caccioppoliCutoff x₀ t₀ ρ R hρ hR) i i z| ≤ 32 / (R ^ 2 - (ρ / 2) ^ 2) + 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)

noncomputable def CKN.caccioppoliAsymmetricTimeCutoff (t₀ ρ ε t : ℝ) : ℝ

Temporal cutoff with separate backward-cylinder and forward regularization transition intervals.

Equations

• CKN.caccioppoliAsymmetricTimeCutoff t₀ ρ ε t = CKN.smoothTransitionProfile ((t - (t₀ - ρ ^ 2 / 2)) / (ρ ^ 2 / 4)) * CKN.smoothTransitionProfile ((t₀ + ε - t) / (ε / 2))

theorem CKN.caccioppoli_asymmetricTimeCutoff_smooth {t₀ ρ ε : ℝ} : 0 < ρ → 0 < ε → ContDiff ℝ (↑⊤) (caccioppoliAsymmetricTimeCutoff t₀ ρ ε)

theorem CKN.caccioppoli_asymmetricTimeCutoff_nonneg (t₀ ρ ε t : ℝ) : 0 ≤ caccioppoliAsymmetricTimeCutoff t₀ ρ ε t

theorem CKN.caccioppoli_asymmetricTimeCutoff_le_one (t₀ ρ ε t : ℝ) : caccioppoliAsymmetricTimeCutoff t₀ ρ ε t ≤ 1

theorem CKN.caccioppoli_asymmetricTimeCutoff_support_subset {t₀ ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : Function.support (caccioppoliAsymmetricTimeCutoff t₀ ρ ε) ⊆ Set.Ioo (t₀ - ρ ^ 2) (t₀ + ε)

theorem CKN.caccioppoli_asymmetricTimeCutoff_tsupport_subset {t₀ ρ ε r : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hεr : ε < r ^ 2) : tsupport (caccioppoliAsymmetricTimeCutoff t₀ ρ ε) ⊆ {t : ℝ | t < t₀ + r ^ 2}

theorem CKN.caccioppoli_asymmetricTimeCutoff_hasCompactSupport {t₀ ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : HasCompactSupport (caccioppoliAsymmetricTimeCutoff t₀ ρ ε)

theorem CKN.caccioppoli_asymmetricTimeCutoff_abs_deriv_le_on_left {t₀ ρ ε t : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (ht : t ≤ t₀) : |deriv (caccioppoliAsymmetricTimeCutoff t₀ ρ ε) t| ≤ 32 / ρ ^ 2

noncomputable def CKN.caccioppoliHeatCutoff (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (_hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

Product cutoff used to test the local energy inequality with a regularized backward heat kernel.

Equations

• CKN.caccioppoliHeatCutoff x₀ t₀ ρ ε hρ _hε z = CKN.mollifiedBallCutoff x₀ hρ z.1 * CKN.caccioppoliAsymmetricTimeCutoff t₀ ρ ε z.2

theorem CKN.caccioppoli_heat_cutoff_smooth (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) : ContDiff ℝ (↑⊤) (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε)

theorem CKN.caccioppoli_heat_cutoff_nonneg (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε z

theorem CKN.caccioppoli_heat_cutoff_le_one (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε z ≤ 1

theorem CKN.caccioppoli_heat_cutoff_support_subset (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) : Function.support (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) ⊆ euclideanBall x₀ (3 * ρ / 4) ×ˢ Set.Ioo (t₀ - ρ ^ 2) (t₀ + ε)

theorem CKN.caccioppoli_heat_cutoff_hasCompactSupport (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) : HasCompactSupport (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε)

theorem CKN.caccioppoli_heat_cutoff_time_support_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε r : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) : 0 < r → ∀ (hεr : ε < r ^ 2), tsupport (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) ⊆ {z : Foundation.Parabolic.Vec3 × ℝ | z.2 < t₀ + r ^ 2}

theorem CKN.caccioppoli_heat_cutoff_spatial_partial_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) : |spatialPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i z| ≤ cutoffGradientConstant / ρ

theorem CKN.caccioppoli_heat_cutoff_time_partial_bound_on_left (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (ht : z.2 ≤ t₀) : |timePartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) z| ≤ 32 / ρ ^ 2

theorem CKN.caccioppoli_heat_cutoff_second_spatial_partial_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) : |spatialSecondPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i j z| ≤ cutoffSecondDerivativeConstant / ρ ^ 2

theorem CKN.caccioppoli_heat_cutoff_laplacian_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : |∑ i : Fin 3, spatialSecondPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i i z| ≤ 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)

theorem CKN.caccioppoli_heat_cutoff_time_plus_laplacian_bound_on_left (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (ht : z.2 ≤ t₀) : |timePartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) z + ∑ i : Fin 3, spatialSecondPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i i z| ≤ 32 / ρ ^ 2 + 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)

theorem CKN.caccioppoli_asymmetricTimeCutoff_eq_one_on {t₀ ρ ε r t : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) (ht : t ∈ Set.Icc (t₀ - r ^ 2) (t₀ + ε / 2)) : caccioppoliAsymmetricTimeCutoff t₀ ρ ε t = 1