theory Laplace_Transform_Library imports "HOL-Analysis.Analysis" begin section ‹References› text ‹ Much of this formalization is based on Schiff's textbook \<^cite>‹"Schiff2013"›. Parts of this formalization are inspired by the HOL-Light formalization (\<^cite>‹"Taqdees2013"›, \<^cite>‹"Rashid2017"›, \<^cite>‹"Rashid2018"›), but stated more generally for piecewise continuous (instead of piecewise continuously differentiable) functions. › section ‹Library Additions› subsection ‹Derivatives› lemma DERIV_compose_FDERIV:―‹TODO: generalize and move from HOL-ODE› assumes "DERIV f (g x) :> f'" assumes "(g has_derivative g') (at x within s)" shows "((λx. f (g x)) has_derivative (λx. g' x * f')) (at x within s)" using assms has_derivative_compose[of g g' x s f "(*) f'"] by (auto simp: has_field_derivative_def ac_simps) lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV] and has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV] and has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV] subsection ‹Integrals› lemma negligible_real_ivlI: fixes a b::real assumes "a ≥ b" shows "negligible {a .. b}" proof - from assms have "{a .. b} = {a} ∨ {a .. b} = {}" by auto then show ?thesis by auto qed lemma absolutely_integrable_on_combine: fixes f :: "real ⇒ 'a::euclidean_space" assumes "f absolutely_integrable_on {a..c}" and "f absolutely_integrable_on {c..b}" and "a ≤ c" and "c ≤ b" shows "f absolutely_integrable_on {a..b}" using assms unfolding absolutely_integrable_on_def integrable_on_def by (auto intro!: has_integral_combine) lemma dominated_convergence_at_top: fixes f :: "real ⇒ 'n::euclidean_space ⇒ 'm::euclidean_space" assumes f: "⋀k. (f k) integrable_on s" and h: "h integrable_on s" and le: "⋀k x. x ∈ s ⟹ norm (f k x) ≤ h x" and conv: "∀x ∈ s. ((λk. f k x) ⤏ g x) at_top" shows "g integrable_on s" "((λk. integral s (f k)) ⤏ integral s g) at_top" proof - have 3: "set_integrable lebesgue s h" unfolding absolutely_integrable_on_def proof show "(λx. norm (h x)) integrable_on s" proof (intro integrable_spike_finite[OF _ _ h, where S="{}"] ballI) fix x assume "x ∈ s - {}" then show "norm (h x) = h x" using order_trans[OF norm_ge_zero le[of x]] by auto qed auto qed fact have 2: "set_borel_measurable lebesgue s (f k)" for k using f[of k] using has_integral_implies_lebesgue_measurable[of "f k"] by (auto intro: simp: integrable_on_def set_borel_measurable_def) have conv': "∀x ∈ s. ((λk. f k x) ⤏ g x) sequentially" using conv filterlim_filtermap filterlim_compose filterlim_real_sequentially by blast from 2 have 1: "set_borel_measurable lebesgue s g" unfolding set_borel_measurable_def by (rule borel_measurable_LIMSEQ_metric) (use conv' in ‹auto split: split_indicator›) have 4: "AE x in lebesgue. ((λi. indicator s x *⇩_{R}f i x) ⤏ indicator s x *⇩_{R}g x) at_top" "∀⇩_{F}i in at_top. AE x in lebesgue. norm (indicator s x *⇩_{R}f i x) ≤ indicator s x *⇩_{R}h x" using conv le by (auto intro!: always_eventually split: split_indicator) note 1 2 3 4 note * = this[unfolded set_borel_measurable_def set_integrable_def] have g: "g absolutely_integrable_on s" unfolding set_integrable_def by (rule integrable_dominated_convergence_at_top[OF *]) then show "g integrable_on s" by (auto simp: absolutely_integrable_on_def) have "((λk. (LINT x:s|lebesgue. f k x)) ⤏ (LINT x:s|lebesgue. g x)) at_top" unfolding set_lebesgue_integral_def using * by (rule integral_dominated_convergence_at_top) then show "((λk. integral s (f k)) ⤏ integral s g) at_top" using g absolutely_integrable_integrable_bound[OF le f h] by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto qed lemma has_integral_dominated_convergence_at_top: fixes f :: "real ⇒ 'n::euclidean_space ⇒ 'm::euclidean_space" assumes "⋀k. (f k has_integral y k) s" "h integrable_on s" "⋀k x. 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