The spatial-temporal cutoff and its support estimates.

theorem CKN.parabolic_norm_eq_cutoff_norm (x : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm x = vecEuclideanNorm x

The cutoff used in the local energy estimate. The spatial factor is the two-derivative cutoff from the pressure construction; the temporal factor is given a separate outer radius so that its support can be placed inside the open time interval.

noncomputable def CKN.caccioppoliCutoff (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (_hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

Spatial and temporal cutoff for the centered Caccioppoli estimate.

Equations

• CKN.caccioppoliCutoff x₀ t₀ ρ R hρ _hR z = CKN.mollifiedBallCutoff x₀ hρ z.1 * CKN.timeCutoff t₀ (ρ / 2) R z.2

theorem CKN.caccioppoli_cutoff_time_parameters {ρ R : ℝ} (hρ : 0 < ρ) (hR : ρ / 2 < R) : 0 ≤ ρ / 2 ∧ ρ / 2 < R

theorem CKN.caccioppoli_cutoff_smooth (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) : ContDiff ℝ (↑⊤) (caccioppoliCutoff x₀ t₀ ρ R hρ hR)

theorem CKN.caccioppoli_cutoff_nonneg (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ caccioppoliCutoff x₀ t₀ ρ R hρ hR z

theorem CKN.caccioppoli_cutoff_eq_one_on (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) {z : Foundation.Parabolic.Vec3 × ℝ} (hx : z.1 ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) (ht : z.2 ∈ Set.Icc (t₀ - (ρ / 2) ^ 2) t₀) : caccioppoliCutoff x₀ t₀ ρ R hρ hR z = 1

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

theorem CKN.caccioppoli_cutoff_hasCompactSupport (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) : HasCompactSupport (caccioppoliCutoff x₀ t₀ ρ R hρ hR)

theorem CKN.caccioppoli_cutoff_time_support_bound (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ R r : ℝ) (hρ : 0 < ρ) (hR : ρ / 2 < R) : 0 < r → ∀ (hgapr : R ^ 2 - (ρ / 2) ^ 2 < r ^ 2), tsupport (caccioppoliCutoff x₀ t₀ ρ R hρ hR) ⊆ {z : Foundation.Parabolic.Vec3 × ℝ | z.2 < t₀ + r ^ 2}