Distance-weighted absorption up to the top time #
A local estimate |g(x, s)| ≤ c₁ ρ Λ + c₂ / ρ, valid whenever |g| ≤ Λ on the backward window
B_bar(x, 2ρ) × [s - ρ², s] inside an annulus, yields a bound for g on every smaller annulus that
is uniform up to the top time t = 0. The circular term carries the small factor ρ; it is
absorbed with the weight d(x) = min(|x| - a, b - |x|). This is the device that makes the
interior estimates of the proof of lem:aniso:annulus uniform up to the blow-up time.
The Euclidean norm is 1-Lipschitz.
A closed Euclidean annulus times a compact time interval is compact.
theorem
CIV.exists_bound_of_weighted_absorption
{g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{a b a' b' t₁ τ c₁ c₂ : ℝ}
(hab : 0 ≤ a ∧ a < a' ∧ a' < b' ∧ b' < b ∧ b ≤ 1)
(hτ : 0 < τ)
(ht₁ : t₁ < 0)
(hc₁ : 0 ≤ c₁)
(hc₂ : 0 ≤ c₂)
(hcont :
ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z)
({x : CKN.Foundation.Parabolic.Vec3 | a ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ b} ×ˢ Set.Ico (t₁ - τ) 0))
(hlocal :
∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ Λ : ℝ),
a < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < b →
t₁ ≤ s →
s < 0 →
0 < ρ →
ρ ≤ 1 →
ρ ^ 2 ≤ τ →
(∀ (y : CKN.Foundation.Parabolic.Vec3),
CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * ρ →
a < CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y < b) →
(∀ (y : CKN.Foundation.Parabolic.Vec3) (s' : ℝ),
CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ 2 * ρ →
s - ρ ^ 2 ≤ s' → s' ≤ s → |g (y, s')| ≤ Λ) →
|g (x, s)| ≤ c₁ * ρ * Λ + c₂ / ρ)
:
∃ (K : ℝ),
∀ (x : CKN.Foundation.Parabolic.Vec3),
a' < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < b' → ∀ (s : ℝ), t₁ ≤ s → s < 0 → |g (x, s)| ≤ K
Distance-weighted absorption: a local circular estimate with a small factor ρ on backward
windows gives a bound on every smaller annulus, uniform up to the top time.