Integrability

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.Foundation.Heat.heatKernelGradientMajorant (x : Parabolic.Vec3) (t : ℝ) : ℝ

Wider Gaussian majorant for the spatial heat-kernel gradient.

Equations

• CKN.Foundation.Heat.heatKernelGradientMajorant x t = if 0 < t then (√t)⁻¹ * (4 * Real.pi * t) ^ (-3 / 2) * Real.exp ((-∑ i : Fin 3, x i ^ 2) / (8 * t)) else 0

theorem CKN.Foundation.Heat.heatKernelGradientNorm_le_majorant {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernelGradientNorm x t ≤ 100 * heatKernelGradientMajorant x t

theorem CKN.Foundation.Heat.heatKernelGradientMajorant_nonneg (x : Parabolic.Vec3) (t : ℝ) : 0 ≤ heatKernelGradientMajorant x t

theorem CKN.Foundation.Heat.heatKernelGradientMajorant_slice_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : Parabolic.Vec3) => heatKernelGradientMajorant x t) MeasureTheory.volume

theorem CKN.Foundation.Heat.heatKernelGradientMajorant_slice_le {t : ℝ} (ht : 0 < t) : ∫ (x : Parabolic.Vec3), ‖heatKernelGradientMajorant x t‖ ≤ 4 * (√t)⁻¹

theorem CKN.Foundation.Heat.heatKernelGradientNorm_measurable : Measurable fun (p : Parabolic.ParabolicPoint) => heatKernelGradientNorm p.1 p.2

theorem CKN.Foundation.Heat.heatKernelPlus_integrable_prod {T : ℝ} : MeasureTheory.Integrable (fun (p : Parabolic.Vec3 × ℝ) => heatKernelPlus (have this := p; this)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))

theorem CKN.Foundation.Heat.heatKernelPlus_integrableOn_time {T : ℝ} : MeasureTheory.IntegrableOn (fun (p : Parabolic.ParabolicPoint) => heatKernelPlus p) (Set.univ ×ˢ Set.Ioc 0 T) MeasureTheory.volume

theorem CKN.Foundation.Heat.time_sqrt_inv_integrable {T : ℝ} (hT : 0 < T) : MeasureTheory.Integrable (fun (t : ℝ) => 4 * (√t)⁻¹) (MeasureTheory.volume.restrict (Set.Ioc 0 T))

theorem CKN.Foundation.Heat.heatKernelGradientNorm_eq_zero_of_nonpos {x : Parabolic.Vec3} {t : ℝ} (ht : t ≤ 0) : heatKernelGradientNorm x t = 0

theorem CKN.Foundation.Heat.heatKernelGradientNorm_integrable_prod {T : ℝ} (hT : 0 < T) : MeasureTheory.Integrable (fun (p : Parabolic.Vec3 × ℝ) => heatKernelGradientNorm p.1 p.2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))

theorem CKN.Foundation.Heat.heatKernelGradientNorm_integrableOn_time {T : ℝ} (hT : 0 < T) : MeasureTheory.IntegrableOn (fun (p : Parabolic.ParabolicPoint) => heatKernelGradientNorm p.1 p.2) (Set.univ ×ˢ Set.Ioc 0 T) MeasureTheory.volume

theorem CKN.Foundation.Heat.heatKernelPlus_locallyIntegrable : MeasureTheory.LocallyIntegrable (fun (p : Parabolic.ParabolicPoint) => heatKernelPlus p) MeasureTheory.volume

theorem CKN.Foundation.Heat.heatKernelGradientNorm_locallyIntegrable : MeasureTheory.LocallyIntegrable (fun (p : Parabolic.ParabolicPoint) => heatKernelGradientNorm p.1 p.2) MeasureTheory.volume