Receding Diffusion Pairing Bound #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.diffusion_term_pairing_bound_fixed
{C h lam rc zc : ℝ}
(hC : 0 ≤ C)
(hh0 : 0 ≤ h)
(hh1 : h ≤ 1 / 2)
(hlam : 0 < lam)
(hdelta : lam ^ (2 * h) ≤ 1)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{K : Set (ℝ × ℝ)}
(hK : IsCompact K)
{τ : ℝ}
(htau : τ ≤ -1)
(hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder)
(ψ : ℝ × ℝ → ℝ)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hψU : tsupport ψ ⊆ interior K)
(B : ℝ)
(hB : 0 ≤ B)
(hψB : ∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B)
:
The diffusion-term pairing bound at a fixed zoom scale: the integral of
∂_R∂_R Θ_n + δ² ∂_Z∂_Z Θ_n, the diffusion term of zoomTheta_pde, against a test
function supported in the interior of a compact set K is bounded by 4C times the
bound B on ψ and its first two derivatives, times the volume of K.
theorem
CIV.diffusion_term_pairing_bound
{C h : ℝ}
(hC : 0 ≤ C)
(hh0 : 0 ≤ h)
(hh1 : h ≤ 1 / 2)
{rc zc : ℝ}
(lam : ℕ → ℝ)
(hlam_pos : ∀ (n : ℕ), 0 < lam n)
(hlam_le : ∀ᶠ (n : ℕ) in Filter.atTop, lam n ^ (2 * h) ≤ 1)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hb : AnisotropicBounds C h u)
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{K : Set (ℝ × ℝ)}
(hK : IsCompact K)
{τ : ℝ}
(htau : τ ≤ -1)
(hmem : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, zoomPointRec (lam n) h rc zc (y, τ) ∈ unitCylinder)
:
∃ (C₀ : ℝ),
0 ≤ C₀ ∧ ∀ (ψ : ℝ × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ interior K →
∀ (B : ℝ),
0 ≤ B →
(∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) →
∀ᶠ (n : ℕ) in Filter.atTop, |∫ (y : ℝ × ℝ), (dr (dr fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ) + (lam n ^ (2 * h)) ^ 2 * dz (dz fun (q : (ℝ × ℝ) × ℝ) => zoomTheta (lam n) h rc zc u q) (y, τ)) * ψ y| ≤ C₀ * B
The eventual-in-n pairing bound for the diffusion term: C₀ := 4C is chosen before
n, matching the eventual form of the time-pairing estimate hpair.