The annular kernel integration-by-parts bound

A kernel estimate for the interior estimates of lem:aniso:annulus: for F smooth with compact support (here specialised to a spatial multi-index derivative of the ball cutoff), moving the γ₂ spatial derivatives off an arbitrary g bounded only by |g| ≤ M, using the cutoff-times-kernel product's compact support in the annulus ρ/2 ≤ |y - x| ≤ ρ to justify the integration by parts, and the Euclidean-norm kernel and ρ-scaled cutoff bounds (AnnularKernelIBP.lean) to close each resulting term.

Part A: the kernel factor's shift chain rule

Part B: smoothness and compact support of a kernel-times-cutoff term

noncomputable def CIV.kernelCutoffTerm (l : Fin 3) (β : Fin 3 → ℕ) (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ) (γ : Fin 3 → ℕ) (t : ℝ) (y : CKN.Foundation.Parabolic.Vec3) : ℝ

A derivative of the Newtonian kernel at x - y times a derivative of the ball cutoff at (y, t): the integrand of abs_integral_kernelCutoffTerm_mul_le.

Equations

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

Part C: the volume of the annulus, and the base term bound

theorem CIV.abs_integral_kernelCutoffTerm_mul_le (l : Fin 3) {β : Fin 3 → ℕ} (hβ : β 0 + β 1 + β 2 ≤ 2) (x : CKN.Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ0 : 0 < ρ) {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (t M : ℝ) (hM : 0 ≤ M) (h : CKN.Foundation.Parabolic.Vec3 → ℝ) (hh : ∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → |h y| ≤ M) : ∃ (C : ℝ), 0 ≤ C ∧ |∫ (y : CKN.Foundation.Parabolic.Vec3), kernelCutoffTerm l β x ρ γ t y * h y| ≤ C * M * ρ / ρ ^ (β 0 + β 1 + β 2 + (γ 0 + γ 1 + γ 2))

The generic bound on the integral of a kernel-times-cutoff term against a function bounded on the ball.

Part D: pushing one more derivative onto the kernel factor

Part E: the Leibniz expansion of one more derivative of a kernel-cutoff term

Part F: the integration-by-parts step

Part G: integrability of a kernel-cutoff term times a slice-continuous function

Part H2: the open-set version, for functions singular off an open set

Part I: order-uniform bounds for the kernel and the cutoff

Part J: the uniform-constant integral bound, and the final assembly

Part K: multi-index bookkeeping and the reusable Leibniz-split step

Part L: the final assembly

theorem CIV.ELc_annular_kernel_ibp : ∃ (C : ℝ), 0 < C ∧ ∀ (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (O : Set CKN.Foundation.Parabolic.ParabolicPoint) (x : CKN.Foundation.Parabolic.Vec3) (t ρ M : ℝ) (γ₁ γ₂ : Fin 3 → ℕ) (l : Fin 3), IsOpen O → 0 < ρ → ρ ≤ 1 → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → (y, t) ∈ O) → ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) O → (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ → |g (y, t)| ≤ M) → γ₁ ≠ 0 → γ₁ 0 + γ₁ 1 + γ₁ 2 + (γ₂ 0 + γ₂ 1 + γ₂ 2) ≤ 3 → |∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel l (x - y) * multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1) γ₁ (y, t) * multiPartial g γ₂ (y, t)| ≤ C * M * ρ / ρ ^ (γ₁ 0 + γ₁ 1 + γ₁ 2 + (γ₂ 0 + γ₂ 1 + γ₂ 2))