# 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.
›

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. x∈s ⟹ norm (f k x) ≤ h x" "∀x∈s. ((λ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: "∀b≥k. 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 x∈X 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 "∀x∈S. 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 ∧
(∀i∈I. (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

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

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)"
"x≥a ⟹ 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)"
"x≥i ⟹ 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. ∑i≤gn. ga i * x ^ i)" by metis
then have "?P n x = (∑i≤gn. 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)

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`