Building blocks for the annular kernel integration-by-parts bound

Prerequisites for a kernel estimate of the interior estimates of lem:aniso:annulus (∫ ∂ₗN(x-y) D^{γ₁}χ(y) D^{γ₂}g(y,t) dy, bounded using only |g| ≤ M, no derivative bound on g): a Vec3-level mirror of CIV.multiPartial built from CKN.spatialDeriv (multiPartialVec3), its deterministic peel (shared with CIV.multiPartial via the same peelDir/peelRest, so the two peel in lockstep), the ρ-scaling bound on multiPartial of the ball cutoff at any order, the Euclidean-norm bound on the Newtonian kernel gradient differentiated up to two further times, and the fact that CIV.multiPartial g γ is smooth on any open set on which g is smooth (generalizing CIV.contDiffOn_spatialPartial from the unit cylinder to an arbitrary open set). The integration-by-parts argument that moves the γ₂ derivatives off g is in CIV/Prerequisites/Serrin/AnnularKernelBound.lean.

Part 0: a Vec3-level mirror of multiPartial, and its scaling bound

noncomputable def CIV.multiPartialVec3 (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (γ : Fin 3 → ℕ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The Vec3-level mirror of multiPartial, built from CKN.spatialDeriv instead of CIV.spatialPartial.

Equations

• One or more equations did not get rendered due to their size.

def CIV.peelDir (γ : Fin 3 → ℕ) : Fin 3

The direction peeled off γ by the deterministic outermost-nonzero-exponent rule.

Equations

• CIV.peelDir γ = if γ 0 ≠ 0 then 0 else if γ 1 ≠ 0 then 1 else 2

def CIV.peelRest (γ : Fin 3 → ℕ) : Fin 3 → ℕ

The multi-index left after peeling peelDir γ off γ.

Equations

• CIV.peelRest γ = Function.update γ (CIV.peelDir γ) (γ (CIV.peelDir γ) - 1)

theorem CIV.multiPartialVec3_peel_det {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (k : CKN.Foundation.Parabolic.Vec3 → ℝ) : multiPartialVec3 k γ = CKN.spatialDeriv (multiPartialVec3 k (peelRest γ)) (peelDir γ)

The deterministic peel: the same direction and remainder work for every function k.

theorem CIV.peelRest_order {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) : peelRest γ 0 + peelRest γ 1 + peelRest γ 2 + 1 = γ 0 + γ 1 + γ 2

theorem CIV.multiPartialVec3_peel {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (k : CKN.Foundation.Parabolic.Vec3 → ℝ) : ∃ (j : Fin 3) (γ' : Fin 3 → ℕ), γ' 0 + γ' 1 + γ' 2 + 1 = γ 0 + γ 1 + γ 2 ∧ multiPartialVec3 k γ = CKN.spatialDeriv (multiPartialVec3 k γ') j

A nonzero spatial multi-index derivative of a Vec3 function peels one derivative off the outermost nonvanishing exponent.

Part 0b: smoothness and the scale-shift identity for multiPartialVec3

theorem CIV.contDiff_multiPartialVec3 {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : ContDiff ℝ (↑⊤) k) (γ : Fin 3 → ℕ) : ContDiff ℝ (↑⊤) (multiPartialVec3 k γ)

Part 0c: the deterministic peel for CIV.multiPartial, and the lift bridge

theorem CIV.multiPartial_peel_det {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : multiPartial g γ = CKN.spatialPartial (multiPartial g (peelRest γ)) (peelDir γ)

The deterministic peel for CIV.multiPartial, using the same peelDir/peelRest as multiPartialVec3, so the two peel in lockstep.

theorem CIV.multiPartial_lift_eq_aux (n : ℕ) (γ : Fin 3 → ℕ) : γ 0 + γ 1 + γ 2 = n → ∀ (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint), multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => k w.1) γ z = multiPartialVec3 k γ z.1

CIV.multiPartial of a lifted, time-independent Vec3 function is the lift of its Vec3-level mirror multiPartialVec3.

theorem CIV.multiPartial_lift_eq (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (γ : Fin 3 → ℕ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => k w.1) γ z = multiPartialVec3 k γ z.1

Part 0d: the ρ-scaling bound on multiPartial of the cutoff, at any order

theorem CIV.hasCompactSupport_multiPartialVec3 {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : HasCompactSupport k) (γ : Fin 3 → ℕ) : HasCompactSupport (multiPartialVec3 k γ)

theorem CIV.exists_bound_multiPartialVec3_serrinBallCutoff (γ : Fin 3 → ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3), |multiPartialVec3 (serrinBallCutoff 0 1) γ z| ≤ C

Every multiPartialVec3 derivative of the fixed unit cutoff is bounded, uniformly in the point (a fixed, x- and ρ-independent constant).

theorem CIV.exists_bound_multiPartial_serrinBallCutoff_scaled (x : CKN.Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (γ : Fin 3 → ℕ) (t : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : CKN.Foundation.Parabolic.Vec3), |multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1) γ (y, t)| ≤ C / ρ ^ (γ 0 + γ 1 + γ 2)

The ρ-scaling bound: every nonzero-or-zero order multiPartial derivative of the ball cutoff serrinBallCutoff x ρ is bounded by an absolute constant (depending only on the order) times ρ^{-n}.

Part 0e: Euclidean-norm bounds on the Newtonian kernel gradient, orders 1-3

theorem CIV.abs_multiPartialVec3_spatialDeriv_newtonianKernel_le (l : Fin 3) (β : Fin 3 → ℕ) (hβ : β 0 + β 1 + β 2 ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3), z ≠ 0 → |multiPartialVec3 (CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel l) β z| ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm z ^ (2 + (β 0 + β 1 + β 2)))⁻¹

The Newtonian kernel gradient, differentiated up to two further times, is bounded in terms of the Euclidean distance to the origin.

Part 1: smoothness of multiPartial g β on an open set, for general O

theorem CIV.contDiffOn_spatialPartial_openSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {O : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hO : IsOpen O) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) O) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial g i z) O

theorem CIV.contDiffOn_multiPartial_open {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {O : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hO : IsOpen O) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) O) (γ : Fin 3 → ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => multiPartial g γ z) O

CIV.multiPartial g γ, jointly in z, is smooth on any open set on which g is smooth.

theorem CIV.contDiffOn_multiPartial_openSlice {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {O : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hO : IsOpen O) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) O) (γ : Fin 3 → ℕ) (t : ℝ) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => multiPartial g γ (y, t)) {y : CKN.Foundation.Parabolic.Vec3 | (y, t) ∈ O}

The time slice of CIV.multiPartial g γ is smooth on the spatial slice of O.