Kadiri.laplaceTransform_ibp

theorem laplaceTransform_ibp {d : ℝ} (hd : 0 < d) {f : ℝ → ℝ}    (hf_C2 : ContDiffOn ℝ 2 f (Set.Icc 0 d))    (hf_supp : tsupport f ⊆ Set.Ico 0 d)    (hf_d : f d = 0)    (hf_derivWithin_0 : derivWithin f (Set.Icc 0 d) 0 = 0)    (hf_derivWithin_d : derivWithin f (Set.Icc 0 d) d = 0)    {w : ℂ} (hw : w ≠ 0) :    laplaceTransform f w =      (f 0 : ℂ) / w + laplaceTransform (fun u => deriv (deriv f) u) w / w ^ 2 := by  let I : Set ℝ := Set.Icc 0 d  let K : ℝ → ℂ := fun t => exp (-w * (t : ℂ))  let A : ℝ → ℂ := fun t => -K t / w  let df : ℝ → ℝ := fun t => derivWithin f I t  let d2f : ℝ → ℝ := fun t => derivWithin df I t  have hdf_C1 : ContDiffOn ℝ 1 df I := by    simpa [df, I] using hf_C2.derivWithin (uniqueDiffOn_Icc hd) (by norm_num)  have hK_int : IntervalIntegrable K volume 0 d := by    apply Continuous.intervalIntegrable    fun_prop  have hdf_int : IntervalIntegrable (fun t => (df t : ℂ)) volume 0 d := by    have hdf_cont : ContinuousOn (fun t => (df t : ℂ)) (Set.uIcc (0 : ℝ) d) := by      have hreal : ContinuousOn df I :=        hdf_C1.continuousOn      simpa [I, Set.uIcc_of_le hd.le] using! continuous_ofReal.comp_continuousOn hreal    exact hdf_cont.intervalIntegrable  have hd2f_int : IntervalIntegrable (fun t => (d2f t : ℂ)) volume 0 d := by    have hd2f_cont : ContinuousOn (fun t => (d2f t : ℂ)) (Set.uIcc (0 : ℝ) d) := by      have hreal : ContinuousOn d2f I := by        simpa [d2f] using hdf_C1.continuousOn_derivWithin (uniqueDiffOn_Icc hd) (by norm_num)      simpa [I, Set.uIcc_of_le hd.le] using! continuous_ofReal.comp_continuousOn hreal    exact hd2f_cont.intervalIntegrable  have hA_deriv : ∀ x ∈ Set.uIcc (0 : ℝ) d, HasDerivWithinAt A (K x) (Set.uIcc (0 : ℝ) d) x := by    intro x _hx    simpa [A, K] using (laplaceKernel_antideriv_hasDerivAt (w := w) hw x).hasDerivWithinAt  have hf_deriv :      ∀ x ∈ Set.uIcc (0 : ℝ) d,        HasDerivWithinAt (fun y : ℝ => (f y : ℂ)) ((df x : ℝ) : ℂ) (Set.uIcc (0 : ℝ) d) x := by    intro x hx    have hxI : x ∈ I := by      simpa [I, Set.uIcc_of_le hd.le] using hx    have hreal : HasDerivWithinAt f (df x) I x := by      simpa [df] using (hf_C2.differentiableOn (by norm_num) x hxI).hasDerivWithinAt    simpa [I, Set.uIcc_of_le hd.le] using hreal.ofReal_comp  have hdf_deriv :      ∀ x ∈ Set.uIcc (0 : ℝ) d,        HasDerivWithinAt (fun y : ℝ => ((df y : ℝ) : ℂ)) ((d2f x : ℝ) : ℂ)          (Set.uIcc (0 : ℝ) d) x := by    intro x hx    have hxI : x ∈ I := by      simpa [I, Set.uIcc_of_le hd.le] using hx    have hreal : HasDerivWithinAt df (d2f x) I x := by      simpa [d2f] using (hdf_C1.differentiableOn (by norm_num) x hxI).hasDerivWithinAt    simpa [I, Set.uIcc_of_le hd.le] using hreal.ofReal_comp  have hA_df :      ∫ t in (0 : ℝ)..d, A t * (df t : ℂ) =        -(∫ t in (0 : ℝ)..d, K t * (df t : ℂ)) / w := by    calc      ∫ t in (0 : ℝ)..d, A t * (df t : ℂ)          = ∫ t in (0 : ℝ)..d, -(K t * (df t : ℂ)) / w := by            apply intervalIntegral.integral_congr            intro t _ht            simp [A]            ring      _ = -(∫ t in (0 : ℝ)..d, K t * (df t : ℂ)) / w := by            rw [intervalIntegral.integral_div, intervalIntegral.integral_neg]  have hA_d2f :      ∫ t in (0 : ℝ)..d, A t * (d2f t : ℂ) =        -(∫ t in (0 : ℝ)..d, K t * (d2f t : ℂ)) / w := by    calc      ∫ t in (0 : ℝ)..d, A t * (d2f t : ℂ)          = ∫ t in (0 : ℝ)..d, -(K t * (d2f t : ℂ)) / w := by            apply intervalIntegral.integral_congr            intro t _ht            simp [A]            ring      _ = -(∫ t in (0 : ℝ)..d, K t * (d2f t : ℂ)) / w := by            rw [intervalIntegral.integral_div, intervalIntegral.integral_neg]  have hibp1 := intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt    (a := (0 : ℝ)) (b := d) (u := A) (v := fun t : ℝ => (f t : ℂ))    (u' := K) (v' := fun t : ℝ => (df t : ℂ)) hA_deriv hf_deriv hK_int hdf_int  have hfirst :      ∫ t in (0 : ℝ)..d, K t * (f t : ℂ) =        (f 0 : ℂ) / w + (∫ t in (0 : ℝ)..d, K t * (df t : ℂ)) / w := by    have hsolve :        ∫ t in (0 : ℝ)..d, K t * (f t : ℂ) =          A d * (f d : ℂ) - A 0 * (f 0 : ℂ) -            ∫ t in (0 : ℝ)..d, A t * (df t : ℂ) := by      rw [hibp1]      abel    rw [hsolve, hA_df, hf_d]    simp [A, K]    field_simp [hw]    ring  have hibp2 := intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt    (a := (0 : ℝ)) (b := d) (u := A) (v := fun t : ℝ => ((df t : ℝ) : ℂ))    (u' := K) (v' := fun t : ℝ => (d2f t : ℂ)) hA_deriv hdf_deriv hK_int hd2f_int  have hsecond :      ∫ t in (0 : ℝ)..d, K t * (df t : ℂ) =        (∫ t in (0 : ℝ)..d, K t * (d2f t : ℂ)) / w := by    have hsolve :        ∫ t in (0 : ℝ)..d, K t * (df t : ℂ) =          A d * (df d : ℂ) - A 0 * (df 0 : ℂ) -            ∫ t in (0 : ℝ)..d, A t * (d2f t : ℂ) := by      rw [hibp2]      abel    have hdf0 : df 0 = 0 := by simpa [df, I] using hf_derivWithin_0    have hdfd : df d = 0 := by simpa [df, I] using hf_derivWithin_d    rw [hsolve, hA_d2f, hdf0, hdfd]    simp [A, K]    field_simp [hw]  have hd2f_interval_eq :      ∫ t in (0 : ℝ)..d, K t * (d2f t : ℂ) =        ∫ t in (0 : ℝ)..d, K t * ((deriv (deriv f) t : ℝ) : ℂ) := by    rw [intervalIntegral.integral_of_le hd.le, intervalIntegral.integral_of_le hd.le]    apply integral_congr_ae    rw [← restrict_Ioo_eq_restrict_Ioc]    filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx    have hdf_eq : df =ᶠ[nhds x] deriv f := by      filter_upwards [Ioo_mem_nhds hx.1 hx.2] with y hy      exact derivWithin_of_mem_nhds (s := I) (Icc_mem_nhds hy.1 hy.2)    have hd2_eq : d2f x = deriv (deriv f) x := by      calc        d2f x = derivWithin df I x := rfl        _ = deriv df x := derivWithin_of_mem_nhds (s := I) (Icc_mem_nhds hx.1 hx.2)        _ = deriv (deriv f) x := Filter.EventuallyEq.deriv_eq hdf_eq    simp [hd2_eq]  rw [laplaceTransform_eq_interval_of_tsupport_subset_Ico hd hf_supp w,    laplaceTransform_deriv_deriv_eq_interval_of_tsupport_subset_Ico hd hf_supp w]  calc    ∫ t in (0 : ℝ)..d, K t * (f t : ℂ)        = (f 0 : ℂ) / w + (∫ t in (0 : ℝ)..d, K t * (df t : ℂ)) / w := hfirst    _ = (f 0 : ℂ) / w + ((∫ t in (0 : ℝ)..d, K t * (d2f t : ℂ)) / w) / w := by      rw [hsecond]    _ = (f 0 : ℂ) / w +          (∫ t in (0 : ℝ)..d, K t * ((deriv (deriv f) t : ℝ) : ℂ)) / w ^ 2 := by      rw [hd2f_interval_eq]      field_simp [hw]