Backward Potential Smooth

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

theorem CKN.Foundation.Heat.backwardTestPotential_future_integral {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x : Parabolic.Vec3) (t : ℝ) : backwardTestPotential ζ (x, t) = ∫ (s : ℝ) in Set.Ioi 0, heatConv s (fun (y : Parabolic.Vec3) => ζ (y, t + s)) x

theorem CKN.Foundation.Heat.backwardTestPotential_future_integrable {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x : Parabolic.Vec3) (t : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => heatConv s (fun (y : Parabolic.Vec3) => ζ (y, t + s)) x) (Set.Ioi 0) MeasureTheory.volume

theorem CKN.Foundation.Heat.backwardTestPotential_future_truncated_tendsto {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (x : Parabolic.Vec3) (t : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (s : ℝ) in Set.Ioi ε, heatConv s (fun (y : Parabolic.Vec3) => ζ (y, t + s)) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (backwardTestPotential ζ (x, t)))