Space-time cutoff for a local energy estimate #
This module combines the spatial and temporal weights for lem:caccioppoli.
noncomputable def
ESS.caccioppoliSpaceTimeWeight
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t r ε : ℝ)
(q : CKN.Foundation.Parabolic.Vec3 × ℝ)
:
The product of the spatial and time cutoffs used in the weighted energy estimate.
Equations
- ESS.caccioppoliSpaceTimeWeight x₀ t r ε q = ESS.caccioppoliSpatialWeight x₀ r q.1 ^ 2 * ESS.caccioppoliTimeWeight t r ε q.2 ^ 2
Instances For
theorem
ESS.caccioppoliSpaceTimeWeight_properties
{x₀ : CKN.Foundation.Parabolic.Vec3}
{t r ε : ℝ}
(hr : 0 < r)
(hε : 0 < ε)
(hεsmall : 4 * ε < r ^ 2)
:
ContDiff ℝ (↑⊤) (caccioppoliSpaceTimeWeight x₀ t r ε) ∧ HasCompactSupport (caccioppoliSpaceTimeWeight x₀ t r ε) ∧ tsupport (caccioppoliSpaceTimeWeight x₀ t r ε) ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (2 * r) ×ˢ Set.Ioo t (t + 4 * r ^ 2) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ),
0 ≤ caccioppoliSpaceTimeWeight x₀ t r ε q ∧ caccioppoliSpaceTimeWeight x₀ t r ε q ≤ 1) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3),
(fderiv ℝ (caccioppoliSpaceTimeWeight x₀ t r ε) q) (CKN.basisVec j, 0) = 2 * caccioppoliSpatialWeight x₀ r q.1 * CKN.classicalGradient (caccioppoliSpatialWeight x₀ r) q.1 j * caccioppoliTimeWeight t r ε q.2 ^ 2) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ),
q.2 ≤ t + r ^ 2 → 0 ≤ (fderiv ℝ (caccioppoliSpaceTimeWeight x₀ t r ε) q) (0, 1)) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ),
t + r ^ 2 ≤ q.2 → -(1600 / 199) / r ^ 2 ≤ (fderiv ℝ (caccioppoliSpaceTimeWeight x₀ t r ε) q) (0, 1)) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ),
CKN.Foundation.Parabolic.vec3EuclideanNorm (q.1 - x₀) < r →
t + 2 * ε ≤ q.2 → q.2 ≤ t + r ^ 2 → caccioppoliSpaceTimeWeight x₀ t r ε q = 1) ∧ ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ),
∑ j : Fin 3, (fderiv ℝ (caccioppoliSpaceTimeWeight x₀ t r ε) q) (CKN.basisVec j, 0) ^ 2 ≤ 4 * (400 / 99) ^ 2 / r ^ 2 * caccioppoliSpaceTimeWeight x₀ t r ε q
Properties of the product cutoff used in lem:caccioppoli.