Kadiri.kadiriTestFn_laplaceTransform

@[blueprint  "kadiri-test-fn-laplace"  (title := "Laplace transform of the Kadiri test function (shift identity)")  (statement := /-- For $f$ satisfying $(H_1)$ of \ref{kadiri-prop-2-1} and  $s, z \in \mathbb{C}$ with $\Re(s + z) > 0$,  $$ \int_0^{\infty} \varphi(y;\, s)\, e^{-z y}\, dy     = \frac{f(0)}{s + z} - F(s + z), $$  where $F$ is the Laplace transform of $f$. -/)  (proof := /-- Direct expansion of the integrand on $y > 0$:  $\varphi(y;\, s) e^{-zy} = (f(0) - f(y)) e^{-(s+z) y}$. Split the integral:  $\int_0^{\infty} f(0)\, e^{-(s+z) y}\, dy = f(0)/(s + z)$ converges by  $\Re(s + z) > 0$; $\int_0^{\infty} f(y)\, e^{-(s+z) y}\, dy = F(s + z)$ unconditionally  since $\mathrm{supp}\, f \subseteq [0, d]$ makes the integral compactly-supported. To be  formalised. -/)  (latexEnv := "lemma")  (discussion := 1486)]theorem kadiriTestFn_laplaceTransform {d : ℝ} (_hd : 0 < d) {f : ℝ → ℝ}    (hf_C2 : ContDiffOn ℝ 2 f (.Icc 0 d))    (hf_supp : tsupport f ⊆ .Ico 0 d)    (s z : ℂ) (hsz : 0 < (s + z).re) :    (∫ y, kadiriTestFn f s y * exp (-z * (y : ℂ)) ∂volume) =      (f 0 : ℂ) / (s + z) - laplaceTransform f (s + z) := by  -- Bridge from two-sided to one-sided: `kadiriTestFn f s` vanishes on $(-\infty, 0]$  -- (it is $0$ for $y < 0$ by the `if 0 ≤ y` branch, and equals $f(0) - f(0) = 0$ at  -- $y = 0$). Hence the integrand equals its $\mathrm{Ioi}\, 0$-indicator, and the  -- two integrals agree.  have heq_indicator :      (fun y => kadiriTestFn f s y * exp (-z * (y : ℂ))) =      (Set.Ioi (0 : ℝ)).indicator (fun y => kadiriTestFn f s y * exp (-z * (y : ℂ))) := by    ext y    by_cases hy : y ∈ Set.Ioi (0 : ℝ)    · rw [Set.indicator_of_mem hy]    · rw [Set.indicator_of_notMem hy]      rw [Set.mem_Ioi, not_lt] at hy      rcases lt_or_eq_of_le hy with hy' | hy'      · simp [kadiriTestFn, not_le.mpr hy']      · simp [kadiriTestFn, ← hy']  have hbridge : (∫ y, kadiriTestFn f s y * exp (-z * (y : ℂ)) ∂volume) =      ∫ y in Set.Ioi (0 : ℝ), kadiriTestFn f s y * exp (-z * (y : ℂ)) ∂volume := by    conv_lhs => rw [heq_indicator]    exact MeasureTheory.integral_indicator measurableSet_Ioi  rw [hbridge]  set w := s + z with hw  have hw0 : w ≠ 0 := fun h => by simp [h] at hsz  have hsplit : Set.EqOn (fun y : ℝ => kadiriTestFn f s y * exp (-z * (y : ℂ)))      (fun y : ℝ => (f 0 : ℂ) * exp (-w * (y : ℂ)) - exp (-w * (y : ℂ)) * (f y : ℂ))      (Set.Ioi 0) := by    intro y hy    have hy0 : (0 : ℝ) ≤ y := (Set.mem_Ioi.1 hy).le    have hmerge : exp (-s * (y : ℂ)) * exp (-z * (y : ℂ)) = exp (-w * (y : ℂ)) := by      rw [← Complex.exp_add]      congr 1      rw [hw]      ring    simp only [kadiriTestFn, if_pos hy0]    calc ((f 0 : ℂ) - (f y : ℂ)) * exp (-s * (y : ℂ)) * exp (-z * (y : ℂ))        = ((f 0 : ℂ) - (f y : ℂ)) * (exp (-s * (y : ℂ)) * exp (-z * (y : ℂ))) := by ring      _ = ((f 0 : ℂ) - (f y : ℂ)) * exp (-w * (y : ℂ)) := by rw [hmerge]      _ = (f 0 : ℂ) * exp (-w * (y : ℂ)) - exp (-w * (y : ℂ)) * (f y : ℂ) := by ring  rw [setIntegral_congr_fun measurableSet_Ioi hsplit]  have hiexp : IntegrableOn (fun y : ℝ => exp (-w * (y : ℂ))) (Set.Ioi 0) := by    refine (integrable_norm_iff (Measurable.aestronglyMeasurable <| by fun_prop)).mp ?_    suffices h : IntegrableOn (fun y : ℝ => Real.exp (-w.re * y)) (Set.Ioi 0) by      simpa [Complex.norm_exp, neg_mul] using! h    exact exp_neg_integrableOn_Ioi 0 hsz  have hiA : IntegrableOn (fun y : ℝ => (f 0 : ℂ) * exp (-w * (y : ℂ))) (Set.Ioi 0) :=    hiexp.const_mul _  have hiB : IntegrableOn (fun y : ℝ => exp (-w * (y : ℂ)) * (f y : ℂ)) (Set.Ioi 0) := by    have hsupp : Function.support (fun y : ℝ => exp (-w * (y : ℂ)) * (f y : ℂ)) ⊆        Set.Icc 0 d := by      intro y hy      have hfy : f y ≠ 0 := by        intro h0        apply hy        simp [h0]      exact Set.Ico_subset_Icc_self (hf_supp (subset_tsupport f hfy))    have hcont : ContinuousOn (fun y : ℝ => exp (-w * (y : ℂ)) * (f y : ℂ)) (Set.Icc 0 d) := by      apply ContinuousOn.mul      · exact Continuous.continuousOn (by fun_prop)      · exact Complex.continuous_ofReal.comp_continuousOn hf_C2.continuousOn    have hIcc : IntegrableOn (fun y : ℝ => exp (-w * (y : ℂ)) * (f y : ℂ)) (Set.Icc 0 d) :=      hcont.integrableOn_compact isCompact_Icc    exact ((integrableOn_iff_integrable_of_support_subset hsupp).mp hIcc).integrableOn  rw [integral_sub hiA hiB]  have hB : (∫ y in Set.Ioi (0 : ℝ), exp (-w * (y : ℂ)) * (f y : ℂ)) =      laplaceTransform f w := rfl  have hA : (∫ y in Set.Ioi (0 : ℝ), (f 0 : ℂ) * exp (-w * (y : ℂ))) = (f 0 : ℂ) / w := by    rw [integral_const_mul]    have hderiv : ∀ x ∈ Set.Ici (0 : ℝ),        HasDerivAt (fun y : ℝ => -exp (-w * (y : ℂ)) / w) (exp (-w * (x : ℂ))) x :=      fun x _ => laplaceKernel_antideriv_hasDerivAt hw0 x    have htend : Filter.Tendsto (fun y : ℝ => -exp (-w * (y : ℂ)) / w)        Filter.atTop (nhds 0) := by      rw [tendsto_zero_iff_norm_tendsto_zero]      have heq : (fun y : ℝ => ‖-exp (-w * (y : ℂ)) / w‖) =          fun y : ℝ => Real.exp (-w.re * y) / ‖w‖ := by        funext y        rw [norm_div, norm_neg, Complex.norm_exp]        congr 2        simp [Complex.mul_re]      rw [heq]      have hnum : Filter.Tendsto (fun y : ℝ => Real.exp (-w.re * y))          Filter.atTop (nhds 0) :=        Real.tendsto_exp_atBot.comp          ((Filter.tendsto_const_mul_atBot_of_neg (neg_lt_zero.2 hsz)).2 Filter.tendsto_id)      simpa using hnum.div_const ‖w‖    have hint : (∫ y in Set.Ioi (0 : ℝ), exp (-w * (y : ℂ))) = 1 / w := by      calc (∫ y in Set.Ioi (0 : ℝ), exp (-w * (y : ℂ)))          = 0 - (-exp (-w * ((0 : ℝ) : ℂ)) / w) :=            MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto' hderiv hiexp htend        _ = 1 / w := by            norm_num [Complex.ofReal_zero, mul_zero, Complex.exp_zero, zero_sub, neg_div,              neg_neg]    rw [hint, mul_one_div]  rw [hA, hB]