Heat from convolution heat Kernel

theorem heat_from_convolution_heatKernel  {α : ℝ} (g : ℝ → ℝ) (hα : 0 < α) (ht : 0 < t) (hg : Integrable g) :  ∀ x,    deriv (fun τ => heatConvolutionHK α g x τ) t      = α * deriv (fun x' => deriv (fun x'' => heatConvolutionHK α g x'' t) x') x := by  intro x  classical   have swap_t : HasDerivAt (fun τ => ∫ y, heatKernel α (x - y) τ * g y) (∫ y, HKt α (x - y) t * g y) t :=    swap_t_heatKernel g ht hα hg   have swap_x : HasDerivAt (fun x' => ∫ y, heatKernel α (x' - y) t * g y) (∫ y, HKx α (x - y) t * g y) x :=    swap_x_heatKernel g ht hα hg   have swap_xx : HasDerivAt (fun x' => ∫ y, HKx α (x' - y) t * g y) (∫ y, HKxx α (x - y) t * g y) x :=    swap_xx_heatKernel g ht hα hg   -- u_t(x,t)  have hut :      deriv (fun τ => heatConvolutionHK α g x τ) t        = ∫ y, HKt α (x - y) t * g y := by    simpa [heatConvolutionHK, HKt] using swap_t.deriv   have swap_x_forall : ∀ x', HasDerivAt (fun x'' => ∫ y, heatKernel α (x'' - y) t * g y)                            (∫ y, HKx α (x' - y) t * g y) x' := by    intro x'    exact swap_x_heatKernel g ht hα hg (x := x')   have hDx :      (fun x' => deriv (fun z => heatConvolutionHK α g z t) x')        = (fun x' => ∫ y, HKx α (x' - y) t * g y) := by    funext x'    simpa [heatConvolutionHK, HKx] using (swap_x_forall x').deriv   -- differentiate that function at x  have hDx_at :      deriv (fun x' => deriv (fun z => heatConvolutionHK α g z t) x') x        = deriv (fun x' => ∫ y, HKx α (x' - y) t * g y) x := by    simpa using congrArg (fun f : ℝ → ℝ => deriv f x) hDx   -- compute that derivative via the second swap  have hx :      deriv (fun x' => ∫ y, HKx α (x' - y) t * g y) x        = ∫ y, HKxx α (x - y) t * g y := by    simpa [HKx, HKxx] using swap_xx.deriv   -- name u_xx(x,t)  have huxx :      deriv (fun x' => deriv (fun z => heatConvolutionHK α g z t) x') x        = ∫ y, HKxx α (x - y) t * g y := hDx_at.trans hx   -- Use the established PDE for the heat kernel  have HK_solves : ∀ y, HKt α (x - y) t = α * HKxx α (x - y) t := fun y =>    heatKernel_solves_heat_eq (hα := hα) (ht := ht) (x := x - y)   -- finish: substitute the kernel PDE inside the integrand and pull α out  calc    deriv (fun τ => heatConvolutionHK α g x τ) t        = ∫ y, HKt α (x - y) t * g y := hut    _   = ∫ y, α * (HKxx α (x - y) t * g y) := by            have hpt : (fun y : ℝ => HKt α (x - y) t * g y)                     = (fun y : ℝ => α * (HKxx α (x - y) t * g y)) := by              funext y              simpa [mul_left_comm, mul_assoc] using                congrArg (fun r => r * g y) (HK_solves y)            simpa using congrArg (fun f : ℝ → ℝ => ∫ y, f y) hpt    _   = α * ∫ y, HKxx α (x - y) t * g y := by            simpa [mul_comm, mul_left_comm, mul_assoc] using              (MeasureTheory.integral_const_mul α (fun y : ℝ => HKxx α (x - y) t * g y))    _   = α * deriv (fun x' => deriv (fun z => heatConvolutionHK α g z t) x') x := by            simp [huxx]