Swap t heat Kernel

lemma swap_t_heatKernel  {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α)  (hg : Integrable g) :    HasDerivAt      (fun τ => ∫ y, heatKernel α (x - y) τ * g y ∂volume)      (∫ y, HKt α (x - y) t * g y ∂volume) t := by    have t_pos: t/2 > 0 := by positivity    have τ_pos: ∀ τ ∈ Metric.ball t (t/2), τ > 0 := by      intro τ hτ      rw [Metric.mem_ball, Real.dist_eq] at hτ      have := abs_sub_lt_iff.mp hτ      linarith    have mem_nhds : Metric.ball t (t/2) ∈ 𝓝 t := Metric.ball_mem_nhds t (by linarith)     have meas_HK_mul : ∀ᶠ τ in 𝓝 t,       AEStronglyMeasurable (fun y : ℝ => heatKernel α (x - y) τ * g y) volume       := by       filter_upwards [mem_nhds] with τ hτ       exact aestronglyMeasurable_heatKernel_mul hα (τ_pos τ hτ) g hg     have integ_HK_mul: Integrable (fun y : ℝ => heatKernel α (x - y) t * g y)      := integrable_heatKernel_mul_of_L1 g hα ht hg     have integ_HKt_mul: Integrable (fun y : ℝ => HKt α (x - y) t * g y)      := integ_HKt_mul_of_L1 g hα ht hg     have meas_HKt_mul:      AEStronglyMeasurable (fun y : ℝ => HKt α (x - y) t * g y) volume      := aestronglyMeasurable_HKt_mul g hg hα ht     have diff_HK_mul' : ∀ᵐ y ∂volume, ∀ τ ∈ Metric.ball t (t/2),      HasDerivAt (fun τ' => heatKernel α (x - y) τ' * g y) (HKt α (x - y) τ * g y) τ        := by        filter_upwards [@diff_HKt_mul α x t g ht hα] with y hy        intro τ hτ        have h := hy τ hτ        exact h     have dominate_fun: ∀ᵐ y ∂volume, ∀ τ ∈ Metric.ball t (t/2),      |HKt α (x - y) τ * g y| ≤ (3/t) * (c α (t/2)) * |g y|        := by        filter_upwards with y        intro τ hτ        unfold c        have τ_lower : τ > t/2 := by            rw [Metric.mem_ball, Real.dist_eq] at hτ            have := abs_sub_lt_iff.mp hτ            linarith        calc          |HKt α (x - y) τ * g y| ≤ |HKt α (x - y) τ| * |g y| := by rw [abs_mul]          _ ≤ (3/(2*τ)) * (c α τ) * |g y| := by            gcongr            exact pointwise_bound_HKt (by linarith) hα          _ ≤ (3/t) * (c α (t/2)) * |g y| := by            gcongr            · exact (c_pos hα (by linarith)).le            · linarith [τ_lower]            · exact mono_Coeff (by linarith) (by linarith) hα (by linarith)     have Integ_dominate_fun: Integrable (fun y : ℝ => (3/t) * (c α (t/2)) * |g y|)      := by      simpa using (hg.abs).const_mul ((3 / t) * (c α (t/2)))     have result := hasDerivAt_integral_of_dominated_loc_of_deriv_le      mem_nhds meas_HK_mul integ_HK_mul meas_HKt_mul dominate_fun Integ_dominate_fun diff_HK_mul'     exact result.2