Swap xx heat Kernel

lemma swap_xx_heatKernel  {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α)  (hg : Integrable g) :    HasDerivAt      (fun x' => ∫ y, HKx α (x' - y) t * g y ∂volume)      (∫ y, HKxx α (x - y) t * g y ∂volume) x := by    have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by norm_num)     have meas_HKx_mul : ∀ᶠ x' in 𝓝 x,      AEStronglyMeasurable (fun y : ℝ => HKx α (x' - y) t * g y) volume := by        filter_upwards [mem_nhds] with τ hτ        exact aestronglyMeasurable_HKx_mul g hg hα ht     have integ_HKx_mul :      Integrable (fun y : ℝ => HKx α (x - y) t * g y) :=      integ_HKx_mul_of_L1 g hα ht hg     have integ_HKxx_mul :      Integrable (fun y : ℝ => HKxx α (x - y) t * g y) := by      simpa using integ_HKxx_mul_of_L1 g hα ht hg     have meas_HKxx_mul:      AEStronglyMeasurable (fun y : ℝ => HKxx α (x - y) t * g y) volume      := aestronglyMeasurable_HKxx_mul g hg ht hα     have diff_HKx_mul' : ∀ᵐ y ∂volume, ∀ x' ∈ Metric.ball x 1,        HasDerivAt (fun x'' => HKx α (x'' - y) t * g y) (HKxx α (x' - y) t * g y) x' := by      filter_upwards [diff_HKxx_mul (α := α) (t := t) (x := x) g ht hα] with y hy      intro x' hx'      have h := hy x' hx'      exact h     have dominate_fun :        ∀ᵐ y ∂volume, ∀ x' ∈ Metric.ball x 1,          |HKxx α (x' - y) t * g y| ≤ Kxx α t * |g y| := by      filter_upwards with y      intro x' hx'      calc        |HKxx α (x' - y) t * g y| ≤ |HKxx α (x' - y) t| * |g y| := by rw [abs_mul]        _ ≤ Kxx α t * |g y| := by          gcongr          exact pointwise_bound_HKxx ht hα     have Integ_dominate_fun :        Integrable (fun y : ℝ => Kxx α t * |g y|) :=      (hg.abs.const_mul (Kxx α t))     have result :=      hasDerivAt_integral_of_dominated_loc_of_deriv_le        mem_nhds        meas_HKx_mul        integ_HKx_mul        meas_HKxx_mul        dominate_fun        Integ_dominate_fun        diff_HKx_mul'     exact result.2