Theory Laplace_Transform_Library
theory Laplace_Transform_Library
imports
"HOL-Analysis.Analysis"
begin
section ‹References›
text ‹
Much of this formalization is based on Schiff's textbook \<^cite>‹"Schiff2013"›.
Parts of this formalization are inspired by the HOL-Light formalization
(\<^cite>‹"Taqdees2013"›, \<^cite>‹"Rashid2017"›, \<^cite>‹"Rashid2018"›), but stated more generally for
piecewise continuous (instead of piecewise continuously differentiable) functions.
›
section ‹Library Additions›
subsection ‹Derivatives›
lemma DERIV_compose_FDERIV:
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"
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