Local energy estimate for a parabolic differential inequality

Smooth compactly supported spatial and time weights for the local energy estimate lem:caccioppoli, with explicit derivative bounds.

noncomputable def ESS.caccioppoliSpatialWeight (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (y : CKN.Foundation.Parabolic.Vec3) : ℝ

A compactly supported spatial weight for lem:caccioppoli.

Equations

• ESS.caccioppoliSpatialWeight x₀ r y = CKN.smoothTransitionProfile ((199 / 100 * r - CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x₀)) / (99 / 100 * r))

noncomputable def ESS.lowerTimeCutoff (t ε s : ℝ) : ℝ

The lower time cutoff in the compactly supported Caccioppoli weight.

Equations

• ESS.lowerTimeCutoff t ε s = CKN.smoothTransitionProfile ((s - (t + ε)) / ε)

noncomputable def ESS.upperTimeCutoff (t r s : ℝ) : ℝ

The upper time cutoff in the compactly supported Caccioppoli weight.

Equations

• ESS.upperTimeCutoff t r s = CKN.smoothTransitionProfile ((t + 3 * r ^ 2 - s) / (199 / 100 * r ^ 2))

noncomputable def ESS.caccioppoliTimeWeight (t r ε s : ℝ) : ℝ

A compactly supported time weight for lem:caccioppoli.

Equations

• ESS.caccioppoliTimeWeight t r ε s = ESS.lowerTimeCutoff t ε s * ESS.upperTimeCutoff t r s

theorem ESS.caccioppoliSpatialWeight_properties (x₀ : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) : ContDiff ℝ (↑⊤) (caccioppoliSpatialWeight x₀ r) ∧ HasCompactSupport (caccioppoliSpatialWeight x₀ r) ∧ tsupport (caccioppoliSpatialWeight x₀ r) ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (2 * r) ∧ (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x₀) < r → caccioppoliSpatialWeight x₀ r y = 1) ∧ ∀ (y : CKN.Foundation.Parabolic.Vec3), 0 ≤ caccioppoliSpatialWeight x₀ r y ∧ caccioppoliSpatialWeight x₀ r y ≤ 1 ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.classicalGradient (caccioppoliSpatialWeight x₀ r) y) ≤ 400 / 99 / r

Properties of the spatial weight used in the local energy estimate.

theorem ESS.caccioppoliTimeWeight_properties {t r ε : ℝ} (hε : 0 < ε) (hr : 0 < r) (hεsmall : 4 * ε < r ^ 2) : ContDiff ℝ (↑⊤) (caccioppoliTimeWeight t r ε) ∧ HasCompactSupport (caccioppoliTimeWeight t r ε) ∧ tsupport (caccioppoliTimeWeight t r ε) ⊆ Set.Icc (t + ε) (t + 3 * r ^ 2) ∧ (∀ (s : ℝ), t + 2 * ε ≤ s → s ≤ t + r ^ 2 → caccioppoliTimeWeight t r ε s = 1) ∧ (∀ (s : ℝ), 0 ≤ caccioppoliTimeWeight t r ε s ∧ caccioppoliTimeWeight t r ε s ≤ 1) ∧ (∀ s ≤ t + r ^ 2, 0 ≤ deriv (caccioppoliTimeWeight t r ε) s) ∧ ∀ (s : ℝ), t + r ^ 2 ≤ s → deriv (caccioppoliTimeWeight t r ε) s ≤ 0 ∧ |deriv (caccioppoliTimeWeight t r ε) s| ≤ 800 / 199 / r ^ 2

Properties of the time weight used in the local energy estimate.