Theory Uniqueness

section ‹Uniqueness of Laplace Transform›
theory Uniqueness

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)
  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 .
  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
    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)))))
            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
      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)
    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
    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)

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)

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

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

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