Integrals of the cut-off heat kernels

Before the time s, the spatial derivative of the cut-off backward heat weight Ψ = Γ(x - ·, s - ·) χ has integral of size ρ; this is the gain in the pointwise heat bound of the interior estimates in the proof of lem:aniso:annulus.

theorem CIV.measurePreserving_sub_left_prod (a : CKN.Foundation.Parabolic.Vec3 × ℝ) : MeasureTheory.MeasurePreserving (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => a - z) MeasureTheory.volume MeasureTheory.volume

The reflection-translation z ↦ a - z preserves Lebesgue measure on Vec3 × ℝ.

theorem CIV.integral_comp_sub_left_prod (g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (a : CKN.Foundation.Parabolic.Vec3 × ℝ) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g (a - z) = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g z

Reflection-translation invariance of Lebesgue measure on Vec3 × ℝ.

theorem CIV.differentiableAt_heatKernel_space {t : ℝ} (ht : 0 < t) (y : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (fun (w : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel w t) y

The heat kernel is differentiable in space at positive times.

theorem CIV.abs_serrinCutoff_le_one (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : |serrinCutoff x s ρ z| ≤ 1

The backward cutoff is bounded by one.

theorem CIV.abs_spatialPartial_serrinCutoff_le : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ), 0 < ρ → ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3), |CKN.spatialPartial (serrinCutoff x s ρ) j z| ≤ C / ρ

Scaling bound for the spatial partials of the backward cutoff.

theorem CIV.spatialPartial_serrinHeatWeight_eq (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z.2 < s) (j : Fin 3) : CKN.spatialPartial (serrinHeatWeight x s ρ) j z = -CKN.Foundation.Heat.heatKernelSpaceDerivative (x - z.1) (s - z.2) j * serrinCutoff x s ρ z + CKN.Foundation.Heat.heatKernel (x - z.1) (s - z.2) * CKN.spatialPartial (serrinCutoff x s ρ) j z

Before the time s, the spatial partial of the cut-off heat weight splits into the derivative of the heat kernel and the derivative of the cutoff.

theorem CIV.continuousOn_spatialPartial_serrinHeatWeight (x : CKN.Foundation.Parabolic.Vec3) {s ρ : ℝ} (hρ : 0 < ρ) (j : Fin 3) : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial (serrinHeatWeight x s ρ) j z) (CKN.spaceTimeSet Set.univ (Set.Iio s))

The spatial partial of the cut-off heat weight is continuous before the time s.

noncomputable def CIV.serrinHeatMajorant (ρ C₁ : ℝ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The majorant of the heat-weight derivative, in the variable (x - z.1, s - z.2).

Equations

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

theorem CIV.heatKernelGradientNorm_nonneg_all (y : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : 0 ≤ CKN.Foundation.Heat.heatKernelGradientNorm y t

The gradient norm of the heat kernel is nonnegative.

theorem CIV.serrinHeatMajorant_nonneg {ρ C₁ : ℝ} (hρ : 0 < ρ) (hC₁ : 0 ≤ C₁) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ serrinHeatMajorant ρ C₁ p

The majorant is nonnegative.

theorem CIV.rhoTwo_continuous : Continuous fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.rhoTwo p.1 p.2

The parabolic size |y| + √t is continuous.

theorem CIV.integrable_and_integral_serrinHeatMajorant {ρ C₁ : ℝ} (hρ : 0 < ρ) (hC₁ : 0 ≤ C₁) : MeasureTheory.Integrable (serrinHeatMajorant ρ C₁) MeasureTheory.volume ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), serrinHeatMajorant ρ C₁ p ≤ (300000 + 9000 * C₁) * ρ

The majorant is integrable, with integral of size ρ.

theorem CIV.serrinHeatWeight_spatialPartial_integral : ∃ (C : ℝ), 0 < C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (s ρ : ℝ), 0 < ρ → ρ ≤ 1 → ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinHeatWeight x s ρ) j z) {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s} MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in {z : CKN.Foundation.Parabolic.ParabolicPoint | z.2 < s}, |CKN.spatialPartial (serrinHeatWeight x s ρ) j z| ≤ C * ρ

The spatial derivative of the cut-off heat weight is integrable before the time s, with integral of size ρ.