Theory Laplace_Transform_Library

theory Laplace_Transform_Library

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

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

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

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

  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
  have "(λx. norm (f x)) integrable_on {a..}"
    using assms by (simp add: absolutely_integrable_on_def)
  note _
  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)
  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 .

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)

  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
      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
      show ?thesis
        by (intro exI[where x="I c"]) auto

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

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)