Session Laplace_Transform

Theory Laplace_Transform_Library

theory Laplace_Transform_Library
  imports
    "HOL-Analysis.Analysis"
begin

section ‹References›

text ‹
Much of this formalization is based on Schiff's textbook @{cite "Schiff2013"}.
Parts of this formalization are inspired by the HOL-Light formalization
(@{cite "Taqdees2013"}, @{cite "Rashid2017"}, @{cite "Rashid2018"}), but stated more generally for
piecewise continuous (instead of piecewise continuously differentiable) functions.
›

section ‹Library Additions›

subsection ‹Derivatives›

lemma DERIV_compose_FDERIV:―‹TODO: generalize and move from HOL-ODE›
  assumes "DERIV f (g x) :> f'"
  assumes "(g has_derivative g') (at x within s)"
  shows "((λx. f (g x)) has_derivative (λx. g' x * f')) (at x within s)"
  using assms has_derivative_compose[of g g' x s f "(*) f'"]
  by (auto simp: has_field_derivative_def ac_simps)

lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
  and  has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
  and  has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]


subsection ‹Integrals›

lemma negligible_real_ivlI:
  fixes a b::real
  assumes "a  b"
  shows "negligible {a .. b}"
proof -
  from assms have "{a .. b} = {a}  {a .. b} = {}"
    by auto
  then show ?thesis
    by auto
qed

lemma absolutely_integrable_on_combine:
  fixes f :: "real  'a::euclidean_space"
  assumes "f absolutely_integrable_on {a..c}"
    and "f absolutely_integrable_on {c..b}"
    and "a  c"
    and "c  b"
  shows "f absolutely_integrable_on {a..b}"
  using assms
  unfolding absolutely_integrable_on_def integrable_on_def
  by (auto intro!: has_integral_combine)

lemma dominated_convergence_at_top:
  fixes f :: "real  'n::euclidean_space  'm::euclidean_space"
  assumes f: "k. (f k) integrable_on s" and h: "h integrable_on s"
    and le: "k x. x  s  norm (f k x)  h x"
    and conv: "x  s. ((λk. f k x)  g x) at_top"
  shows "g integrable_on s" "((λk. integral s (f k))  integral s g) at_top"
proof -
  have 3: "set_integrable lebesgue s h"
    unfolding absolutely_integrable_on_def
  proof
    show "(λx. norm (h x)) integrable_on s"
    proof (intro integrable_spike_finite[OF _ _ h, where S="{}"] ballI)
      fix x assume "x  s - {}" then show "norm (h x) = h x"
        using order_trans[OF norm_ge_zero le[of x]] by auto
    qed auto
  qed fact
  have 2: "set_borel_measurable lebesgue s (f k)" for k
    using f[of k]
    using has_integral_implies_lebesgue_measurable[of "f k"]
    by (auto intro:  simp: integrable_on_def set_borel_measurable_def)
  have conv': "x  s. ((λk. f k x)  g x) sequentially"
    using conv filterlim_filtermap filterlim_compose filterlim_real_sequentially by blast
  from 2 have 1: "set_borel_measurable lebesgue s g"
    unfolding set_borel_measurable_def
    by (rule borel_measurable_LIMSEQ_metric) (use conv' in auto split: split_indicator›)
  have 4: "AE x in lebesgue. ((λi. indicator s x *R f i x)  indicator s x *R g x) at_top"
    "F i in at_top. AE x in lebesgue. norm (indicator s x *R f i x)  indicator s x *R h x"
    using conv le by (auto intro!: always_eventually split: split_indicator)

  note 1 2 3 4
  note * = this[unfolded set_borel_measurable_def set_integrable_def]
  have g: "g absolutely_integrable_on s"
    unfolding set_integrable_def
    by (rule integrable_dominated_convergence_at_top[OF *])
  then show "g integrable_on s"
    by (auto simp: absolutely_integrable_on_def)
  have "((λk. (LINT x:s|lebesgue. f k x))  (LINT x:s|lebesgue. g x)) at_top"
    unfolding set_lebesgue_integral_def
    using *
    by (rule integral_dominated_convergence_at_top)
  then show "((λk. integral s (f k))  integral s g) at_top"
    using g absolutely_integrable_integrable_bound[OF le f h]
    by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
qed

lemma has_integral_dominated_convergence_at_top:
  fixes f :: "real  'n::euclidean_space  'm::euclidean_space"
  assumes "k. (f k has_integral y k) s" "h integrable_on s"
    "k x. xs  norm (f k x)  h x" "xs. ((λk. f k x)  g x) at_top"
    and x: "(y  x) at_top"
  shows "(g has_integral x) s"
proof -
  have int_f: "k. (f k) integrable_on s"
    using assms by (auto simp: integrable_on_def)
  have "(g has_integral (integral s g)) s"
    by (intro integrable_integral dominated_convergence_at_top[OF int_f assms(2)]) fact+
  moreover have "integral s g = x"
  proof (rule tendsto_unique)
    show "((λi. integral s (f i))  x) at_top"
      using integral_unique[OF assms(1)] x by simp
    show "((λi. integral s (f i))  integral s g) at_top"
      by (intro dominated_convergence_at_top[OF int_f assms(2)]) fact+
  qed simp
  ultimately show ?thesis
    by simp
qed

lemma integral_indicator_eq_restriction:
  fixes f::"'a::euclidean_space  'b::banach"
  assumes f: "f integrable_on R"
    and "R  S"
  shows "integral S (λx. indicator R x *R f x) = integral R f"
proof -
  let ?f = "λx. indicator R x *R f x"
  have "?f integrable_on R"
    using f negligible_empty
    by (rule integrable_spike) auto
  from integrable_integral[OF this]
  have "(?f has_integral integral R ?f) S"
    by (rule has_integral_on_superset) (use R  S in auto simp: indicator_def›)
  also have "integral R ?f = integral R f"
    using negligible_empty
    by (rule integral_spike) auto
  finally show ?thesis
    by blast
qed

lemma
  improper_integral_at_top:
  fixes f::"real  'a::euclidean_space"
  assumes "f absolutely_integrable_on {a..}"
  shows "((λx. integral {a..x} f)  integral {a..} f) at_top"
proof -
  let ?f = "λ(k::real) (t::real). indicator {a..k} t *R f t"
  have f: "f integrable_on {a..k}" for k
    using set_lebesgue_integral_eq_integral(1)[OF assms]
    by (rule integrable_on_subinterval) simp
  from this negligible_empty have "?f k integrable_on {a..k}" for k
    by (rule integrable_spike) auto
  from this have "?f k integrable_on {a..}" for k
    by (rule integrable_on_superset) auto
  moreover
  have "(λx. norm (f x)) integrable_on {a..}"
    using assms by (simp add: absolutely_integrable_on_def)
  moreover
  note _
  moreover
  have "F k in at_top. k  x" for x::real
    by (simp add: eventually_ge_at_top)
  then have "x{a..}. ((λk. ?f k x)  f x) at_top"
    by (auto intro!: Lim_transform_eventually[OF tendsto_const] simp: indicator_def eventually_at_top_linorder)
  ultimately
  have "((λk. integral {a..} (?f k))  integral {a ..} f) at_top"
    by (rule dominated_convergence_at_top) (auto simp: indicator_def)
  also have "(λk. integral {a..} (?f k)) = (λk. integral {a..k} f)"
    by (auto intro!: ext integral_indicator_eq_restriction f)
  finally show ?thesis .
qed

lemma norm_integrable_onI: "(λx. norm (f x)) integrable_on S"
  if "f absolutely_integrable_on S"
  for f::"'a::euclidean_space'b::euclidean_space"
  using that by (auto simp: absolutely_integrable_on_def)

lemma
  has_integral_improper_at_topI:
  fixes f::"real  'a::banach"
  assumes I: "F k in at_top. (f has_integral I k) {a..k}"
  assumes J: "(I  J) at_top"
  shows "(f has_integral J) {a..}"
  apply (subst has_integral')
proof (auto, goal_cases)
  case (1 e)
  from tendstoD[OF J 0 < e]
  have "F x in at_top. dist (I x) J < e" .
  moreover have "F x in at_top. (x::real) > 0" by simp
  moreover have "F x in at_top. (x::real) > - a"―‹TODO: this seems to be strange?›
    by simp
  moreover note I
  ultimately have "F x in at_top. x > 0  x > - a  dist (I x) J < e 
    (f has_integral I x) {a..x}" by eventually_elim auto
  then obtain k where k: "bk. norm (I b - J) < e" "k > 0" "k > - a"
    and I: "c. c  k  (f has_integral I c) {a..c}"
    by (auto simp: eventually_at_top_linorder dist_norm)
  show ?case
    apply (rule exI[where x=k])
    apply (auto simp: 0 < k)
    subgoal premises prems for b c
    proof -
      have ball_eq: "ball 0 k = {-k <..< k}" by (auto simp: abs_real_def split: if_splits)
      from prems 0 < k have "c  0" "b  0"
        by (auto simp: subset_iff)
      with prems 0 < k have "c  k"
        apply (auto simp: ball_eq)
        apply (auto simp: subset_iff)
        apply (drule spec[where x="(c + k)/2"])
        apply (auto simp: algebra_split_simps not_less)
        using 0  c by linarith
      then have "norm (I c - J) < e" using k by auto
      moreover
      from prems 0 < k c  0 b  0 c  k k > - a have "a  b"
        apply (auto simp: ball_eq)
        apply (auto simp: subset_iff)
        by (meson b  0 less_eq_real_def minus_less_iff not_le order_trans)
      have "((λx. if x  cbox a c then f x else 0) has_integral I c) (cbox b c)"
        apply (subst has_integral_restrict_closed_subintervals_eq)
        using I[of c] prems a  b k  c
        by (auto )
      from negligible_empty _ this have "((λx. if a  x then f x else 0) has_integral I c) (cbox b c)"
        by (rule has_integral_spike) auto
      ultimately
      show ?thesis
        by (intro exI[where x="I c"]) auto
    qed
    done
qed

lemma has_integral_improperE:
  fixes f::"real  'a::euclidean_space"
  assumes I: "(f has_integral I) {a..}"
  assumes ai: "f absolutely_integrable_on {a..}"
  obtains J where
    "k. (f has_integral J k) {a..k}"
    "(J  I) at_top"
proof -
  define J where "J k = integral {a .. k} f" for k
  have "(f has_integral J k) {a..k}" for k
    unfolding J_def
    by (force intro: integrable_on_subinterval has_integral_integrable[OF I])
  moreover
  have I_def[symmetric]: "integral {a..} f = I"
    using I by auto
  from improper_integral_at_top[OF ai]
  have "(J  I) at_top"
    unfolding J_def I_def .
  ultimately show ?thesis ..
qed


subsection ‹Miscellaneous›

lemma AE_BallI: "AE xX in F. P x" if "x  X. P x"
  using that by (intro always_eventually) auto

lemma bounded_le_Sup:
  assumes "bounded (f ` S)"
  shows "xS. norm (f x)  Sup (norm ` f ` S)"
  by (auto intro!: cSup_upper bounded_imp_bdd_above simp: bounded_norm_comp assms)

end

Theory Piecewise_Continuous

section ‹Piecewise Continous Functions›
theory Piecewise_Continuous
  imports
    Laplace_Transform_Library
begin

subsection ‹at within filters›

lemma at_within_self_singleton[simp]: "at i within {i} = bot"
  by (auto intro!: antisym filter_leI simp: eventually_at_filter)

lemma at_within_t1_space_avoid:
  "(at x within X - {i}) = (at x within X)" if "x  i" for x i::"'a::t1_space"
proof (safe intro!: antisym filter_leI)
  fix P
  assume "eventually P (at x within X - {i})"
  moreover have "eventually (λx. x  i) (nhds x)"
    by (rule t1_space_nhds) fact
  ultimately
  show "eventually P (at x within X)"
    unfolding eventually_at_filter
    by eventually_elim auto
qed (simp add: eventually_mono order.order_iff_strict eventually_at_filter)

lemma at_within_t1_space_avoid_finite:
  "(at x within X - I) = (at x within X)" if "finite I" "x  I" for x::"'a::t1_space"
  using that
proof (induction I)
  case (insert i I)
  then show ?case
    by auto (metis Diff_insert at_within_t1_space_avoid)
qed simp

lemma at_within_interior:
  "NO_MATCH (UNIV::'a set) (S::'a::topological_space set)  x  interior S  at x within S = at x"
  by (rule at_within_interior)


subsection ‹intervals›

lemma Compl_Icc: "- {a .. b} = {..<a}  {b<..}" for a b::"'a::linorder"
  by auto

lemma interior_Icc[simp]: "interior {a..b} = {a<..<b}"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
    ― ‹TODO: is no_bot› and no_top› really required?›
  by (auto simp add: Compl_Icc interior_closure)

lemma closure_finite[simp]: "closure X = X" if "finite X" for X::"'a::t1_space set"
  using that
  by (induction X) (simp_all add: closure_insert)

definition piecewise_continuous_on :: "'a::linorder_topology  'a  'a set  ('a  'b::topological_space)  bool"
where "piecewise_continuous_on a b I f 
  (continuous_on ({a .. b} - I) f  finite I 
    (iI. (i  {a<..b}  (l. (f  l) (at_left i))) 
      (i  {a..<b}  (u. (f  u) (at_right i)))))"

lemma piecewise_continuous_on_subset:
  "piecewise_continuous_on a b I f  {c .. d}  {a .. b}  piecewise_continuous_on c d I f"
  by (force simp add: piecewise_continuous_on_def intro: continuous_on_subset)

lemma piecewise_continuous_onE:
  assumes "piecewise_continuous_on a b I f"
  obtains l u
  where "finite I"
      and "continuous_on ({a..b} - I) f"
      and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  using assms
  by (auto simp: piecewise_continuous_on_def Ball_def) metis

lemma piecewise_continuous_onI:
  assumes "finite I" "continuous_on ({a..b} - I) f"
    and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  shows "piecewise_continuous_on a b I f"
  using assms
  by (force simp: piecewise_continuous_on_def)

lemma piecewise_continuous_onI':
  fixes a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  assumes "finite I" "x. a < x  x < b  isCont f x"
    and "a  I  continuous (at_right a) f"
    and "b  I  continuous (at_left b) f"
    and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  shows "piecewise_continuous_on a b I f"
proof (rule piecewise_continuous_onI)
  have "x  I  a  x  x  b  (f  f x) (at x within {a..b})" for x
    using assms(2)[of x] assms(3,4)
    by (cases "a = x"; cases "b = x"; cases "x  {a<..<b}")
      (auto simp: at_within_Icc_at_left at_within_Icc_at_right isCont_def
        continuous_within filterlim_at_split at_within_interior)
  then show "continuous_on ({a .. b} - I) f"
    by (auto simp: continuous_on_def ‹finite I at_within_t1_space_avoid_finite)
qed fact+

lemma piecewise_continuous_onE':
  fixes a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  assumes "piecewise_continuous_on a b I f"
  obtains l u
  where "finite I"
      and "x. a < x  x < b  x  I  isCont f x"
      and "(x. a < x  x  b  (f  l x) (at_left x))"
      and "(x. a  x  x < b  (f  u x) (at_right x))"
      and "x. a  x  x  b  x  I  f x = l x"
      and "x. a  x  x  b  x  I  f x = u x"
proof -
  from piecewise_continuous_onE[OF assms] obtain l u
    where "finite I"
      and continuous: "continuous_on ({a..b} - I) f"
      and left: "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and right: "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
    by metis
  define l' where "l' x = (if x  I then l x else f x)" for x
  define u' where "u' x = (if x  I then u x else f x)" for x
  note ‹finite I
  moreover from continuous
  have "a < x  x < b  x  I  isCont f x" for x
    by (rule continuous_on_interior) (auto simp: interior_diff ‹finite I)
  moreover
  from continuous have "a < x  x  b  x  I  (f  f x) (at_left x)" for x
    by (cases "x = b")
     (auto simp: continuous_on_def at_within_t1_space_avoid_finite ‹finite I
        at_within_Icc_at_left at_within_interior filterlim_at_split
        dest!: bspec[where x=x])
  then have "a < x  x  b  (f  l' x) (at_left x)" for x
    by (auto simp: l'_def left)
  moreover
  from continuous have "a  x  x < b  x  I  (f  f x) (at_right x)" for x
    by (cases "x = a")
     (auto simp: continuous_on_def at_within_t1_space_avoid_finite ‹finite I
        at_within_Icc_at_right at_within_interior filterlim_at_split
        dest!: bspec[where x=x])
  then have "a  x  x < b  (f  u' x) (at_right x)" for x
    by (auto simp: u'_def right)
  moreover have "a  x  x  b  x  I  f x = l' x" for x by (auto simp: l'_def)
  moreover have "a  x  x  b  x  I  f x = u' x" for x by (auto simp: u'_def)
  ultimately show ?thesis ..
qed

lemma tendsto_avoid_at_within:
  "(f  l) (at x within X)"
  if "(f  l) (at x within X - {x})"
  using that
  by (auto simp: eventually_at_filter dest!: topological_tendstoD intro!: topological_tendstoI)

lemma tendsto_within_subset_eventuallyI:
  "(f  fx) (at x within X)"
  if g: "(g  gy) (at y within Y)"
    and ev: "F x in (at y within Y). f x = g x"
    and xy: "x = y"
    and fxgy: "fx = gy"
    and XY: "X - {x}  Y"
  apply (rule tendsto_avoid_at_within)
  apply (rule tendsto_within_subset[where S = "Y"])
  unfolding xy
   apply (subst tendsto_cong[OF ev ])
   apply (rule g[folded fxgy])
  apply (rule XY[unfolded xy])
  done

lemma piecewise_continuous_on_insertE:
  assumes "piecewise_continuous_on a b (insert i I) f"
  assumes "i  {a .. b}"
  obtains g h where
    "piecewise_continuous_on a i I g"
    "piecewise_continuous_on i b I h"
    "x. a  x  x < i  g x = f x"
    "x. i < x  x  b  h x = f x"
proof -
  from piecewise_continuous_onE[OF assms(1)] i  {a .. b} obtain l u where
        finite: "finite I"
    and cf: "continuous_on ({a..b} - insert i I) f"
    and l: "(i. i  I  a < i  i  b  (f  l i) (at_left i))" "i > a  (f  l i) (at_left i)"
    and u: "(i. i  I  a  i  i < b  (f  u i) (at_right i))" "i < b  (f  u i) (at_right i)"
    by auto (metis (mono_tags))

  have fl: "(f(i := x)  l j) (at_left j)" if "j  I" "a < j" "j  b" for j x
    using l(1)
    apply (rule tendsto_within_subset_eventuallyI)
        apply (auto simp: eventually_at_filter that)
    apply (cases "j  i")
    subgoal premises prems
      using t1_space_nhds[OF prems]
      by eventually_elim auto
    subgoal by simp
    done
  have fr: "(f(i := x)  u j) (at_right j)" if "j  I" "a  j" "j < b" for j x
    using u(1)
    apply (rule tendsto_within_subset_eventuallyI)
        apply (auto simp: eventually_at_filter that)
    apply (cases "j  i")
    subgoal premises prems
      using t1_space_nhds[OF prems]
      by eventually_elim auto
    subgoal by simp
    done
  from cf have tendsto: "(f  f x) (at x within {a..b} - insert i I)"
    if "x  {a .. b} - insert i I" for x using that
    by (auto simp: continuous_on_def)
  have "continuous_on ({a..i} - I) (f(i:=l i))"
    apply (cases "a = i")
    subgoal by (auto simp: continuous_on_def Diff_triv)
    unfolding continuous_on_def
    apply safe
    subgoal for x
      apply (cases "x = i")
      subgoal
        apply (rule tendsto_within_subset_eventuallyI)
            apply (rule l(2))
        by (auto simp: eventually_at_filter)
      subgoal
        apply (subst at_within_t1_space_avoid[symmetric], assumption)
        apply (rule tendsto_within_subset_eventuallyI[where y=x])
            apply (rule tendsto)
        using i  {a .. b} by (auto simp: eventually_at_filter)
      done
    done
  then have "piecewise_continuous_on a i I (f(i:=l i))"
    using i  {a .. b}
    by (auto intro!: piecewise_continuous_onI finite fl fr)

  moreover
  have "continuous_on ({i..b} - I) (f(i:=u i))"
    apply (cases "b = i")
    subgoal by (auto simp: continuous_on_def Diff_triv)
    unfolding continuous_on_def
    apply safe
    subgoal for x
      apply (cases "x = i")
      subgoal
        apply (rule tendsto_within_subset_eventuallyI)
            apply (rule u(2))
        by (auto simp: eventually_at_filter)
      subgoal
        apply (subst at_within_t1_space_avoid[symmetric], assumption)
        apply (rule tendsto_within_subset_eventuallyI[where y=x])
            apply (rule tendsto)
        using i  {a .. b} by (auto simp: eventually_at_filter)
      done
    done
  then have "piecewise_continuous_on i b I (f(i:=u i))"
    using i  {a .. b}
    by (auto intro!: piecewise_continuous_onI finite fl fr)
  moreover have "(f(i:=l i)) x = f x" if "a  x" "x < i" for x
    using that by auto
  moreover have "(f(i:=u i)) x = f x" if "i < x" "x  b" for x
    using that by auto
  ultimately show ?thesis ..
qed

lemma eventually_avoid_finite:
  "F x in at y within Y. x  I" if "finite I" for y::"'a::t1_space"
  using that
proof (induction)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
    apply (auto intro!: eventually_conj)
    apply (cases "y = x")
    subgoal by (simp add: eventually_at_filter)
    subgoal by (rule tendsto_imp_eventually_ne) (rule tendsto_ident_at)
    done
qed

lemma eventually_at_left_linorder:― ‹TODO: generalize @{thm eventually_at_left_real}
  "a > (b :: 'a :: linorder_topology)  eventually (λx. x  {b<..<a}) (at_left a)"
  unfolding eventually_at_left
  by auto

lemma eventually_at_right_linorder:― ‹TODO: generalize @{thm eventually_at_right_real}
  "a > (b :: 'a :: linorder_topology)  eventually (λx. x  {b<..<a}) (at_right b)"
  unfolding eventually_at_right
  by auto

lemma piecewise_continuous_on_congI:
  "piecewise_continuous_on a b I g"
  if "piecewise_continuous_on a b I f"
    and eq: "x. x  {a .. b} - I  g x = f x"
proof -
  from piecewise_continuous_onE[OF that(1)]
  obtain l u where finite: "finite I"
    and *:
    "continuous_on ({a..b} - I) f"
    "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    "i. i  I  a  i  i < b  (f  u i) (at_right i)"
    by blast
  note finite
  moreover
  from * have "continuous_on ({a..b} - I) g"
    using that(2)
    by (auto simp: eq cong: continuous_on_cong) (subst continuous_on_cong[OF refl eq]; assumption)
  moreover
  have "F x in at_left i. f x = g x" if "a < i" "i  b" for i
    using eventually_avoid_finite[OF ‹finite I, of i "{..<i}"]
      eventually_at_left_linorder[OF a < i]
    by eventually_elim (subst eq, use that in auto)
  then have "i  I  a < i  i  b  (g  l i) (at_left i)" for i
    using *(2)
    by (rule Lim_transform_eventually[rotated]) auto
  moreover
  have "F x in at_right i. f x = g x" if "a  i" "i < b" for i
    using eventually_avoid_finite[OF ‹finite I, of i "{i<..}"]
      eventually_at_right_linorder[OF i < b]
    by eventually_elim (subst eq, use that in auto)
  then have "i  I  a  i  i < b  (g  u i) (at_right i)" for i
    using *(3)
    by (rule Lim_transform_eventually[rotated]) auto
  ultimately
  show ?thesis
    by (rule piecewise_continuous_onI) auto
qed

lemma piecewise_continuous_on_cong[cong]:
  "piecewise_continuous_on a b I f  piecewise_continuous_on c d J g"
  if "a = c"
    "b = d"
    "I = J"
    "x. c  x  x  d  x  J  f x = g x"
  using that
  by (auto intro: piecewise_continuous_on_congI)

lemma tendsto_at_left_continuous_on_avoidI: "(f  g i) (at_left i)"
  if g: "continuous_on ({a..i} - I) g"
    and gf: "x. a < x  x < i  g x = f x"
    "i  I" "finite I" "a < i"
  for i::"'a::linorder_topology"
proof (rule Lim_transform_eventually)
  from that have "i  {a .. i}" by auto
  from g have "(g  g i) (at i within {a..i} - I)"
    using i  I i  {a .. i}
    by (auto elim!: piecewise_continuous_onE simp: continuous_on_def)
  then show "(g  g i) (at_left i)"
    by (metis that at_within_Icc_at_left at_within_t1_space_avoid_finite
        greaterThanLessThan_iff)
  show "F x in at_left i. g x = f x"
    using eventually_at_left_linorder[OF a < i]
    by eventually_elim (auto simp: a < i gf)
qed

lemma tendsto_at_right_continuous_on_avoidI: "(f  g i) (at_right i)"
  if g: "continuous_on ({i..b} - I) g"
    and gf: "x. i < x  x < b  g x = f x"
    "i  I" "finite I" "i < b"
  for i::"'a::linorder_topology"
proof (rule Lim_transform_eventually)
  from that have "i  {i .. b}" by auto
  from g have "(g  g i) (at i within {i..b} - I)"
    using i  I i  {i .. b}
    by (auto elim!: piecewise_continuous_onE simp: continuous_on_def)
  then show "(g  g i) (at_right i)"
    by (metis that at_within_Icc_at_right at_within_t1_space_avoid_finite
        greaterThanLessThan_iff)
  show "F x in at_right i. g x = f x"
    using eventually_at_right_linorder[OF i < b]
    by eventually_elim (auto simp: i < b gf)
qed

lemma piecewise_continuous_on_insert_leftI:
  "piecewise_continuous_on a b (insert a I) f" if "piecewise_continuous_on a b I f"
  apply (cases "a  I")
  subgoal using that by (auto dest: insert_absorb)
  subgoal
    using that
    apply (rule piecewise_continuous_onE)
    subgoal for l u
      apply (rule piecewise_continuous_onI[where u="u(a:=f a)"])
         apply (auto intro: continuous_on_subset )
      apply (rule tendsto_at_right_continuous_on_avoidI, assumption)
         apply auto
      done
    done
  done

lemma piecewise_continuous_on_insert_rightI:
  "piecewise_continuous_on a b (insert b I) f" if "piecewise_continuous_on a b I f"
  apply (cases "b  I")
  subgoal using that by (auto dest: insert_absorb)
  subgoal
    using that
    apply (rule piecewise_continuous_onE)
    subgoal for l u
      apply (rule piecewise_continuous_onI[where l="l(b:=f b)"])
         apply (auto intro: continuous_on_subset )
      apply (rule tendsto_at_left_continuous_on_avoidI, assumption)
         apply auto
      done
    done
  done

theorem piecewise_continuous_on_induct[consumes 1, case_names empty combine weaken]:
  assumes pc: "piecewise_continuous_on a b I f"
  assumes 1: "a b f. continuous_on {a .. b} f  P a b {} f"
  assumes 2: "a i b I f1 f2 f. a  i  i  b  i  I  P a i I f1  P i b I f2 
    piecewise_continuous_on a i I f1 
    piecewise_continuous_on i b I f2 
    (x. a  x  x < i  f1 x = f x) 
    (x. i < x  x  b  f2 x = f x) 
    (i > a  (f  f1 i) (at_left i)) 
    (i < b  (f  f2 i) (at_right i)) 
    P a b (insert i I) f"
  assumes 3: "a b i I f. P a b I f  finite I  i  I  P a b (insert i I) f"
  shows "P a b I f"
proof -
  from pc have "finite I"
    by (auto simp: piecewise_continuous_on_def)
  then show ?thesis
    using pc
  proof (induction I arbitrary: a b f)
    case empty
    then show ?case
      by (auto simp: piecewise_continuous_on_def 1)
  next
    case (insert i I)
    show ?case
    proof (cases "i  {a .. b}")
      case True
      from insert.prems[THEN piecewise_continuous_on_insertE, OF i  {a .. b}]
      obtain g h
        where g: "piecewise_continuous_on a i I g"
          and h: "piecewise_continuous_on i b I h"
          and gf: "x. a  x  x < i  g x = f x"
          and hf: "x. i < x  x  b  h x = f x"
        by metis
      from g have pcg: "piecewise_continuous_on a i I (f(i:=g i))"
        by (rule piecewise_continuous_on_congI) (auto simp: gf)
      from h have pch: "piecewise_continuous_on i b I (f(i:=h i))"
        by (rule piecewise_continuous_on_congI) (auto simp: hf)

      have fg: "(f  g i) (at_left i)" if "a < i"
        apply (rule tendsto_at_left_continuous_on_avoidI[where a=a and I=I])
        using g i  I a < i
        by (auto elim!: piecewise_continuous_onE simp: gf)
      have fh: "(f  h i) (at_right i)" if "i < b"
        apply (rule tendsto_at_right_continuous_on_avoidI[where b=b and I=I])
        using h i  I i < b
        by (auto elim!: piecewise_continuous_onE simp: hf)
      show ?thesis
        apply (rule 2)
        using True apply force
        using True apply force
                apply (rule insert)
               apply (rule insert.IH, rule pcg)
              apply (rule insert.IH, rule pch)
             apply fact
            apply fact
        using 3
        by (auto simp: fg fh)
    next
      case False
      with insert.prems
      have "piecewise_continuous_on a b I f"
        by (auto simp: piecewise_continuous_on_def)
      from insert.IH[OF this] show ?thesis
        by (rule 3) fact+
    qed
  qed
qed

lemma continuous_on_imp_piecewise_continuous_on:
  "continuous_on {a .. b} f  piecewise_continuous_on a b {} f"
  by (auto simp: piecewise_continuous_on_def)

lemma piecewise_continuous_on_imp_absolutely_integrable:
  fixes a b::real and f::"real  'a::euclidean_space"
  assumes "piecewise_continuous_on a b I f"
  shows "f absolutely_integrable_on {a..b}"
  using assms
proof (induction rule: piecewise_continuous_on_induct)
  case (empty a b f)
  show ?case
    by (auto intro!: absolutely_integrable_onI integrable_continuous_interval
          continuous_intros empty)
next
  case (combine a i b I f1 f2 f)
  from combine(10)
  have "f absolutely_integrable_on {a..i}"
    by (rule absolutely_integrable_spike[where S="{i}"]) (auto simp: combine)
  moreover
  from combine(11)
  have "f absolutely_integrable_on {i..b}"
    by (rule absolutely_integrable_spike[where S="{i}"]) (auto simp: combine)
  ultimately
  show ?case
    by (rule absolutely_integrable_on_combine) fact+
qed

lemma piecewise_continuous_on_integrable:
  fixes a b::real and f::"real  'a::euclidean_space"
  assumes "piecewise_continuous_on a b I f"
  shows "f integrable_on {a..b}"
  using piecewise_continuous_on_imp_absolutely_integrable[OF assms]
  unfolding absolutely_integrable_on_def by auto

lemma piecewise_continuous_on_comp:
  assumes p: "piecewise_continuous_on a b I f"
  assumes c: "x. isCont (λ(x, y). g x y) x"
  shows "piecewise_continuous_on a b I (λx. g x (f x))"
proof -
  from piecewise_continuous_onE[OF p]
  obtain l u
    where I: "finite I"
      and cf: "continuous_on ({a..b} - I) f"
      and l: "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and u: "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
    by metis
  note ‹finite I
  moreover
  from c have cg: "continuous_on UNIV (λ(x, y). g x y)"
    using c by (auto simp: continuous_on_def isCont_def intro: tendsto_within_subset)
  then have "continuous_on ({a..b} - I) (λx. g x (f x))"
    by (intro continuous_on_compose2[OF cg, where f="λx. (x, f x)", simplified])
      (auto intro!: continuous_intros cf)
  moreover
  note tendstcomp = tendsto_compose[OF c[unfolded isCont_def], where f="λx. (x, f x)", simplified, THEN tendsto_eq_rhs]
  have "((λx. g x (f x))  g i (u i)) (at_right i)" if "i  I" "a  i" "i < b" for i
    by (rule tendstcomp) (auto intro!: tendsto_eq_intros u[OF i  I] that)
  moreover
  have "((λx. g x (f x))  g i (l i)) (at_left i)" if "i  I" "a < i" "i  b" for i
    by (rule tendstcomp) (auto intro!: tendsto_eq_intros l[OF i  I] that)
  ultimately show ?thesis
    by (intro piecewise_continuous_onI)
qed

lemma bounded_piecewise_continuous_image:
  "bounded (f ` {a .. b})"
  if "piecewise_continuous_on a b I f" for a b::real
  using that
proof (induction rule: piecewise_continuous_on_induct)
  case (empty a b f)
  then show ?case by (auto intro!: compact_imp_bounded compact_continuous_image)
next
  case (combine a i b I f1 f2 f)
  have "(f ` {a..b})  (insert (f i) (f1 ` {a..i}  f2 ` {i..b}))"
    using combine
    by (auto simp: image_iff) (metis antisym_conv atLeastAtMost_iff le_cases not_less)
  also have "bounded "
    using combine by auto
  finally (bounded_subset[rotated]) show ?case .
qed

lemma tendsto_within_eventually:
  "(f  l) (at x within X)"
  if
    "(f  l) (at x within Y)"
    "F y in at x within X. y  Y"
  using _ that(1)
proof (rule tendsto_mono)
  show "at x within X  at x within Y"
  proof (rule filter_leI)
    fix P
    assume "eventually P (at x within Y)"
    with that(2) show "eventually P (at x within X)"
      unfolding eventually_at_filter
      by eventually_elim auto
  qed
qed

lemma at_within_eq_bot_lemma:
  "at x within {b..c} = (if x < b  b > c then bot else at x within {b..c})"
  for x b c::"'a::linorder_topology"
  by (auto intro!: not_in_closure_trivial_limitI)

lemma at_within_eq_bot_lemma2:
  "at x within {a..b} = (if x > b  a > b then bot else at x within {a..b})"
  for x a b::"'a::linorder_topology"
  by (auto intro!: not_in_closure_trivial_limitI)

lemma piecewise_continuous_on_combine:
  "piecewise_continuous_on a c J f"
  if "piecewise_continuous_on a b J f" "piecewise_continuous_on b c J f"
  using that
  apply (auto elim!: piecewise_continuous_onE)
  subgoal for l u l' u'
    apply (rule piecewise_continuous_onI[where
          l="λi. if i  b then l i else l' i" and
          u="λi. if i < b then u i else u' i"])
    subgoal by force
    subgoal
      apply (rule continuous_on_subset[where s="({a .. b}  {b .. c} - J)"])
      apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
       apply (rule Lim_Un)
      subgoal by auto
      subgoal by (subst at_within_eq_bot_lemma) auto
      apply (rule Lim_Un)
      subgoal by (subst at_within_eq_bot_lemma2) auto
      subgoal by auto
      done
    by auto
  done

lemma piecewise_continuous_on_finite_superset:
  "piecewise_continuous_on a b I f  I  J  finite J  piecewise_continuous_on a b J f"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  apply (auto simp add: piecewise_continuous_on_def)
    apply (rule continuous_on_subset, assumption, force)
  subgoal for i
    apply (cases "i  I")
     apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
    apply (drule bspec[where x=i])
     apply (auto simp: at_within_t1_space_avoid)
    apply (cases "i = b")
     apply (auto simp: at_within_Icc_at_left )
    apply (subst (asm) at_within_interior[where x=i])
    by (auto simp: filterlim_at_split)
  subgoal for i
    apply (cases "i  I")
     apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
    apply (drule bspec[where x=i])
     apply (auto simp: at_within_t1_space_avoid)
    apply (cases "i = a")
     apply (auto simp: at_within_Icc_at_right)
    apply (subst (asm) at_within_interior[where x=i])
    subgoal by (simp add: interior_Icc)
    by (auto simp: filterlim_at_split)
  done

lemma piecewise_continuous_on_splitI:
  "piecewise_continuous_on a c K f"
  if
    "piecewise_continuous_on a b I f"
    "piecewise_continuous_on b c J f"
    "I  K" "J  K" "finite K"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  apply (rule piecewise_continuous_on_combine[where b=b])
  subgoal
    by (rule piecewise_continuous_on_finite_superset, fact)
    (use that in auto elim!: piecewise_continuous_onE›)
  subgoal
    by (rule piecewise_continuous_on_finite_superset, fact)
    (use that in auto elim!: piecewise_continuous_onE›)
  done

end

Theory Existence

section ‹Existence›
theory Existence imports
  Piecewise_Continuous
begin

subsection ‹Definition›

definition has_laplace :: "(real  complex)  complex  complex  bool"
  (infixr "has'_laplace" 46)
  where "(f has_laplace L) s  ((λt. exp (t *R - s) * f t) has_integral L) {0..}"

lemma has_laplaceI:
  assumes "((λt. exp (t *R - s) * f t) has_integral L) {0..}"
  shows "(f has_laplace L) s"
  using assms
  by (auto simp: has_laplace_def)

lemma has_laplaceD:
  assumes "(f has_laplace L) s"
  shows "((λt. exp (t *R - s) * f t) has_integral L) {0..}"
  using assms
  by (auto simp: has_laplace_def)

lemma has_laplace_unique:
  "L = M" if
  "(f has_laplace L) s"
  "(f has_laplace M) s"
  using that
  by (auto simp: has_laplace_def has_integral_unique)


subsection ‹Condition for Existence: Exponential Order›

definition "exponential_order M c f  0 < M  (F t in at_top. norm (f t)  M * exp (c * t))"

lemma exponential_orderI:
  assumes "0 < M" and eo: "F t in at_top. norm (f t)  M * exp (c * t)"
  shows "exponential_order M c f"
  by (auto intro!: assms simp: exponential_order_def)

lemma exponential_orderD:
  assumes "exponential_order M c f"
  shows "0 < M" "F t in at_top. norm (f t)  M * exp (c * t)"
  using assms by (auto simp: exponential_order_def)

context
  fixes f::"real  complex"
begin

definition laplace_integrand::"complex  real  complex"
  where "laplace_integrand s t = exp (t *R - s) * f t"

lemma laplace_integrand_absolutely_integrable_on_Icc:
  "laplace_integrand s absolutely_integrable_on {a..b}"
  if "AE x{a..b} in lebesgue. cmod (f x)  B" "f integrable_on {a..b}"
  apply (cases "b  a")
  subgoal by (auto intro!: absolutely_integrable_onI integrable_negligible[OF negligible_real_ivlI])
proof goal_cases
  case 1
  have "compact ((λx. exp (- (x *R s))) ` {a .. b})"
    by (rule compact_continuous_image) (auto intro!: continuous_intros)
  then obtain C where C: "0  C" "a  x  x  b  cmod (exp (- (x *R s)))  C" for x
    using 1
    apply (auto simp: bounded_iff dest!: compact_imp_bounded)
    by (metis atLeastAtMost_iff exp_ge_zero order_refl order_trans scaleR_complex.sel(1))

  have m: "(λx. indicator {a..b} x *R f x)  borel_measurable lebesgue"
    apply (rule has_integral_implies_lebesgue_measurable)
    apply (rule integrable_integral)
    apply (rule that)
    done
  have "complex_set_integrable lebesgue {a..b} (λx. exp (- (x *R s)) * (indicator {a .. b} x *R f x))"
    unfolding set_integrable_def
    apply (rule integrableI_bounded_set_indicator[where B="C * B"])
       apply (simp; fail)
      apply (rule borel_measurable_times)
       apply measurable
        apply (simp add: measurable_completion)
       apply (simp add: measurable_completion)
      apply (rule m)
    apply (simp add: emeasure_lborel_Icc_eq)
    using that(1)
    apply eventually_elim
    apply (auto simp: norm_mult)
    apply (rule mult_mono)
    using C
    by auto
  then show ?case
    unfolding set_integrable_def
    by (simp add: laplace_integrand_def[abs_def] indicator_inter_arith[symmetric])
qed

lemma laplace_integrand_integrable_on_Icc:
  "laplace_integrand s integrable_on {a..b}"
  if "AE x{a..b} in lebesgue. cmod (f x)  B" "f integrable_on {a..b}"
  using laplace_integrand_absolutely_integrable_on_Icc[OF that]
  using set_lebesgue_integral_eq_integral(1) by blast

lemma eventually_laplace_integrand_le:
  "F t in at_top. cmod (laplace_integrand s t)  M * exp (- (Re s - c) * t)"
  if "exponential_order M c f"
  using exponential_orderD(2)[OF that]
proof (eventually_elim)
  case (elim t)
  show ?case
    unfolding laplace_integrand_def
    apply (rule norm_mult_ineq[THEN order_trans])
    apply (auto intro!: mult_left_mono[THEN order_trans, OF elim])
    apply (auto simp: exp_minus divide_simps algebra_simps exp_add[symmetric])
    done
qed

lemma
  assumes eo: "exponential_order M c f"
    and cs: "c < Re s"
  shows laplace_integrand_integrable_on_Ici_iff:
    "laplace_integrand s integrable_on {a..} 
      (k>a. laplace_integrand s integrable_on {a..k})"
    (is ?th1)
  and laplace_integrand_absolutely_integrable_on_Ici_iff:
    "laplace_integrand s absolutely_integrable_on {a..} 
      (k>a. laplace_integrand s absolutely_integrable_on {a..k})"
    (is ?th2)
proof -
  have "F t in at_top. a < (t::real)"
    using eventually_gt_at_top by blast
  then have "F t in at_top. t > a  cmod (laplace_integrand s t)  M * exp (- (Re s - c) * t)"
    using eventually_laplace_integrand_le[OF eo]
    by eventually_elim (auto)
  then obtain A where A: "A > a" and le: "t  A  cmod (laplace_integrand s t)  M * exp (- (Re s - c) * t)" for t
    unfolding eventually_at_top_linorder
    by blast

  let ?f = "λ(k::real) (t::real). indicat_real {A..k} t *R laplace_integrand s t"

  from exponential_orderD[OF eo] have "M  0" by simp
  have 2: "(λt. M * exp (- (Re s - c) * t)) integrable_on {A..}"
    unfolding integrable_on_cmult_iff[OF M  0] norm_exp_eq_Re
    by (rule integrable_on_exp_minus_to_infinity) (simp add: cs)

  have 3: "t{A..}  cmod (?f k t)  M * exp (- (Re s - c) * t)"
    (is "t_ ?lhs t  ?rhs t")
    for t k
  proof safe
    fix t assume "A  t"
    have "?lhs t  cmod (laplace_integrand s t)"
      by (auto simp: indicator_def)
    also have "  ?rhs t" using A  t le by (simp add: laplace_integrand_def)
    finally show "?lhs t  ?rhs t" .
  qed

  have 4: "t{A..}. ((λk. ?f k t)  laplace_integrand s t) at_top"
  proof safe
    fix t assume t: "t  A"
    have "F k in at_top. k  t"
      by (simp add: eventually_ge_at_top)
    then have "F k in at_top. laplace_integrand s t = ?f k t"
      by eventually_elim (use t in auto simp: indicator_def›)
    then show "((λk. ?f k t)  laplace_integrand s t) at_top" using tendsto_const
      by (rule Lim_transform_eventually[rotated])
  qed

  show th1: ?th1
  proof safe
    assume "k>a. laplace_integrand s integrable_on {a..k}"
    note li = this[rule_format]
    have liA: "laplace_integrand s integrable_on {A..k}" for k
    proof cases
      assume "k  A"
      then have "{A..k} = (if A = k then {k} else {})" by auto
      then show ?thesis by (auto intro!: integrable_negligible)
    next
      assume n: "¬ k  A"
      show ?thesis
        by (rule integrable_on_subinterval[OF li[of k]]) (use A n in auto)
    qed
    have "?f k integrable_on {A..k}" for k
      using liA[of k] negligible_empty
      by (rule integrable_spike) auto
    then have 1: "?f k integrable_on {A..}" for k
      by (rule integrable_on_superset) auto
    note 1 2 3 4
    note * = this[unfolded set_integrable_def]
    from li[of A] dominated_convergence_at_top(1)[OF *]
    show "laplace_integrand s integrable_on {a..}"
      by (rule integrable_Un') (use a < A in auto simp: max_def li›)
  qed (rule integrable_on_subinterval, assumption, auto)

  show ?th2
  proof safe
    assume ai: "k>a. laplace_integrand s absolutely_integrable_on {a..k}"
    then have "laplace_integrand s absolutely_integrable_on {a..A}"
      using A by auto
    moreover
    from ai have "k>a. laplace_integrand s integrable_on {a..k}"
      using set_lebesgue_integral_eq_integral(1) by blast
    with th1 have i: "laplace_integrand s integrable_on {a..}" by auto
    have 1: "?f k integrable_on {A..}" for k
      apply (rule integrable_on_superset[where S="{A..k}"])
      using _ negligible_empty
        apply (rule integrable_spike[where f="laplace_integrand s"])
        apply (rule integrable_on_subinterval)
         apply (rule i)
      by (use a < A in auto)
    have "laplace_integrand s absolutely_integrable_on {A..}"
      using _ dominated_convergence_at_top(1)[OF 1 2 3 4] 2
      by (rule absolutely_integrable_integrable_bound) (use le in auto)
    ultimately
    have "laplace_integrand s absolutely_integrable_on ({a..A}  {A..})"
      by (rule set_integrable_Un) auto
    also have "{a..A}  {A..} = {a..}" using a < A by auto
    finally show "local.laplace_integrand s absolutely_integrable_on {a..}" .
  qed (rule set_integrable_subset, assumption, auto)
qed

theorem laplace_exists_laplace_integrandI:
  assumes "laplace_integrand s integrable_on {0..}"
  obtains F where "(f has_laplace F) s"
proof -
  from assms
  have "(f has_laplace integral {0..} (laplace_integrand s)) s"
    unfolding has_laplace_def laplace_integrand_def by blast
  thus ?thesis ..
qed

lemma
  assumes eo: "exponential_order M c f"
    and pc: "k. AE x{0..k} in lebesgue. cmod (f x)  B k" "k. f integrable_on {0..k}"
    and s: "Re s > c"
  shows laplace_integrand_integrable: "laplace_integrand s integrable_on {0..}" (is ?th1)
    and laplace_integrand_absolutely_integrable:
      "laplace_integrand s absolutely_integrable_on {0..}" (is ?th2)
  using eo laplace_integrand_absolutely_integrable_on_Icc[OF pc] s
  by (auto simp: laplace_integrand_integrable_on_Ici_iff
      laplace_integrand_absolutely_integrable_on_Ici_iff
      set_lebesgue_integral_eq_integral)

lemma piecewise_continuous_on_AE_boundedE:
  assumes pc: "k. piecewise_continuous_on a k (I k) f"
  obtains B where "k. AE x{a..k} in lebesgue. cmod (f x)  B k"
  apply atomize_elim
  apply (rule choice)
  apply (rule allI)
  subgoal for k
    using bounded_piecewise_continuous_image[OF pc[of k]]
    by (force simp: bounded_iff)
  done

theorem piecewise_continuous_on_has_laplace:
  assumes eo: "exponential_order M c f"
    and pc: "k. piecewise_continuous_on 0 k (I k) f"
    and s: "Re s > c"
  obtains F where "(f has_laplace F) s"
proof -
  from piecewise_continuous_on_AE_boundedE[OF pc]
  obtain B where AE: "AE x{0..k} in lebesgue. cmod (f x)  B k" for k by force
  have int: "f integrable_on {0..k}" for k
    using pc
    by (rule piecewise_continuous_on_integrable)
  show ?thesis
    using pc
    apply (rule piecewise_continuous_on_AE_boundedE)
    apply (rule laplace_exists_laplace_integrandI)
     apply (rule laplace_integrand_integrable)
        apply (rule eo)
       apply assumption
      apply (rule int)
     apply (rule s)
    by (rule that)
qed

end


subsection ‹Concrete Laplace Transforms›

lemma exp_scaleR_has_vector_derivative_left'[derivative_intros]:
  "((λt. exp (t *R A)) has_vector_derivative A * exp (t *R A)) (at t within S)"
  by (metis exp_scaleR_has_vector_derivative_right exp_times_scaleR_commute)

lemma
  fixes a::complex―‹TODO: generalize›
  assumes a: "0 < Re a"
  shows integrable_on_cexp_minus_to_infinity: "(λx. exp (x *R - a)) integrable_on {c..}"
    and integral_cexp_minus_to_infinity:  "integral {c..} (λx. exp (x *R - a)) = exp (c *R - a) / a"
proof -
  from a have "a  0" by auto
  define f where "f = (λk x. if x  {c..real k} then exp (x *R -a) else 0)"
  {
    fix k :: nat assume k: "of_nat k  c"
    from a  0 k
      have "((λx. exp (x *R -a)) has_integral (-exp (k *R -a)/a - (-exp (c *R -a)/a))) {c..real k}"
      by (intro fundamental_theorem_of_calculus)
         (auto intro!: derivative_eq_intros exp_scaleR_has_vector_derivative_left
            simp: divide_inverse_commute
               simp del: scaleR_minus_left scaleR_minus_right)
    hence "(f k has_integral (exp (c *R -a)/a - exp (k *R -a)/a)) {c..}" unfolding f_def
      by (subst has_integral_restrict) simp_all
  } note has_integral_f = this

  have integrable_fk: "f k integrable_on {c..}" for k
  proof -
    have "(λx. exp (x *R -a)) integrable_on {c..of_real k}" (is ?P)
      unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
    then have int: "(f k) integrable_on {c..of_real k}"
      by (rule integrable_eq) (simp add: f_def)
    show ?thesis
      by (rule integrable_on_superset[OF int]) (auto simp: f_def)
  qed
  have limseq: "x. x {c..}  (λk. f k x)  exp (x *R - a)"
    apply (auto intro!: Lim_transform_eventually[OF tendsto_const] simp: f_def)
    by (meson eventually_sequentiallyI nat_ceiling_le_eq)
  have bnd: "x. x  {c..}  cmod (f k x)  exp (- Re a * x)" for k
    by (auto simp: f_def)

  have [simp]: "f k = (λ_. 0)" if "of_nat k < c" for k using that by (auto simp: fun_eq_iff f_def)
  have integral_f: "integral {c..} (f k) =
                      (if real k  c then exp (c *R -a)/a - exp (k *R -a)/a else 0)"
    for k using integral_unique[OF has_integral_f[of k]] by simp

  have "(λk. exp (c *R -a)/a - exp (k *R -a)/a)  exp (c*R-a)/a - 0/a"
    apply (intro tendsto_intros filterlim_compose[OF exp_at_bot]
          filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
     apply (rule tendsto_norm_zero_cancel)
    by (auto intro!: assms a  0 filterlim_real_sequentially
        filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top]
        filterlim_at_top_mult_tendsto_pos[OF tendsto_const])
  moreover
  note A = dominated_convergence[where g="λx. exp (x *R -a)",
    OF integrable_fk integrable_on_exp_minus_to_infinity[where a="Re a" and c=c, OF 0 < Re a]
      bnd limseq]
  from A(1) show "(λx. exp (x *R - a)) integrable_on {c..}" .
  from eventually_gt_at_top[of "nat c"] have "eventually (λk. of_nat k > c) sequentially"
    by eventually_elim linarith
  hence "eventually (λk. exp (c *R -a)/a - exp (k *R -a)/a = integral {c..} (f k)) sequentially"
    by eventually_elim (simp add: integral_f)
  ultimately have "(λk. integral {c..} (f k))  exp (c *R -a)/a - 0/a"
    by (rule Lim_transform_eventually)
  from LIMSEQ_unique[OF A(2) this]
  show "integral {c..} (λx. exp (x *R -a)) = exp (c *R -a)/a" by simp
qed

lemma has_integral_cexp_minus_to_infinity:
  fixes a::complex―‹TODO: generalize›
  assumes a: "0 < Re a"
  shows "((λx. exp (x *R - a)) has_integral exp (c *R - a) / a) {c..}"
  using integral_cexp_minus_to_infinity[OF assms]
    integrable_on_cexp_minus_to_infinity[OF assms]
  using has_integral_integrable_integral by blast

lemma has_laplace_one:
  "((λ_. 1) has_laplace inverse s) s" if "Re s > 0"
proof (safe intro!: has_laplaceI)
  from that have "((λt. exp (t *R - s)) has_integral inverse s) {0..}"
    by (rule has_integral_cexp_minus_to_infinity[THEN has_integral_eq_rhs])
       (auto simp: inverse_eq_divide)
  then show "((λt. exp (t *R - s) * 1) has_integral inverse s) {0..}" by simp
qed

lemma has_laplace_add:
  assumes f: "(f has_laplace F) S"
  assumes g: "(g has_laplace G) S"
  shows "((λx. f x + g x) has_laplace F + G) S"
  apply (rule has_laplaceI)
  using has_integral_add[OF has_laplaceD[OF f ] has_laplaceD[OF g]]
  by (auto simp: algebra_simps)

lemma has_laplace_cmul:
  assumes "(f has_laplace F) S"
  shows "((λx. r *R f x) has_laplace r *R F) S"
  apply (rule has_laplaceI)
  using has_laplaceD[OF assms, THEN has_integral_cmul[where c=r]]
  by auto

lemma has_laplace_uminus:
  assumes "(f has_laplace F) S"
  shows "((λx. - f x) has_laplace - F) S"
  using has_laplace_cmul[OF assms, of "-1"]
  by auto

lemma has_laplace_minus:
  assumes f: "(f has_laplace F) S"
  assumes g: "(g has_laplace G) S"
  shows "((λx. f x - g x) has_laplace F - G) S"
  using has_laplace_add[OF f has_laplace_uminus[OF g]]
  by simp

lemma has_laplace_spike:
  "(f has_laplace L) s"
  if L: "(g has_laplace L) s"
    and "negligible T"
    and "t. t  T  t  0  f t = g t"
  by (auto intro!: has_laplaceI has_integral_spike[where S="T", OF _ _ has_laplaceD[OF L]] that)


lemma has_laplace_frequency_shift:―‹First Translation Theorem in Schiff›
  "((λt. exp (t *R b) * f t) has_laplace L) s"
  if "(f has_laplace L) (s - b)"
  using that
  by (auto intro!: has_laplaceI dest!: has_laplaceD
      simp: mult_exp_exp algebra_simps)

theorem has_laplace_derivative_time_domain:
  "(f' has_laplace s * L - f0) s"
  if L: "(f has_laplace L) s"
    and f': "t. t > 0  (f has_vector_derivative f' t) (at t)"
    and f0: "(f  f0) (at_right 0)"
    and eo: "exponential_order M c f"
    and cs: "c < Re s"
    ―‹Proof and statement follow "The Laplace Transform: Theory and Applications" by Joel L. Schiff.›
proof (rule has_laplaceI)
  have ce: "continuous_on S (λt. exp (t *R - s))" for S
    by (auto intro!: continuous_intros)
  have de: "((λt. exp (t *R - s)) has_vector_derivative (- s * exp (- (t *R s)))) (at t)" for t
    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros ext)
  have "((λx. -s * (f x * exp (- (x *R s)))) has_integral - s * L) {0..}"
    apply (rule has_integral_mult_right)
    using has_laplaceD[OF L]
    by (auto simp: ac_simps)

  define g where "g x = (if x  0 then f0 else f x)" for x

  have eog: "exponential_order M c g"
  proof -
    from exponential_orderD[OF eo] have "0 < M"
      and ev: "F t in at_top. cmod (f t)  M * exp (c * t)" .
    have "F t::real in at_top. t > 0" by simp
    with ev have "F t in at_top. cmod (g t)  M * exp (c * t)"
      by eventually_elim (auto simp: g_def)
    with 0 < M show ?thesis
      by (rule exponential_orderI)
  qed
  have Lg: "(g has_laplace L) s"
    using L
    by (rule has_laplace_spike[where T="{0}"]) (auto simp: g_def)
  have g': "t. 0 < t  (g has_vector_derivative f' t) (at t)"
    using f'
    by (rule has_vector_derivative_transform_within_open[where S="{0<..}"]) (auto simp: g_def)
  have cg: "continuous_on {0..k} g" for k
    apply (auto simp: g_def continuous_on_def)
     apply (rule filterlim_at_within_If)
    subgoal by (rule tendsto_intros)
    subgoal
      apply (rule tendsto_within_subset)
       apply (rule f0)
      by auto
    subgoal premises prems for x
    proof -
      from prems have "0 < x" by auto
      from order_tendstoD[OF tendsto_ident_at this]
      have "eventually ((<) 0) (at x within {0..k})" by auto
      then have "F x in at x within {0..k}. f x = (if x  0 then f0 else f x)"
        by eventually_elim auto
      moreover
      note [simp] = at_within_open[where S="{0<..}"]
      have "continuous_on {0<..} f"
        by (rule continuous_on_vector_derivative)
          (auto simp add: intro!: f')
      then have "(f  f x) (at x within {0..k})"
        using 0 < x
        by (auto simp: continuous_on_def intro: Lim_at_imp_Lim_at_within)
      ultimately show ?thesis
        by (rule Lim_transform_eventually[rotated])
    qed
    done
  then have pcg: "piecewise_continuous_on 0 k {} g" for k
    by (auto simp: piecewise_continuous_on_def)
  from piecewise_continuous_on_AE_boundedE[OF this]
  obtain B where B: "AE x{0..k} in lebesgue. cmod (g x)  B k" for k by auto
  have 1: "laplace_integrand g s absolutely_integrable_on {0..}"
    apply (rule laplace_integrand_absolutely_integrable[OF eog])
      apply (rule B)
     apply (rule piecewise_continuous_on_integrable)
     apply (rule pcg)
    apply (rule cs)
    done
  then have csi: "complex_set_integrable lebesgue {0..} (λx. exp (x *R - s) * g x)"
    by (auto simp: laplace_integrand_def[abs_def])
  from has_laplaceD[OF Lg, THEN has_integral_improperE, OF csi]
  obtain J where J: "k. ((λt. exp (t *R - s) * g t) has_integral J k) {0..k}"
    and [tendsto_intros]: "(J  L) at_top"
    by auto
  have "((λx. -s * (exp (x *R - s) * g x)) has_integral -s * J k) {0..k}" for k
    by (rule has_integral_mult_right) (rule J)
  then have *: "((λx. g x * (- s * exp (- (x *R s)))) has_integral -s * J k) {0..k}" for k
    by (auto simp: algebra_simps)
  have "F k::real in at_top. k  0"
    using eventually_ge_at_top by blast
  then have evI: "F k in at_top. ((λt. exp (t *R - s) * f' t) has_integral
    g k * exp (k *R - s) + s * J k - g 0) {0..k}"
  proof eventually_elim
    case (elim k)
    show ?case
      apply (subst mult.commute)
      apply (rule integration_by_parts_interior[OF bounded_bilinear_mult], fact)
      apply (rule cg) apply (rule ce) apply (rule g') apply force apply (rule de)
      apply (rule has_integral_eq_rhs)
       apply (rule *)
      by (auto simp: )
  qed
  have t1: "((λx. g x * exp (x *R - s))  0) at_top"
    apply (subst mult.commute)
    unfolding laplace_integrand_def[symmetric]
    apply (rule Lim_null_comparison)
    apply (rule eventually_laplace_integrand_le[OF eog])
    apply (rule tendsto_mult_right_zero)
    apply (rule filterlim_compose[OF exp_at_bot])
    apply (rule filterlim_tendsto_neg_mult_at_bot)
      apply (rule tendsto_intros)
    using cs apply simp
    apply (rule filterlim_ident)
    done
  show "((λt. exp (t *R - s) * f' t) has_integral s * L - f0) {0..}"
    apply (rule has_integral_improper_at_topI[OF evI])
    subgoal
      apply (rule tendsto_eq_intros)
       apply (rule tendsto_intros)
        apply (rule t1)
       apply (rule tendsto_intros)
        apply (rule tendsto_intros)
       apply (rule tendsto_intros)
       apply (rule tendsto_intros)
      by (simp add: g_def)
    done
qed

lemma exp_times_has_integral:
  "((λt. exp (c * t)) has_integral (if c = 0 then t else exp (c * t) / c) - (if c = 0 then t0 else exp (c * t0) / c)) {t0 .. t}"
  if "t0  t"
  for c t::real
  apply (cases "c = 0")
  subgoal
    using that
    apply auto
    apply (rule has_integral_eq_rhs)
     apply (rule has_integral_const_real)
    by auto
  subgoal
    apply (rule fundamental_theorem_of_calculus)
    using that
    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
  done

lemma integral_exp_times:
  "integral {t0 .. t} (λt. exp (c * t)) = (if c = 0 then t - t0 else exp (c * t) / c - exp (c * t0) / c)"
  if "t0  t"
  for c t::real
  using exp_times_has_integral[OF that, of c] that
  by (auto split: if_splits)

lemma filtermap_times_pos_at_top: "filtermap ((*) e) at_top = at_top"
  if "e > 0"
  for e::real
  apply (rule filtermap_fun_inverse[of "(*) (inverse e)"])
    apply (rule filterlim_tendsto_pos_mult_at_top)
      apply (rule tendsto_intros)
  subgoal using that by simp
    apply (rule filterlim_ident)
    apply (rule filterlim_tendsto_pos_mult_at_top)
      apply (rule tendsto_intros)
  subgoal using that by simp
   apply (rule filterlim_ident)
  using that by auto

lemma exponential_order_additiveI:
  assumes "0 < M" and eo: "F t in at_top. norm (f t)  K + M * exp (c * t)" and "c  0"
  obtains M' where "exponential_order M' c f"
proof -
  consider "c = 0" | "c > 0" using c  0 by arith
  then show ?thesis
  proof cases
    assume "c = 0"
    have "exponential_order (max K 0 + M) c f"
      using eo
       apply (auto intro!: exponential_orderI add_nonneg_pos 0 < M simp: c = 0)
      apply (auto simp: max_def)
      using eventually_elim2 by force
    then show ?thesis ..
  next
    assume "c > 0"
    have "F t in at_top. norm (f t)  K + M * exp (c * t)"
      by fact
    moreover
    have "F t in (filtermap exp (filtermap ((*) c) at_top)). K < t"
      by (simp add: filtermap_times_pos_at_top c > 0 filtermap_exp_at_top)
    then have "F t in at_top. K < exp (c * t)"
      by (simp add: eventually_filtermap)
    ultimately
    have "F t in at_top. norm (f t)  (1 + M) * exp (c * t)"
      by eventually_elim (auto simp: algebra_simps)
    with add_nonneg_pos[OF zero_le_one 0 < M]
    have "exponential_order (1 + M) c f"
      by (rule exponential_orderI)
    then show ?thesis ..
  qed
qed

lemma exponential_order_integral:
  fixes f::"real  'a::banach"
  assumes I: "t. t  a  (f has_integral I t) {a .. t}"
    and eo: "exponential_order M c f"
    and "c > 0"
  obtains M' where "exponential_order M' c I"
proof -
  from exponential_orderD[OF eo] have "0 < M"
    and bound: "F t in at_top. norm (f t)  M * exp (c * t)"
    by auto
  have "F t in at_top. t > a"
    by simp
  from bound this
  have "F t in at_top. norm (f t)  M * exp (c * t)  t > a"
    by eventually_elim auto
  then obtain t0 where t0: "t. t  t0  norm (f t)  M * exp (c * t)" "t0 > a"
    by (auto simp: eventually_at_top_linorder)
  have "F t in at_top. t > t0" by simp
  then have "F t in at_top. norm (I t)  norm (integral {a..t0} f) - M * exp (c * t0) / c + (M / c) * exp (c * t)"
  proof eventually_elim
    case (elim t) then have that: "t  t0" by simp
    from t0 have "a  t0" by simp
    have "f integrable_on {a .. t0}" "f integrable_on {t0 .. t}"
      subgoal by (rule has_integral_integrable[OF I[OF a  t0]])
      subgoal
        apply (rule integrable_on_subinterval[OF has_integral_integrable[OF I[where t=t]]])
        using t0 > a that by auto
      done
    have "I t = integral {a .. t0} f + integral {t0 .. t} f"
      by (smt I a  t0 f integrable_on {t0..t} has_integral_combine has_integral_integrable_integral that)
    also have "norm   norm (integral {a .. t0} f) + norm (integral {t0 .. t} f)" by norm
    also
    have "norm (integral {t0 .. t} f)  integral {t0 .. t} (λt. M * exp (c * t))"
      apply (rule integral_norm_bound_integral)
        apply fact
      by (auto intro!: integrable_continuous_interval continuous_intros t0)
    also have " = M * integral {t0 .. t} (λt. exp (c * t))"
      by simp
    also have "integral {t0 .. t} (λt. exp (c * t)) = exp (c * t) / c - exp (c * t0) / c"
      using c > 0 t0  t
      by (subst integral_exp_times) auto
    finally show ?case
      using c > 0
      by (auto simp: algebra_simps)
  qed
  from exponential_order_additiveI[OF divide_pos_pos[OF 0 < M 0 < c] this less_imp_le[OF 0 < c]]
  obtain M' where "exponential_order M' c I" .
  then show ?thesis ..
qed

lemma integral_has_vector_derivative_piecewise_continuous:
  fixes f :: "real  'a::euclidean_space"―‹TODO: generalize?›
  assumes "piecewise_continuous_on a b D f"
  shows "x. x  {a .. b} - D 
    ((λu. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b} - D)"
  using assms
proof (induction a b D f rule: piecewise_continuous_on_induct)
  case (empty a b f)
  then show ?case
    by (auto intro: integral_has_vector_derivative)
next
  case (combine a i b I f1 f2 f)
  then consider "x < i" | "i < x" by auto arith

  then show ?case
  proof cases―‹TODO: this is very explicit...›
    case 1
    have evless: "F xa in nhds x. xa < i"
      apply (rule order_tendstoD[OF _ x < i])
      by (simp add: filterlim_ident)
    have eq: "at x within {a..b} - insert i I = at x within {a .. i} - I"
      unfolding filter_eq_iff
    proof safe
      fix P
      assume "eventually P (at x within {a..i} - I)"
      with evless show "eventually P (at x within {a..b} - insert i I)"
        unfolding eventually_at_filter
        by eventually_elim auto
    next
      fix P
      assume "eventually P (at x within {a..b} - insert i I)"
      with evless show "eventually P (at x within {a..i} - I)"
        unfolding eventually_at_filter
        apply eventually_elim
        using 1 combine
        by auto
    qed
    have "f x = f1 x" using combine 1 by auto
    have i_eq: "integral {a..y} f = integral {a..y} f1" if "y < i" for y
      using negligible_empty
      apply (rule integral_spike)
      using combine 1 that
      by auto
    from evless have ev_eq: "F x in nhds x. x  {a..i} - I  integral {a..x} f = integral {a..x} f1"
      by eventually_elim (auto simp: i_eq)
    show ?thesis unfolding eq f x = f1 x
      apply (subst has_vector_derivative_cong_ev[OF ev_eq])
      using combine.IH[of x]
      using combine.hyps combine.prems 1
      by (auto simp: i_eq)
  next
    case 2
    have evless: "F xa in nhds x. xa > i"
      apply (rule order_tendstoD[OF _ x > i])
      by (simp add: filterlim_ident)
    have eq: "at x within {a..b} - insert i I = at x within {i .. b} - I"
      unfolding filter_eq_iff
    proof safe
      fix P
      assume "eventually P (at x within {i..b} - I)"
      with evless show "eventually P (at x within {a..b} - insert i I)"
        unfolding eventually_at_filter
        by eventually_elim auto
    next
      fix P
      assume "eventually P (at x within {a..b} - insert i I)"
      with evless show "eventually P (at x within {i..b} - I)"
        unfolding eventually_at_filter
        apply eventually_elim
        using 2 combine
        by auto
    qed
    have "f x = f2 x" using combine 2 by auto
    have i_eq: "integral {a..y} f = integral {a..i} f + integral {i..y} f2" if "i < y" "y  b" for y
    proof -
      have "integral {a..y} f = integral {a..i} f + integral {i..y} f"
        apply (cases "i = y")
        subgoal by auto
        subgoal
          apply (rule Henstock_Kurzweil_Integration.integral_combine[symmetric])
          using combine that apply auto
          apply (rule integrable_Un'[where A="{a .. i}" and B="{i..y}"])
          subgoal
            by (rule integrable_spike[where S="{i}" and f="f1"])
              (auto intro: piecewise_continuous_on_integrable)
          subgoal
            apply (rule integrable_on_subinterval[where S="{i..b}"])
            by (rule integrable_spike[where S="{i}" and f="f2"])
              (auto intro: piecewise_continuous_on_integrable)
          subgoal by (auto simp: max_def min_def)
          subgoal by auto
          done
        done
      also have "integral {i..y} f = integral {i..y} f2"
        apply (rule integral_spike[where S="{i}"])
        using combine 2 that
        by auto
      finally show ?thesis .
    qed
    from evless have ev_eq: "F y in nhds x. y  {i..b} - I  integral {a..y} f = integral {a..i} f + integral {i..y} f2"
      by eventually_elim (auto simp: i_eq)
    show ?thesis unfolding eq
      apply (subst has_vector_derivative_cong_ev[OF ev_eq])
      using combine.IH[of x] combine.prems combine.hyps 2
      by (auto simp: i_eq intro!: derivative_eq_intros)
  qed
qed (auto intro: has_vector_derivative_within_subset)

lemma has_derivative_at_split:
  "(f has_derivative f') (at x)  (f has_derivative f') (at_left x)  (f has_derivative f') (at_right x)"
  for x::"'a::{linorder_topology, real_normed_vector}"
  by (auto simp: has_derivative_at_within filterlim_at_split)

lemma has_vector_derivative_at_split:
  "(f has_vector_derivative f') (at x) 
   (f has_vector_derivative f') (at_left x) 
   (f has_vector_derivative f') (at_right x)"
  using has_derivative_at_split[of f "λh. h *R f'" x]
  by (simp add: has_vector_derivative_def)

lemmas differentiableI_vector[intro]

lemma differentiable_at_splitD:
  "f differentiable at_left x"
  "f differentiable at_right x"
  if "f differentiable (at x)"
  for x::real
  using that[unfolded vector_derivative_works has_vector_derivative_at_split]
  by auto

lemma integral_differentiable:
  fixes f :: "real  'a::banach"
  assumes "continuous_on {a..b} f"
    and "x  {a..b}"
  shows "(λu. integral {a..u} f) differentiable at x within {a..b}"
  using integral_has_vector_derivative[OF assms]
  by blast

theorem integral_has_vector_derivative_piecewise_continuous':
  fixes f :: "real  'a::euclidean_space"―‹TODO: generalize?›
  assumes "piecewise_continuous_on a b D f" "a < b"
  shows
    "(x. a < x  x < b  x  D  (λu. integral {a..u} f) differentiable at x) 
    (x. a  x  x < b  (λt. integral {a..t} f) differentiable at_right x) 
    (x. a < x  x  b  (λt. integral {a..t} f) differentiable at_left x)"
  using assms
proof (induction a b D f rule: piecewise_continuous_on_induct)
  case (empty a b f)
  have "a < x  x < b  (λu. integral {a..u} f) differentiable (at x)" for x
    using integral_differentiable[OF empty(1), of x]
    by (auto simp: at_within_interior)
  then show ?case
    using integral_differentiable[OF empty(1), of a]
      integral_differentiable[OF empty(1), of b]
      a < b
    by (auto simp: at_within_Icc_at_right at_within_Icc_at_left le_less
        intro: differentiable_at_withinI)
next
  case (combine a i b I f1 f2 f)
  from ‹piecewise_continuous_on a i I f1 have "finite I"
    by (auto elim!: piecewise_continuous_onE)

  from combine(4) have "piecewise_continuous_on a i (insert i I) f1"
    by (rule piecewise_continuous_on_insert_rightI)
  then have "piecewise_continuous_on a i (insert i I) f"
    by (rule piecewise_continuous_on_congI) (auto simp: combine)
  moreover
  from combine(5) have "piecewise_continuous_on i b (insert i I) f2"
    by (rule piecewise_continuous_on_insert_leftI)
  then have "piecewise_continuous_on i b (insert i I) f"
    by (rule piecewise_continuous_on_congI) (auto simp: combine)
  ultimately have "piecewise_continuous_on a b (insert i I) f"
    by (rule piecewise_continuous_on_combine)
  then have f_int: "f integrable_on {a .. b}"
    by (rule piecewise_continuous_on_integrable)

  from combine.IH
  have f1: "x>a  x < i  x  I  (λu. integral {a..u} f1) differentiable (at x)"
    "xa  x < i  (λt. integral {a..t} f1) differentiable (at_right x)"
    "x>a  x  i  (λt. integral {a..t} f1) differentiable (at_left x)"
   and f2: "x>i  x < b  x  I  (λu. integral {i..u} f2) differentiable (at x)"
    "xi  x < b  (λt. integral {i..t} f2) differentiable (at_right x)"
    "x>i  x  b  (λt. integral {i..t} f2) differentiable (at_left x)"
    for x
    by auto

  have "(λu. integral {a..u} f) differentiable at x" if "a < x" "x < b" "x  i" "x  I" for x
  proof -
    from that consider "x < i" |"i < x" by arith
    then show ?thesis
    proof cases
      case 1
      have at: "at x within {a<..<i} - I = at x"
        using that 1
        by (intro at_within_open) (auto intro!: open_Diff finite_imp_closed ‹finite I)
      then have "(λu. integral {a..u} f1) differentiable at x within {a<..<i} - I"
        using that 1 f1 by auto
      then have "(λu. integral {a..u} f) differentiable at x within {a<..<i} - I"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 1 by (auto intro!: integral_cong)
      then show ?thesis by (simp add: at)
    next
      case 2
      have at: "at x within {i<..<b} - I = at x"
        using that 2
        by (intro at_within_open) (auto intro!: open_Diff finite_imp_closed ‹finite I)
      then have "(λu. integral {a..i} f + integral {i..u} f2) differentiable at x within {i<..<b} - I"
        using that 2 f2 by auto
      then have "(λu. integral {a..i} f + integral {i..u} f) differentiable at x within {i<..<b} - I"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 2 by (auto intro!: integral_spike[where S="{i,x}"])
      then have "(λu. integral {a..u} f) differentiable at x within {i<..<b} - I"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        subgoal using that 2 by auto
        apply (auto simp: )
        apply (subst Henstock_Kurzweil_Integration.integral_combine)
        using that 2 a  i
        apply auto
        by (auto intro: integrable_on_subinterval f_int)
      then show ?thesis by (simp add: at)
    qed
  qed
  moreover
  have "(λt. integral {a..t} f) differentiable at_right x" if "a  x" "x < b" for x
  proof -
    from that consider "x < i" |"i  x" by arith
    then show ?thesis
    proof cases
      case 1
      have at: "at x within {x..i} = at_right x"
        using x < i by (rule at_within_Icc_at_right)
      then have "(λu. integral {a..u} f1) differentiable at x within {x..i}"
        using that 1 f1 by auto
      then have "(λu. integral {a..u} f) differentiable at x within {x..i}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 1 by (auto intro!: integral_spike[where S="{i,x}"])
      then show ?thesis by (simp add: at)
    next
      case 2
      have at: "at x within {x..b} = at_right x"
        using x < b by (rule at_within_Icc_at_right)
      then have "(λu. integral {a..i} f + integral {i..u} f2) differentiable at x within {x..b}"
        using that 2 f2 by auto
      then have "(λu. integral {a..i} f + integral {i..u} f) differentiable at x within {x..b}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 2 by (auto intro!: integral_spike[where S="{i,x}"])
      then have "(λu. integral {a..u} f) differentiable at x within {x..b}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        subgoal using that 2 by auto
        apply (auto simp: )
        apply (subst Henstock_Kurzweil_Integration.integral_combine)
        using that 2 a  i
        apply auto
        by (auto intro: integrable_on_subinterval f_int)
      then show ?thesis by (simp add: at)
    qed
  qed
  moreover
  have "(λt. integral {a..t} f) differentiable at_left x" if "a < x" "x  b" for x
  proof -
    from that consider "x  i" |"i < x" by arith
    then show ?thesis
    proof cases
      case 1
      have at: "at x within {a..x} = at_left x"
        using a < x by (rule at_within_Icc_at_left)
      then have "(λu. integral {a..u} f1) differentiable at x within {a..x}"
        using that 1 f1 by auto
      then have "(λu. integral {a..u} f) differentiable at x within {a..x}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 1 by (auto intro!: integral_spike[where S="{i,x}"])
      then show ?thesis by (simp add: at)
    next
      case 2
      have at: "at x within {i..x} = at_left x"
        using i < x by (rule at_within_Icc_at_left)
      then have "(λu. integral {a..i} f + integral {i..u} f2) differentiable at x within {i..x}"
        using that 2 f2 by auto
      then have "(λu. integral {a..i} f + integral {i..u} f) differentiable at x within {i..x}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        using that combine.hyps 2 by (auto intro!: integral_spike[where S="{i,x}"])
      then have "(λu. integral {a..u} f) differentiable at x within {i..x}"
        apply (rule differentiable_transform_within[OF _ zero_less_one])
        subgoal using that 2 by auto
        apply (auto simp: )
        apply (subst Henstock_Kurzweil_Integration.integral_combine)
        using that 2 a  i
        apply auto
        by (auto intro: integrable_on_subinterval f_int)
      then show ?thesis by (simp add: at)
    qed
  qed
  ultimately
  show ?case
    by auto
next
  case (weaken a b i I f)
  from weaken.IH[OF a < b]
  obtain l u where IH:
    "x. a < x  x < b  x  I  (λu. integral {a..u} f) differentiable (at x)"
    "x. a  x  x < b  (λt. integral {a..t} f) differentiable (at_right x)"
    "x. a < x  x  b  (λt. integral {a..t} f) differentiable (at_left x)"
    by metis
  then show ?case by auto
qed

lemma "closure (-S)  closure S = frontier S"
  by (auto simp add: frontier_def closure_complement)

theorem integral_time_domain_has_laplace:
  "((λt. integral {0 .. t} f) has_laplace L / s) s"
  if pc: "k. piecewise_continuous_on 0 k D f"
    and eo: "exponential_order M c f"
    and L: "(f has_laplace L) s"
    and s: "Re s > c"
    and c: "c > 0"
    and TODO: "D = {}" ― ‹TODO: generalize to actual piecewise_continuous_on›
  for f::"real  complex"
proof -
  define I where "I = (λt. integral {0 .. t} f)"
  have I': "(I has_vector_derivative f t) (at t within {0..x} - D)"
    if "t  {0 .. x} - D"
    for x t
    unfolding I_def
    by (rule integral_has_vector_derivative_piecewise_continuous; fact)
  have fi: "f integrable_on {0..t}" for t
    by (rule piecewise_continuous_on_integrable) fact
  have Ic: "continuous_on {0 .. t} I" for t
    unfolding I_def using fi
    by (rule indefinite_integral_continuous_1)
  have Ipc: "piecewise_continuous_on 0 t {} I" for t
    by (rule piecewise_continuous_onI) (auto intro!: Ic)
  have I: "(f has_integral I t) {0 .. t}" for t
    unfolding I_def
    using fi
    by (rule integrable_integral)
  from exponential_order_integral[OF I eo 0 < c] obtain M'
    where Ieo: "exponential_order M' c I" .
  have Ili: "laplace_integrand I s integrable_on {0..}"
    using Ipc
    apply (rule piecewise_continuous_on_AE_boundedE)
    apply (rule laplace_integrand_integrable)
    apply (rule Ieo)
      apply assumption
     apply (rule integrable_continuous_interval)
     apply (rule Ic)
    apply (rule s)
    done
  then obtain LI where LI: "(I has_laplace LI) s"
    by (rule laplace_exists_laplace_integrandI)

  from piecewise_continuous_onE[OF pc] have ‹finite D by auto
  have I'2: "(I has_vector_derivative f t) (at t)" if "t > 0" "t  D" for t
    apply (subst at_within_open[symmetric, where S="{0<..<t+1} - D"])
    subgoal using that by auto
    subgoal by (auto intro!:open_Diff finite_imp_closed ‹finite D)
    subgoal using I'[where x="t + 1"]
      apply (rule has_vector_derivative_within_subset)
      using that
      by auto
    done
  have I_tndsto: "(I  0) (at_right 0)"
    apply (rule tendsto_eq_rhs)
     apply (rule continuous_on_Icc_at_rightD)
      apply (rule Ic)
    apply (rule zero_less_one)
    by (auto simp: I_def)
  have "(f has_laplace s * LI - 0) s"
    by (rule has_laplace_derivative_time_domain[OF LI I'2 I_tndsto Ieo s])
      (auto simp: TODO)
  from has_laplace_unique[OF this L] have "LI = L / s"
    using s c by auto
  with LI show "(I has_laplace L / s) s" by simp
qed

subsection ‹higher derivatives›

definition "nderiv i f X = ((λf. (λx. vector_derivative f (at x within X)))^^i) f"

definition "ndiff n f X  (i<n. x  X. nderiv i f X differentiable at x within X)"

lemma nderiv_zero[simp]: "nderiv 0 f X = f"
  by (auto simp: nderiv_def)

lemma nderiv_Suc[simp]:
  "nderiv (Suc i) f X x = vector_derivative (nderiv i f X) (at x within X)"
  by (auto simp: nderiv_def)

lemma ndiff_zero[simp]: "ndiff 0 f X"
  by (auto simp: ndiff_def)

lemma ndiff_Sucs[simp]:
  "ndiff (Suc i) f X 
    (ndiff i f X) 
    (x  X. (nderiv i f X) differentiable (at x within X))"
  apply (auto simp: ndiff_def )
  using less_antisym by blast

theorem has_laplace_vector_derivative:
  "((λt. vector_derivative f (at t)) has_laplace s * L - f0) s"
  if L: "(f has_laplace L) s"
    and f': "t. t > 0  f differentiable (at t)"
    and f0: "(f  f0) (at_right 0)"
    and eo: "exponential_order M c f"
    and cs: "c < Re s"
proof -
  have f': "(t. 0 < t  (f has_vector_derivative vector_derivative f (at t)) (at t))"
    using f'
    by (subst vector_derivative_works[symmetric])
  show ?thesis
    by (rule has_laplace_derivative_time_domain[OF L f' f0 eo cs])
qed

lemma has_laplace_nderiv:
  "(nderiv n f {0<..} has_laplace s^n * L - (i<n. s^(n - Suc i) * f0 i)) s"
  if L: "(f has_laplace L) s"
    and f': "ndiff n f {0<..}"
    and f0: "i. i < n  (nderiv i f {0<..}  f0 i) (at_right 0)"
    and eo: "i. i < n  exponential_order M c (nderiv i f {0<..})"
    and cs: "c < Re s"
  using f' f0 eo
proof (induction n)
  case 0
  then show ?case
    by (auto simp: L)
next
  case (Suc n)
  have awo: "at t within {0<..} = at t" if "t > 0" for t::real
    using that
    by (subst at_within_open) auto
  have "((λa. vector_derivative (nderiv n f {0<..}) (at a)) has_laplace
    s * ( s ^ n * L - (i<n. s^(n - Suc i) * f0 i)) - f0 n) s"
    (is "(_ has_laplace ?L) _")
    apply (rule has_laplace_vector_derivative)
        apply (rule Suc.IH)
    subgoal using Suc.prems by auto
    subgoal using Suc.prems by auto
    subgoal using Suc.prems by auto
    subgoal using Suc.prems by (auto simp: awo)
    subgoal using Suc.prems by auto
     apply (rule Suc.prems; force)
    apply (rule cs)
    done
  also have "?L = s ^ Suc n * L - (i<Suc n. s ^ (Suc n - Suc i) * f0 i)"
    by (auto simp: algebra_simps sum_distrib_left diff_Suc Suc_diff_le
        split: nat.splits
        intro!: sum.cong)
  finally show ?case
    by (rule has_laplace_spike[where T="{0}"]) (auto simp: awo)
qed

end

Theory Lerch_Lemma

section ‹Lerch Lemma›
theory Lerch_Lemma
  imports
     "HOL-Analysis.Analysis"
begin

text ‹The main tool to prove uniqueness of the Laplace transform.›

lemma lerch_lemma_real:
  fixes h::"real  real"
  assumes h_cont[continuous_intros]: "continuous_on {0 .. 1} h"
  assumes int_0: "n. ((λu. u ^ n * h u) has_integral 0) {0 .. 1}"
  assumes u: "0  u" "u  1"
  shows "h u = 0"
proof -
  from Stone_Weierstrass_uniform_limit[OF compact_Icc h_cont]
  obtain g where g: "uniform_limit {0..1} g h sequentially" "polynomial_function (g n)" for n
    by blast
  then have rpf_g: "real_polynomial_function (g n)" for n
    by (simp add: real_polynomial_function_eq)

  let ?P = "λn x. h x * g n x"
  have continuous_on_g[continuous_intros]: "continuous_on s (g n)" for s n
    by (rule continuous_on_polymonial_function) fact
  have P_cont: "continuous_on {0 .. 1} (?P n)" for n
    by (auto intro!: continuous_intros)
  have "uniform_limit {0 .. 1} (λn x. h x * g n x) (λx. h x * h x) sequentially"
    by (auto intro!: uniform_limit_intros g assms compact_imp_bounded compact_continuous_image)

  from uniform_limit_integral[OF this P_cont]
  obtain I J where
    I: "(n. (?P n has_integral I n) {0..1})"
    and J: "((λx. h x * h x) has_integral J) {0..1}"
    and IJ: "I  J"
    by auto

  have "(?P n has_integral 0) {0..1}" for n
  proof -
    from real_polynomial_function_imp_sum[OF rpf_g]
    obtain gn ga where "g n = (λx. ign. ga i * x ^ i)" by metis
    then have "?P n x = (ign. x ^ i * h x * ga i)" for x
      by (auto simp: sum_distrib_left algebra_simps)
    moreover have "((λx.  x) has_integral 0) {0 .. 1}"
      by (auto intro!: has_integral_sum[THEN has_integral_eq_rhs] has_integral_mult_left assms)
    ultimately show ?thesis by simp
  qed
  with I have "I n = 0" for n
    using has_integral_unique by blast
  with IJ J have "((λx. h x * h x) has_integral 0) (cbox 0 1)"
    by (metis (full_types) LIMSEQ_le_const LIMSEQ_le_const2 box_real(2) dual_order.antisym order_refl)
  with _ _ have "h u * h u = 0"
    by (rule has_integral_0_cbox_imp_0) (auto intro!: continuous_intros u)
  then show "h u = 0"
    by simp
qed

lemma lerch_lemma:
  fixes h::"real  'a::euclidean_space"
  assumes [continuous_intros]: "continuous_on {0 .. 1} h"
  assumes int_0: "n. ((λu. u ^ n *R h u) has_integral 0) {0 .. 1}"
  assumes u: "0  u" "u  1"
  shows "h u = 0"
proof (rule euclidean_eqI)
  fix b::'a assume "b  Basis"
  have "continuous_on {0 .. 1} (λx. h x  b)"
    by (auto intro!: continuous_intros)
  moreover
  from b  Basis› have "((λu. u ^ n * (h u  b)) has_integral 0) {0 .. 1}" for n
    using int_0[of n] has_integral_componentwise_iff[of "λu. u ^ n *R h u" 0 "{0 .. 1}"]
    by auto
  moreover note u
  ultimately show "h u  b = 0  b"
    unfolding inner_zero_left
    by (rule lerch_lemma_real)
qed

end

Theory Uniqueness

section ‹Uniqueness of Laplace Transform›
theory Uniqueness
  imports
    "Existence"
    "Lerch_Lemma"
begin

text ‹We show uniqueness of the Laplace transform for continuous functions.›

lemma laplace_transform_zero:― ‹should also work for piecewise continuous›
  assumes cont_f: "continuous_on {0..} f"
  assumes eo: "exponential_order M a f"
  assumes laplace: "s. Re s > a  (f has_laplace 0) s"
  assumes "t  0"
  shows "f t = 0"
proof -
  define I where "I  λs k. integral {0..k} (laplace_integrand f s)"
  have bounded_image: "bounded (f ` {0..b})" for b
    by (auto intro!: compact_imp_bounded compact_continuous_image cont_f intro: continuous_on_subset)
  obtain B where B: "x{0..b}. cmod (f x)  B b" for b
    apply atomize_elim
    apply (rule choice)
    using bounded_image[unfolded bounded_iff]
    by auto
  have fi: "f integrable_on {0..b}" for b
    by (auto intro!: integrable_continuous_interval intro: continuous_on_subset cont_f)
  have aint: "complex_set_integrable lebesgue {0..b} (laplace_integrand f s)" for b s
    by (rule laplace_integrand_absolutely_integrable_on_Icc[OF
          AE_BallI[OF bounded_le_Sup[OF bounded_image]] fi])
  have int: "((λt. exp (t *R - s) * f t) has_integral I s b) {0 .. b}" for s b
    using aint[of b s]
    unfolding laplace_integrand_def[symmetric] I_def absolutely_integrable_on_def
    by blast
  have I_integral: "Re s > a  (I s  integral {0..} (laplace_integrand f s)) at_top" for s
    unfolding I_def
    by (metis aint eo improper_integral_at_top laplace_integrand_absolutely_integrable_on_Ici_iff)
  have imp: "(I s  0) at_top" if s: "Re s > a" for s
    using I_integral[of s] laplace[unfolded has_laplace_def, rule_format, OF s] s
    unfolding has_laplace_def I_def laplace_integrand_def
    by (simp add: integral_unique)

  define s0 where "s0 = a + 1"
  then have "s0 > a" by auto
  have "F x in at_right (0::real). 0 < x  x < 1"
    by (auto intro!: eventually_at_rightI)
  moreover
  from exponential_orderD(2)[OF eo]
  have "F t in at_right 0. cmod (f (- ln t))  M * exp (a * (- ln t))"
    unfolding at_top_mirror filtermap_ln_at_right[symmetric] eventually_filtermap .
  ultimately have "F x in at_right 0. cmod ((x powr s0) * f (- ln x))  M * x powr (s0 - a)"
    (is "F x in _. ?l x  ?r x")
  proof eventually_elim
    case x: (elim x)
    then have "cmod ((x powr s0) * f (- ln x))  x powr s0 * (M * exp (a * (- ln x)))"
      by (intro norm_mult_ineq[THEN order_trans]) (auto intro!: x(2)[THEN order_trans])
    also have " = M * x powr (s0 - a)"
      by (simp add: exp_minus ln_inverse divide_simps powr_def mult_exp_exp algebra_simps)
    finally show ?case .
  qed
  then have "((λx. x powr s0 * f (- ln x))  0) (at_right 0)"
    by (rule Lim_null_comparison)
      (auto intro!: tendsto_eq_intros a < s0 eventually_at_rightI zero_less_one)
  moreover have "F x in at x. ln x  0" if "0 < x" "x < 1" for x::real
    using order_tendstoD(1)[OF tendsto_ident_at 0 < x, of UNIV]
      order_tendstoD(2)[OF tendsto_ident_at x < 1, of UNIV]
    by eventually_elim simp
  ultimately have [continuous_intros]:
    "continuous_on {0..1} (λx. x powr s0 * f (- ln x))"
    by (intro continuous_on_IccI;
        force intro!: continuous_on_tendsto_compose[OF cont_f] tendsto_eq_intros eventually_at_leftI
        zero_less_one)
  {
    fix n::nat
    let ?i = "(λu. u ^ n *R (u powr s0 * f (- ln u)))"
    let ?I = "λn b. integral {exp (- b).. 1} ?i"
    have "F (b::real) in at_top. b > 0"
      by (simp add: eventually_gt_at_top)
    then have "F b in at_top. I (s0 + Suc n) b = ?I n b"
    proof eventually_elim
      case (elim b)
      have eq: "exp (t *R - complex_of_real (s0 + real (Suc n))) * f t =
        complex_of_real (exp (- (real n * t)) * exp (- t) * exp (- (s0 * t))) * f t"
        for t
        by (auto simp: Euler mult_exp_exp algebra_simps simp del: of_real_mult)
      from int[of "s0 + Suc n" b]
      have int': "((λt. exp (- (n * t)) * exp (-t) * exp (- (s0 * t)) * f t)
          has_integral I (s0 + Suc n) b) {0..b}"
        (is "(?fe has_integral _) _")
        unfolding eq .
      have "((λx. - exp (- x) *R exp (- x) ^ n *R (exp (- x) powr s0 * f (- ln (exp (- x)))))
          has_integral
            integral {exp (- 0)..exp (- b)} ?i - integral {exp (- b)..exp (- 0)} ?i) {0..b}"
        by (rule has_integral_substitution_general[of "{}" 0 b "λt. exp(-t)" 0 1 ?i "λx. -exp(-x)"])
           (auto intro!: less_imp_le[OF b > 0] continuous_intros integrable_continuous_real
             derivative_eq_intros)
      then have "(?fe has_integral ?I n b) {0..b}"
        using b > 0
        by (auto simp: algebra_simps mult_exp_exp exp_of_nat_mult[symmetric] scaleR_conv_of_real
            exp_add powr_def of_real_exp has_integral_neg_iff)
      with int' show ?case
        by (rule has_integral_unique)
    qed
    moreover have "(I (s0 + Suc n)  0) at_top"
      by (rule imp) (use s0 > a in auto)
    ultimately have "(?I n  0) at_top"
      by (rule Lim_transform_eventually[rotated])
    then have 1: "((λx. integral {exp (ln x)..1} ?i)  0) (at_right 0)"
      unfolding at_top_mirror filtermap_ln_at_right[symmetric] filtermap_filtermap filterlim_filtermap
      by simp
    have "F x in at_right 0. x > 0"
      by (simp add: eventually_at_filter)
    then have "F x in at_right 0. integral {exp (ln x)..1} ?i = integral {x .. 1} ?i"
      by eventually_elim (auto simp:)
    from Lim_transform_eventually[OF 1 this]
    have "((λx. integral {x..1} ?i)  0) (at_right 0)"
      by simp
    moreover
    have "?i integrable_on {0..1}"
      by (force intro: continuous_intros integrable_continuous_real)
    from continuous_on_Icc_at_rightD[OF indefinite_integral_continuous_1'[OF this] zero_less_one]
    have "((λx. integral {x..1} ?i)  integral {0 .. 1} ?i) (at_right 0)"
      by simp
    ultimately have "integral {0 .. 1} ?i = 0"
      by (rule tendsto_unique[symmetric, rotated]) simp
    then have "(?i has_integral 0) {0 .. 1}"
      using integrable_integral ?i integrable_on {0..1}
      by (metis (full_types))
  } from lerch_lemma[OF _ this, of "exp (- t)"]
  show "f t = 0" using t  0
    by (auto intro!: continuous_intros)
qed

lemma exponential_order_eventually_eq: "exponential_order M a f"
  if "exponential_order M a g" "t. t  k  f t = g t"
proof -
  have "F t in at_top. f t = g t"
    using that
    unfolding eventually_at_top_linorder
    by blast
  with exponential_orderD(2)[OF that(1)]
  have "(F t in at_top. norm (f t)  M * exp (a * t))"
    by eventually_elim auto
  with exponential_orderD(1)[OF that(1)]
  show ?thesis
    by (rule exponential_orderI)
qed

lemma exponential_order_mono:
  assumes eo: "exponential_order M a f"
  assumes "a  b" "M  N"
  shows "exponential_order N b f"
proof (rule exponential_orderI)
  from exponential_orderD[OF eo] assms(3)
  show "0 < N" by simp
  have "F t in at_top. (t::real) > 0"
    by (simp add: eventually_gt_at_top)
  then have "F t in at_top. M * exp (a * t)  N * exp (b * t)"
    by eventually_elim
      (use 0 < N in force intro: mult_mono assms›)
  with exponential_orderD(2)[OF eo]
  show "F t in at_top. norm (f t)  N * exp (b * t)"
    by (eventually_elim) simp
qed

lemma exponential_order_uminus_iff:
  "exponential_order M a (λx. - f x) = exponential_order M a f"
  by (auto simp: exponential_order_def)

lemma exponential_order_add:
  assumes "exponential_order M a f" "exponential_order M a g"
  shows "exponential_order (2 * M) a (λx. f x + g x)"
  using assms
  apply (auto simp: exponential_order_def)
  subgoal premises prems
    using prems(1,3)
    apply (eventually_elim)
    apply (rule norm_triangle_le)
    by linarith
  done

theorem laplace_transform_unique:
  assumes f: "s. Re s > a  (f has_laplace F) s"
  assumes g: "s. Re s > b  (g has_laplace F) s"
  assumes [continuous_intros]: "continuous_on {0..} f"
  assumes [continuous_intros]: "continuous_on {0..} g"
  assumes eof: "exponential_order M a f"
  assumes eog: "exponential_order N b g"
  assumes "t  0"
  shows "f t = g t"
proof -
  define c where "c = max a b"
  define L where "L = max M N"
  from eof have eof: "exponential_order L c f"
    by (rule exponential_order_mono) (auto simp: L_def c_def)
  from eog have eog: "exponential_order L c (λx. - g x)"
    unfolding exponential_order_uminus_iff
    by (rule exponential_order_mono) (auto simp: L_def c_def)
  from exponential_order_add[OF eof eog]
  have eom: "exponential_order (2 * L) c (λx. f x - g x)"
    by simp
  have l0: "((λx. f x - g x) has_laplace 0) s" if "Re s > c" for s
    using has_laplace_minus[OF f g, of s] that by (simp add: c_def max_def split: if_splits)
  have "f t - g t = 0"
    by (rule laplace_transform_zero[OF _ eom l0 t  0])
      (auto intro!: continuous_intros)
  then show ?thesis by simp
qed

end

Theory Laplace_Transform

theory Laplace_Transform
  imports
    "Existence"
    "Uniqueness"
begin

end