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:
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)
lemma exponential_order_add:
assumes "exponential_order M a f" "exponential_order M a g"
shows "exponential_order (2 * M) a (λx. f x + g x)"
using assms
apply (auto simp: exponential_order_def)
subgoal premises prems
using prems(1,3)
apply (eventually_elim)
apply (rule norm_triangle_le)
by linarith
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