Theory Interval_Integral
theory Interval_Integral
imports Equivalence_Lebesgue_Henstock_Integration
begin
definition "einterval a b = {x. a < ereal x ∧ ereal x < b}"
lemma einterval_eq[simp]:
shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
and einterval_eq_Ici: "einterval (ereal a) ∞ = {a <..}"
and einterval_eq_Iic: "einterval (- ∞) (ereal b) = {..< b}"
and einterval_eq_UNIV: "einterval (- ∞) ∞ = UNIV"
by (auto simp: einterval_def)
lemma einterval_same: "einterval a a = {}"
by (auto simp: einterval_def)
lemma einterval_iff: "x ∈ einterval a b ⟷ a < ereal x ∧ ereal x < b"
by (simp add: einterval_def)
lemma einterval_nonempty: "a < b ⟹ ∃c. c ∈ einterval a b"
by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex)
lemma open_einterval[simp]: "open (einterval a b)"
by (cases a b rule: ereal2_cases)
(auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)
lemma borel_einterval[measurable]: "einterval a b ∈ sets borel"
unfolding einterval_def by measurable
subsection ‹Approximating a (possibly infinite) interval›
lemma filterlim_sup1: "(LIM x F. f x :> G1) ⟹ (LIM x F. f x :> (sup G1 G2))"
unfolding filterlim_def by (auto intro: le_supI1)
lemma ereal_incseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat ⇒ real" where "incseq X" "⋀i. a < X i" "⋀i. X i < b" "X ⇢ b"
proof (cases b)
case PInf
with ‹a < b› have "a = -∞ ∨ (∃r. a = ereal r)"
by (cases a) auto
moreover have "(λx. ereal (real (Suc x))) ⇢ ∞"
by (simp add: Lim_PInfty filterlim_sequentially_Suc) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
moreover have "⋀r. (λx. ereal (r + real (Suc x))) ⇢ ∞"
by (simp add: filterlim_sequentially_Suc Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
ultimately show thesis
by (intro that[of "λi. real_of_ereal a + Suc i"])
(auto simp: incseq_def PInf)
next
case (real b')
define d where "d = b' - (if a = -∞ then b' - 1 else real_of_ereal a)"
with ‹a < b› have a': "0 < d"
by (cases a) (auto simp: real)
moreover
have "⋀i r. r < b' ⟹ (b' - r) * 1 < (b' - r) * real (Suc (Suc i))"
by (intro mult_strict_left_mono) auto
with ‹a < b› a' have "⋀i. a < ereal (b' - d / real (Suc (Suc i)))"
by (cases a) (auto simp: real d_def field_simps)
moreover
have "(λi. b' - d / real i) ⇢ b'"
by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
then have "(λi. b' - d / Suc (Suc i)) ⇢ b'"
by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
ultimately show thesis
by (intro that[of "λi. b' - d / Suc (Suc i)"])
(auto simp: real incseq_def intro!: divide_left_mono)
qed (use ‹a < b› in auto)
lemma ereal_decseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat ⇒ real" where
"decseq X" "⋀i. a < X i" "⋀i. X i < b" "X ⇢ a"
proof -
have "-b < -a" using ‹a < b› by simp
from ereal_incseq_approx[OF this] obtain X where
"incseq X"
"⋀i. - b < ereal (X i)"
"⋀i. ereal (X i) < - a"
"(λx. ereal (X x)) ⇢ - a"
by auto
then show thesis
apply (intro that[of "λi. - X i"])
apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
done
qed
proposition einterval_Icc_approximation:
fixes a b :: ereal
assumes "a < b"
obtains u l :: "nat ⇒ real" where
"einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
proof -
from dense[OF ‹a < b›] obtain c where "a < c" "c < b" by safe
from ereal_incseq_approx[OF ‹c < b›] obtain u where u:
"incseq u"
"⋀i. c < ereal (u i)"
"⋀i. ereal (u i) < b"
"(λx. ereal (u x)) ⇢ b"
by auto
from ereal_decseq_approx[OF ‹a < c›] obtain l where l:
"decseq l"
"⋀i. a < ereal (l i)"
"⋀i. ereal (l i) < c"
"(λx. ereal (l x)) ⇢ a"
by auto
have "einterval a b = (⋃i. {l i .. u i})"
proof (auto simp: einterval_iff)
fix x assume "a < ereal x" "ereal x < b"
have "eventually (λi. ereal (l i) < ereal x) sequentially"
using l(4) ‹a < ereal x› by (rule order_tendstoD)
moreover
have "eventually (λi. ereal x < ereal (u i)) sequentially"
using u(4) ‹ereal x< b› by (rule order_tendstoD)
ultimately have "eventually (λi. l i < x ∧ x < u i) sequentially"
by eventually_elim auto
then show "∃i. l i ≤ x ∧ x ≤ u i"
by (auto intro: less_imp_le simp: eventually_sequentially)
next
fix x i assume "l i ≤ x" "x ≤ u i"
with ‹a < ereal (l i)› ‹ereal (u i) < b›
show "a < ereal x" "ereal x < b"
by (auto simp flip: ereal_less_eq(3))
qed
moreover { fix i from less_trans[OF ‹l i < c› ‹c < u i›] have "l i < u i" by simp }
ultimately show thesis
by (simp add: l that u)
qed
definition interval_lebesgue_integral :: "real measure ⇒ ereal ⇒ ereal ⇒ (real ⇒ 'a) ⇒ 'a::{banach, second_countable_topology}" where
"interval_lebesgue_integral M a b f =
(if a ≤ b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
syntax
"_ascii_interval_lebesgue_integral" :: "pttrn ⇒ real ⇒ real ⇒ real measure ⇒ real ⇒ real"
(‹(‹indent=5 notation=‹binder LINT››LINT _=_.._|_. _)› [0,60,60,61,100] 60)
syntax_consts
"_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
translations
"LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (λx. f)"
definition interval_lebesgue_integrable :: "real measure ⇒ ereal ⇒ ereal ⇒ (real ⇒ 'a::{banach, second_countable_topology}) ⇒ bool" where
"interval_lebesgue_integrable M a b f =
(if a ≤ b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
syntax
"_ascii_interval_lebesgue_borel_integral" :: "pttrn ⇒ real ⇒ real ⇒ real ⇒ real"
(‹(‹indent=4 notation=‹binder LBINT››LBINT _=_.._. _)› [0,60,60,61] 60)
syntax_consts
"_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (λx. f)"
subsection‹Basic properties of integration over an interval›
lemma interval_lebesgue_integral_cong:
"a ≤ b ⟹ (⋀x. x ∈ einterval a b ⟹ f x = g x) ⟹ einterval a b ∈ sets M ⟹
interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_cong_AE:
"f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹
a ≤ b ⟹ AE x ∈ einterval a b in M. f x = g x ⟹ einterval a b ∈ sets M ⟹
interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)
lemma interval_integrable_mirror:
shows "interval_lebesgue_integrable lborel a b (λx. f (-x)) ⟷
interval_lebesgue_integrable lborel (-b) (-a) f"
proof -
have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)"
for a b :: ereal and x :: real
by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator)
show ?thesis
unfolding interval_lebesgue_integrable_def
using lborel_integrable_real_affine_iff[symmetric, of "-1" "λx. indicator (einterval _ _) x *⇩R f x" 0]
by (simp add: * set_integrable_def)
qed
lemma interval_lebesgue_integral_add [intro, simp]:
fixes M a b f
assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
shows "interval_lebesgue_integrable M a b (λx. f x + g x)"
and "interval_lebesgue_integral M a b (λx. f x + g x) =
interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)
lemma interval_lebesgue_integral_diff [intro, simp]:
fixes M a b f
assumes "interval_lebesgue_integrable M a b f"
"interval_lebesgue_integrable M a b g"
shows "interval_lebesgue_integrable M a b (λx. f x - g x)" and
"interval_lebesgue_integral M a b (λx. f x - g x) =
interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)
lemma interval_lebesgue_integrable_mult_right [intro, simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, second_countable_topology}"
shows "(c ≠ 0 ⟹ interval_lebesgue_integrable M a b f) ⟹
interval_lebesgue_integrable M a b (λx. c * f x)"
by (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integrable_mult_left [intro, simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, second_countable_topology}"
shows "(c ≠ 0 ⟹ interval_lebesgue_integrable M a b f) ⟹
interval_lebesgue_integrable M a b (λx. f x * c)"
by (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integrable_divide [intro, simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "(c ≠ 0 ⟹ interval_lebesgue_integrable M a b f) ⟹
interval_lebesgue_integrable M a b (λx. f x / c)"
by (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integral_mult_right [simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (λx. c * f x) =
c * interval_lebesgue_integral M a b f"
by (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_mult_left [simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (λx. f x * c) =
interval_lebesgue_integral M a b f * c"
by (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_divide [simp]:
fixes M a b c and f :: "real ⇒ 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (λx. f x / c) =
interval_lebesgue_integral M a b f / c"
by (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_uminus:
"interval_lebesgue_integral M a b (λx. - f x) = - interval_lebesgue_integral M a b f"
by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
lemma interval_lebesgue_integral_of_real:
"interval_lebesgue_integral M a b (λx. complex_of_real (f x)) =
of_real (interval_lebesgue_integral M a b f)"
unfolding interval_lebesgue_integral_def
by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
lemma interval_lebesgue_integral_le_eq:
fixes a b f
assumes "a ≤ b"
shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
using assms by (auto simp: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_gt_eq:
fixes a b f
assumes "a > b"
shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
lemma interval_lebesgue_integral_gt_eq':
fixes a b f
assumes "a > b"
shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
lemma interval_integrable_endpoints_reverse:
"interval_lebesgue_integrable lborel a b f ⟷
interval_lebesgue_integrable lborel b a f"
by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
lemma interval_integral_reflect:
"(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
split: if_split_asm)
next
case (le a b)
have "(LBINT x:{x. - x ∈ einterval a b}. f (- x)) = (LBINT x:einterval (- b) (- a). f (- x))"
unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
then show ?case
unfolding interval_lebesgue_integral_def
by (subst set_integral_reflect) (simp add: le)
qed
lemma interval_lebesgue_integral_0_infty:
"interval_lebesgue_integrable M 0 ∞ f ⟷ set_integrable M {0<..} f"
"interval_lebesgue_integral M 0 ∞ f = (LINT x:{0<..}|M. f x)"
unfolding zero_ereal_def
by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)
lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..∞ | M. f x) = (LINT x : {a<..} | M. f x)"
unfolding interval_lebesgue_integral_def by auto
proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a ∞ f) =
(set_integrable M {a<..} f)"
unfolding interval_lebesgue_integrable_def by auto
subsection‹Basic properties of integration over an interval wrt lebesgue measure›
lemma interval_integral_zero [simp]:
fixes a b :: ereal
shows "(LBINT x=a..b. 0) = 0"
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
by simp
lemma interval_integral_const [intro, simp]:
fixes a b c :: real
shows "interval_lebesgue_integrable lborel a b (λx. c)" and "(LBINT x=a..b. c) = c * (b - a)"
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
lemma interval_integral_cong_AE:
assumes [measurable]: "f ∈ borel_measurable borel" "g ∈ borel_measurable borel"
assumes "AE x ∈ einterval (min a b) (max a b) in lborel. f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
by (auto simp: interval_lebesgue_integral_def max_def min_def intro!: set_lebesgue_integral_cong_AE)
lemma interval_integral_cong:
assumes "⋀x. x ∈ einterval (min a b) (max a b) ⟹ f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_cong)
lemma interval_lebesgue_integrable_cong_AE:
"f ∈ borel_measurable lborel ⟹ g ∈ borel_measurable lborel ⟹
AE x ∈ einterval (min a b) (max a b) in lborel. f x = g x ⟹
interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
apply (simp add: interval_lebesgue_integrable_def)
apply (intro conjI impI set_integrable_cong_AE)
apply (auto simp: min_def max_def)
done
lemma interval_integrable_abs_iff:
fixes f :: "real ⇒ real"
shows "f ∈ borel_measurable lborel ⟹
interval_lebesgue_integrable lborel a b (λx. ¦f x¦) = interval_lebesgue_integrable lborel a b f"
unfolding interval_lebesgue_integrable_def
by (simp add: set_integrable_abs_iff')
lemma interval_integral_Icc:
fixes a b :: real
shows "a ≤ b ⟹ (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)"
by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
simp add: interval_lebesgue_integral_def)
lemma interval_integral_Icc':
"a ≤ b ⟹ (LBINT x=a..b. f x) = (LBINT x : {x. a ≤ ereal x ∧ ereal x ≤ b}. f x)"
by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
simp add: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_Ioc:
"a ≤ b ⟹ (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)"
by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
simp add: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_Ioc':
"a ≤ b ⟹ (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x ∧ ereal x ≤ b}. f x)"
by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
simp add: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_Ico:
"a ≤ b ⟹ (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)"
by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
simp add: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_Ioi:
"¦a¦ < ∞ ⟹ (LBINT x=a..∞. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
by (auto simp: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_Ioo:
"a ≤ b ⟹ ¦a¦ < ∞ ==> ¦b¦ < ∞ ⟹ (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
by (auto simp: interval_lebesgue_integral_def einterval_iff)
lemma interval_integral_discrete_difference:
fixes f :: "real ⇒ 'b::{banach, second_countable_topology}" and a b :: ereal
assumes "countable X"
and eq: "⋀x. a ≤ b ⟹ a < x ⟹ x < b ⟹ x ∉ X ⟹ f x = g x"
and anti_eq: "⋀x. b ≤ a ⟹ b < x ⟹ x < a ⟹ x ∉ X ⟹ f x = g x"
assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0" "⋀x. x ∈ X ⟹ {x} ∈ sets M"
shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
apply (intro if_cong refl arg_cong[where f="λx. - x"] integral_discrete_difference[of X] assms)
apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
done
lemma interval_integral_sum:
fixes a b c :: ereal
assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
proof -
let ?I = "λa b. LBINT x=a..b. f x"
{ fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a ≤ b" "b ≤ c"
then have ord: "a ≤ b" "b ≤ c" "a ≤ c" and f': "set_integrable lborel (einterval a c) f"
by (auto simp: interval_lebesgue_integrable_def)
then have f: "set_borel_measurable borel (einterval a c) f"
unfolding set_integrable_def set_borel_measurable_def
by (drule_tac borel_measurable_integrable) simp
have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b ∪ einterval b c. f x)"
proof (rule set_integral_cong_set)
show "AE x in lborel. (x ∈ einterval a b ∪ einterval b c) = (x ∈ einterval a c)"
using AE_lborel_singleton[of "real_of_ereal b"] ord
by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b ∪ einterval b c) f"
unfolding set_borel_measurable_def
using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def])
qed
also have "… = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
using ord
by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
finally have "?I a b + ?I b c = ?I a c"
using ord by (simp add: interval_lebesgue_integral_def)
} note 1 = this
{ fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a ≤ b" "b ≤ c"
from 1[OF this] have "?I b c + ?I a b = ?I a c"
by (metis add.commute)
} note 2 = this
have 3: "⋀a b. b ≤ a ⟹ (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)"
by (rule interval_integral_endpoints_reverse)
show ?thesis
using integrable
apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
apply simp_all
by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed
lemma interval_integrable_isCont:
fixes a b and f :: "real ⇒ 'a::{banach, second_countable_topology}"
shows "(⋀x. min a b ≤ x ⟹ x ≤ max a b ⟹ isCont f x) ⟹
interval_lebesgue_integrable lborel a b f"
proof (induct a b rule: linorder_wlog)
case (le a b) then show ?case
unfolding interval_lebesgue_integrable_def set_integrable_def
by (auto simp: interval_lebesgue_integrable_def
intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
continuous_at_imp_continuous_on)
qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
lemma interval_integrable_continuous_on:
fixes a b :: real and f
assumes "a ≤ b" and "continuous_on {a..b} f"
shows "interval_lebesgue_integrable lborel a b f"
using assms unfolding interval_lebesgue_integrable_def apply simp
by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)
lemma interval_integral_eq_integral:
fixes f :: "real ⇒ 'a::euclidean_space"
shows "a ≤ b ⟹ set_integrable lborel {a..b} f ⟹ LBINT x=a..b. f x = integral {a..b} f"
by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)
lemma interval_integral_eq_integral':
fixes f :: "real ⇒ 'a::euclidean_space"
shows "a ≤ b ⟹ set_integrable lborel (einterval a b) f ⟹ LBINT x=a..b. f x = integral (einterval a b) f"
by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
subsection‹General limit approximation arguments›
proposition interval_integral_Icc_approx_nonneg:
fixes a b :: ereal
assumes "a < b"
fixes u l :: "nat ⇒ real"
assumes approx: "einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
fixes f :: "real ⇒ real"
assumes f_integrable: "⋀i. set_integrable lborel {l i..u i} f"
assumes f_nonneg: "AE x in lborel. a < ereal x ⟶ ereal x < b ⟶ 0 ≤ f x"
assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
assumes lbint_lim: "(λi. LBINT x=l i.. u i. f x) ⇢ C"
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
proof -
have 1 [unfolded set_integrable_def]: "⋀i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
have 2: "AE x in lborel. mono (λn. indicator {l n..u n} x *⇩R f x)"
proof -
from f_nonneg have "AE x in lborel. ∀i. l i ≤ x ⟶ x ≤ u i ⟶ 0 ≤ f x"
by eventually_elim
(metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans)
then show ?thesis
apply eventually_elim
apply (auto simp: mono_def split: split_indicator)
apply (metis approx(3) decseqD order_trans)
apply (metis approx(2) incseqD order_trans)
done
qed
have 3: "AE x in lborel. (λi. indicator {l i..u i} x *⇩R f x) ⇢ indicator (einterval a b) x *⇩R f x"
proof -
{ fix x i assume "l i ≤ x" "x ≤ u i"
then have "eventually (λi. l i ≤ x ∧ x ≤ u i) sequentially"
apply (auto simp: eventually_sequentially intro!: exI[of _ i])
apply (metis approx(3) decseqD order_trans)
apply (metis approx(2) incseqD order_trans)
done
then have "eventually (λi. f x * indicator {l i..u i} x = f x) sequentially"
by eventually_elim auto }
then show ?thesis
unfolding approx(1) by (auto intro!: AE_I2 tendsto_eventually split: split_indicator)
qed
have 4: "(λi. ∫ x. indicator {l i..u i} x *⇩R f x ∂lborel) ⇢ C"
using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
have 5: "(λx. indicat_real (einterval a b) x *⇩R f x) ∈ borel_measurable lborel"
using f_measurable set_borel_measurable_def by blast
have "(LBINT x=a..b. f x) = lebesgue_integral lborel (λx. indicator (einterval a b) x *⇩R f x)"
using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
also have "… = C"
by (rule integral_monotone_convergence [OF 1 2 3 4 5])
finally show "(LBINT x=a..b. f x) = C" .
show "set_integrable lborel (einterval a b) f"
unfolding set_integrable_def
by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed
proposition interval_integral_Icc_approx_integrable:
fixes u l :: "nat ⇒ real" and a b :: ereal
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}"
assumes "a < b"
assumes approx: "einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
shows "(λi. LBINT x=l i.. u i. f x) ⇢ (LBINT x=a..b. f x)"
proof -
have "(λi. LBINT x:{l i.. u i}. f x) ⇢ (LBINT x:einterval a b. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
show "integrable lborel (λx. norm (indicator (einterval a b) x *⇩R f x))"
using f_integrable integrable_norm set_integrable_def by blast
show "(λx. indicat_real (einterval a b) x *⇩R f x) ∈ borel_measurable lborel"
using f_integrable by (simp add: set_integrable_def)
then show "⋀i. (λx. indicat_real {l i..u i} x *⇩R f x) ∈ borel_measurable lborel"
by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx)
show "⋀i. AE x in lborel. norm (indicator {l i..u i} x *⇩R f x) ≤ norm (indicator (einterval a b) x *⇩R f x)"
by (intro AE_I2) (auto simp: approx split: split_indicator)
show "AE x in lborel. (λi. indicator {l i..u i} x *⇩R f x) ⇢ indicator (einterval a b) x *⇩R f x"
proof (intro AE_I2 tendsto_intros tendsto_eventually)
fix x
{ fix i assume "l i ≤ x" "x ≤ u i"
with ‹incseq u›[THEN incseqD, of i] ‹decseq l›[THEN decseqD, of i]
have "eventually (λi. l i ≤ x ∧ x ≤ u i) sequentially"
by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
then show "eventually (λxa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
using approx order_tendstoD(2)[OF ‹l ⇢ a›, of x] order_tendstoD(1)[OF ‹u ⇢ b›, of x]
by (auto split: split_indicator)
qed
qed
with ‹a < b› ‹⋀i. l i < u i› show ?thesis
by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
qed
subsection‹A slightly stronger Fundamental Theorem of Calculus›
text‹Three versions: first, for finite intervals, and then two versions for
arbitrary intervals.›
lemma interval_integral_FTC_finite:
fixes f F :: "real ⇒ 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
assumes F: "⋀x. min a b ≤ x ⟹ x ≤ max a b ⟹ (F has_vector_derivative (f x)) (at x within
{min a b..max a b})"
shows "(LBINT x=a..b. f x) = F b - F a"
proof (cases "a ≤ b")
case True
have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *⇩R f x)"
by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
also have "… = F b - F a"
proof (rule integral_FTC_atLeastAtMost [OF True])
show "continuous_on {a..b} f"
using True f by linarith
show "⋀x. ⟦a ≤ x; x ≤ b⟧ ⟹ (F has_vector_derivative f x) (at x within {a..b})"
by (metis F True max.commute max_absorb1 min_def)
qed
finally show ?thesis .
next
case False
then have "b ≤ a"
by simp
have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *⇩R f x)"
by (simp add: ‹b ≤ a› interval_integral_Icc set_lebesgue_integral_def)
also have "… = F b - F a"
proof (subst integral_FTC_atLeastAtMost [OF ‹b ≤ a›])
show "continuous_on {b..a} f"
using False f by linarith
show "⋀x. ⟦b ≤ x; x ≤ a⟧
⟹ (F has_vector_derivative f x) (at x within {b..a})"
by (metis F False max_def min_def)
qed auto
finally show ?thesis
by (metis interval_integral_endpoints_reverse)
qed
lemma interval_integral_FTC_nonneg:
fixes f F :: "real ⇒ real" and a b :: ereal
assumes "a < b"
assumes F: "⋀x. a < ereal x ⟹ ereal x < b ⟹ DERIV F x :> f x"
assumes f: "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont f x"
assumes f_nonneg: "AE x in lborel. a < ereal x ⟶ ereal x < b ⟶ 0 ≤ f x"
assumes A: "((F ∘ real_of_ereal) ⤏ A) (at_right a)"
assumes B: "((F ∘ real_of_ereal) ⤏ B) (at_left b)"
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = B - A"
proof -
obtain u l where approx:
"einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
by (blast intro: einterval_Icc_approximation[OF ‹a < b›])
have aless[simp]: "⋀x i. l i ≤ x ⟹ a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have lessb[simp]: "⋀x i. x ≤ u i ⟹ ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
have cf: "⋀i. continuous_on {min (l i) (u i)..max (l i) (u i)} f"
using approx f by (intro continuous_at_imp_continuous_on strip) auto
have FTCi: "⋀i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
apply (intro interval_integral_FTC_finite cf DERIV_subset [OF F])
by (smt (verit) F aless approx(4) has_real_derivative_iff_has_vector_derivative has_vector_derivative_at_within lessb)
have 1: "⋀i. set_integrable lborel {l i..u i} f"
by (meson aless lessb assms(3) atLeastAtMost_iff borel_integrable_atLeastAtMost' continuous_at_imp_continuous_on)
have 2: "set_borel_measurable lborel (einterval a b) f"
unfolding set_borel_measurable_def
by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
simp: continuous_on_eq_continuous_at einterval_iff f)
have "(λx. F (l x)) ⇢ A"
using A approx unfolding tendsto_at_iff_sequentially comp_def
by (force elim!: allE[of _ "λi. ereal (l i)"])
moreover have "(λx. F (u x)) ⇢ B"
using B approx unfolding tendsto_at_iff_sequentially comp_def
by (force elim!: allE[of _ "λi. ereal (u i)"])
ultimately have 3: "(λi. LBINT x=l i..u i. f x) ⇢ B - A"
by (simp add: FTCi tendsto_diff)
show "(LBINT x=a..b. f x) = B - A"
by (rule interval_integral_Icc_approx_nonneg [OF ‹a < b› approx 1 f_nonneg 2 3])
show "set_integrable lborel (einterval a b) f"
by (rule interval_integral_Icc_approx_nonneg [OF ‹a < b› approx 1 f_nonneg 2 3])
qed
theorem interval_integral_FTC_integrable:
fixes f F :: "real ⇒ 'a::euclidean_space" and a b :: ereal
assumes "a < b"
assumes F: "⋀x. a < ereal x ⟹ ereal x < b ⟹ (F has_vector_derivative f x) (at x)"
assumes f: "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont f x"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
assumes A: "((F ∘ real_of_ereal) ⤏ A) (at_right a)"
assumes B: "((F ∘ real_of_ereal) ⤏ B) (at_left b)"
shows "(LBINT x=a..b. f x) = B - A"
proof -
obtain u l where approx:
"einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
by (blast intro: einterval_Icc_approximation[OF ‹a < b›])
have [simp]: "⋀x i. l i ≤ x ⟹ a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have [simp]: "⋀x i. x ≤ u i ⟹ ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
have FTCi: "⋀i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
using assms approx
by (auto simp: less_imp_le min_def max_def
intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
intro: has_vector_derivative_at_within)
have "(λi. LBINT x=l i..u i. f x) ⇢ B - A"
unfolding FTCi
proof (intro tendsto_intros)
show "(λx. F (l x)) ⇢ A"
using A approx unfolding tendsto_at_iff_sequentially comp_def
by (elim allE[of _ "λi. ereal (l i)"], auto)
show "(λx. F (u x)) ⇢ B"
using B approx unfolding tendsto_at_iff_sequentially comp_def
by (elim allE[of _ "λi. ereal (u i)"], auto)
qed
moreover have "(λi. LBINT x=l i..u i. f x) ⇢ (LBINT x=a..b. f x)"
by (rule interval_integral_Icc_approx_integrable [OF ‹a < b› approx f_integrable])
ultimately show ?thesis
by (elim LIMSEQ_unique)
qed
theorem interval_integral_FTC2:
fixes a b c :: real and f :: "real ⇒ 'a::euclidean_space"
assumes "a ≤ c" "c ≤ b"
and contf: "continuous_on {a..b} f"
fixes x :: real
assumes "a ≤ x" and "x ≤ b"
shows "((λu. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
proof -
let ?F = "(λu. LBINT y=a..u. f y)"
have intf: "set_integrable lborel {a..b} f"
by (rule borel_integrable_atLeastAtMost', rule contf)
have "((λu. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
using ‹a ≤ x› ‹x ≤ b›
by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf])
then have "((λu. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
by simp
then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
by (rule has_vector_derivative_weaken)
(auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf])
then have "((λx. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})"
by (auto intro!: derivative_eq_intros)
then show ?thesis
proof (rule has_vector_derivative_weaken)
fix u assume "u ∈ {a .. b}"
then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
using assms
apply (intro interval_integral_sum)
apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
qed (insert assms, auto)
qed
proposition einterval_antiderivative:
fixes a b :: ereal and f :: "real ⇒ 'a::euclidean_space"
assumes "a < b" and contf: "⋀x :: real. a < x ⟹ x < b ⟹ isCont f x"
shows "∃F. ∀x :: real. a < x ⟶ x < b ⟶ (F has_vector_derivative f x) (at x)"
proof -
from einterval_nonempty [OF ‹a < b›] obtain c :: real where [simp]: "a < c" "c < b"
by (auto simp: einterval_def)
let ?F = "(λu. LBINT y=c..u. f y)"
show ?thesis
proof (rule exI, clarsimp)
fix x :: real
assume [simp]: "a < x" "x < b"
have 1: "a < min c x" by simp
from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
by (auto simp: einterval_def)
have 2: "max c x < b" by simp
from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
by (auto simp: einterval_def)
have "(?F has_vector_derivative f x) (at x within {d<..<e})"
proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
have "continuous_on {d..e} f"
proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
show "⋀x. ⟦d ≤ x; x ≤ e⟧ ⟹ a < ereal x"
using ‹a < ereal d› ereal_less_ereal_Ex by auto
show "⋀x. ⟦d ≤ x; x ≤ e⟧ ⟹ ereal x < b"
using ‹ereal e < b› ereal_less_eq(3) le_less_trans by blast
qed
then show "(?F has_vector_derivative f x) (at x within {d..e})"
by (intro interval_integral_FTC2) (use ‹d < c› ‹c < e› ‹d < x› ‹x < e› in ‹linarith+›)
qed auto
then show "(?F has_vector_derivative f x) (at x)"
by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
qed
qed
subsection‹The substitution theorem›
text‹Once again, three versions: first, for finite intervals, and then two versions for
arbitrary intervals.›
theorem interval_integral_substitution_finite:
fixes a b :: real and f :: "real ⇒ 'a::euclidean_space"
assumes "a ≤ b"
and derivg: "⋀x. a ≤ x ⟹ x ≤ b ⟹ (g has_real_derivative (g' x)) (at x within {a..b})"
and contf : "continuous_on (g ` {a..b}) f"
and contg': "continuous_on {a..b} g'"
shows "(LBINT x=a..b. g' x *⇩R f (g x)) = (LBINT y=g a..g b. f y)"
proof-
have v_derivg: "⋀x. a ≤ x ⟹ x ≤ b ⟹ (g has_vector_derivative (g' x)) (at x within {a..b})"
using derivg unfolding has_real_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
by (rule continuous_on_vector_derivative) auto
have 1: "∃x∈{a..b}. u = g x" if "min (g a) (g b) ≤ u" "u ≤ max (g a) (g b)" for u
by (cases "g a ≤ g b") (use that assms IVT' [of g a u b] IVT2' [of g b u a] in ‹auto simp: min_def max_def›)
obtain c d where g_im: "g ` {a..b} = {c..d}" and "c ≤ d"
by (metis continuous_image_closed_interval contg ‹a ≤ b›)
obtain F where derivF:
"⋀x. ⟦a ≤ x; x ≤ b⟧ ⟹ (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
using continuous_on_subset [OF contf] g_im
by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
have contfg: "continuous_on {a..b} (λx. f (g x))"
by (blast intro: continuous_on_compose2 contf contg)
have "continuous_on {a..b} (λx. g' x *⇩R f (g x))"
by (auto intro!: continuous_on_scaleR contg' contfg)
then have "(LBINT x. indicat_real {a..b} x *⇩R g' x *⇩R f (g x)) = F (g b) - F (g a)"
using integral_FTC_atLeastAtMost [OF ‹a ≤ b› vector_diff_chain_within[OF v_derivg derivF]]
by force
then have "LBINT x=a..b. g' x *⇩R f (g x) = F (g b) - F (g a)"
by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
proof (rule interval_integral_FTC_finite)
show "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1)
show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})"
if y: "min (g a) (g b) ≤ y" "y ≤ max (g a) (g b)" for y
proof -
obtain x where "a ≤ x" "x ≤ b" "y = g x"
using 1 y by force
then show ?thesis
by (auto simp: image_def intro!: 1 has_vector_derivative_within_subset [OF derivF])
qed
qed
ultimately show ?thesis by simp
qed
theorem interval_integral_substitution_integrable:
fixes f :: "real ⇒ 'a::euclidean_space" and a b u v :: ereal
assumes "a < b"
and deriv_g: "⋀x. a < ereal x ⟹ ereal x < b ⟹ DERIV g x :> g' x"
and contf: "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont f (g x)"
and contg': "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont g' x"
and g'_nonneg: "⋀x. a ≤ ereal x ⟹ ereal x ≤ b ⟹ 0 ≤ g' x"
and A: "((ereal ∘ g ∘ real_of_ereal) ⤏ A) (at_right a)"
and B: "((ereal ∘ g ∘ real_of_ereal) ⤏ B) (at_left b)"
and integrable: "set_integrable lborel (einterval a b) (λx. g' x *⇩R f (g x))"
and integrable2: "set_integrable lborel (einterval A B) (λx. f x)"
shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *⇩R f (g x))"
proof -
obtain u l where approx [simp]:
"einterval a b = (⋃i. {l i .. u i})"
"incseq u" "decseq l" "⋀i. l i < u i" "⋀i. a < l i" "⋀i. u i < b"
"l ⇢ a" "u ⇢ b"
by (blast intro: einterval_Icc_approximation[OF ‹a < b›])
note less_imp_le [simp]
have [simp]: "⋀x i. l i ≤ x ⟹ a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have [simp]: "⋀x i. x ≤ u i ⟹ ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
then have lessb[simp]: "⋀i. l i < b"
using approx(4) less_eq_real_def by blast
have [simp]: "⋀i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
have lle[simp]: "⋀i j. i ≤ j ⟹ l j ≤ l i" by (rule decseqD, rule approx)
have [simp]: "⋀i j. i ≤ j ⟹ u i ≤ u j" by (rule incseqD, rule approx)
have g_nondec [simp]: "g x ≤ g y" if "a < x" "x ≤ y" "y < b" for x y
proof (rule DERIV_nonneg_imp_nondecreasing [OF ‹x ≤ y›], intro exI conjI)
show "⋀u. x ≤ u ⟹ u ≤ y ⟹ (g has_real_derivative g' u) (at u)"
by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
show "⋀u. x ≤ u ⟹ u ≤ y ⟹ 0 ≤ g' u"
by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
qed
have "A ≤ B" and un: "einterval A B = (⋃i. {g(l i)<..<g(u i)})"
proof -
have A2: "(λi. g (l i)) ⇢ A"
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "λi. ereal (l i)" in spec, auto)
hence A3: "⋀i. g (l i) ≥ A"
by (intro decseq_ge, auto simp: decseq_def)
have B2: "(λi. g (u i)) ⇢ B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "λi. ereal (u i)" in spec, auto)
hence B3: "⋀i. g (u i) ≤ B"
by (intro incseq_le, auto simp: incseq_def)
have "ereal (g (l 0)) ≤ ereal (g (u 0))"
by auto
then show "A ≤ B"
by (meson A3 B3 order.trans)
{ fix x :: real
assume "A < x" and "x < B"
then have "eventually (λi. ereal (g (l i)) < x ∧ x < ereal (g (u i))) sequentially"
by (fast intro: eventually_conj order_tendstoD A2 B2)
hence "∃i. g (l i) < x ∧ x < g (u i)"
by (simp add: eventually_sequentially, auto)
} note AB = this
show "einterval A B = (⋃i. {g(l i)<..<g(u i)})"
proof
show "einterval A B ⊆ (⋃i. {g(l i)<..<g(u i)})"
by (auto simp: einterval_def AB)
show "(⋃i. {g(l i)<..<g(u i)}) ⊆ einterval A B"
proof (clarsimp simp add: einterval_def, intro conjI)
show "⋀x i. ⟦g (l i) < x; x < g (u i)⟧ ⟹ A < ereal x"
using A3 le_ereal_less by blast
show "⋀x i. ⟦g (l i) < x; x < g (u i)⟧ ⟹ ereal x < B"
using B3 ereal_le_less by blast
qed
qed
qed
have eq1: "(LBINT x=l i.. u i. g' x *⇩R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
apply (auto intro!: continuous_at_imp_continuous_on contf contg')
done
have "(λi. LBINT x=l i..u i. g' x *⇩R f (g x)) ⇢ (LBINT x=a..b. g' x *⇩R f (g x))"
using approx(4) ‹a < b› integrable interval_integral_Icc_approx_integrable by fastforce
hence 2: "(λi. (LBINT y=g (l i)..g (u i). f y)) ⇢ (LBINT x=a..b. g' x *⇩R f (g x))"
by (simp add: eq1)
have incseq: "incseq (λi. {g (l i)<..<g (u i)})"
apply (clarsimp simp: incseq_def, intro conjI)
using lessb lle approx(5) g_nondec le_less_trans apply blast
by (force intro: less_le_trans)
have "(λi. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
⇢ set_lebesgue_integral lborel (einterval A B) f"
unfolding un by (rule set_integral_cont_up) (use incseq integrable2 un in auto)
then have "(λi. (LBINT y=g (l i)..g (u i). f y)) ⇢ (LBINT x = A..B. f x)"
by (simp add: interval_lebesgue_integral_le_eq ‹A ≤ B›)
thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
qed
theorem interval_integral_substitution_nonneg:
fixes f g g':: "real ⇒ real" and a b u v :: ereal
assumes "a < b"
and deriv_g: "⋀x. a < ereal x ⟹ ereal x < b ⟹ DERIV g x :> g' x"
and contf: "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont f (g x)"
and contg': "⋀x. a < ereal x ⟹ ereal x < b ⟹ isCont g' x"
and f_nonneg: "⋀x. a < ereal x ⟹ ereal x < b ⟹ 0 ≤ f (g x)"
and g'_nonneg: "⋀x. a ≤ ereal x ⟹ ereal x ≤ b ⟹ 0 ≤ g' x"
and A: "((ereal ∘ g ∘ real_of_ereal) ⤏ A) (at_right a)"
and B: "((ereal ∘ g ∘ real_of_ereal) ⤏ B) (at_left b)"
and integrable_fg: "set_integrable lborel (einterval a b) (λx. f (g x) * g' x)"
shows
"set_integrable lborel (einterval A B) f"
"(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
proof -
from einterval_Icc_approximation[OF ‹a < b›] obtain u l where approx [simp]:
"einterval a b = (⋃i. {l i..u i})"
"incseq u"
"decseq l"
"⋀i. l i < u i"
"⋀i. a < ereal (l i)"
"⋀i. ereal (u i) < b"
"(λx. ereal (l x)) ⇢ a"
"(λx. ereal (u x)) ⇢ b" by this auto
have aless[simp]: "⋀x i. l i ≤ x ⟹ a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have lessb[simp]: "⋀x i. x ≤ u i ⟹ ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
have llb[simp]: "⋀i. l i < b"
using lessb approx(4) less_eq_real_def by blast
have alu[simp]: "⋀i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
have [simp]: "⋀i j. i ≤ j ⟹ l j ≤ l i" by (rule decseqD, rule approx)
have uleu[simp]: "⋀i j. i ≤ j ⟹ u i ≤ u j" by (rule incseqD, rule approx)
have g_nondec [simp]: "g x ≤ g y" if "a < x" "x ≤ y" "y < b" for x y
proof (rule DERIV_nonneg_imp_nondecreasing [OF ‹x ≤ y›], intro exI conjI)
show "⋀u. x ≤ u ⟹ u ≤ y ⟹ (g has_real_derivative g' u) (at u)"
by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
show "⋀u. x ≤ u ⟹ u ≤ y ⟹ 0 ≤ g' u"
by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
qed
have "A ≤ B" and un: "einterval A B = (⋃i. {g(l i)<..<g(u i)})"
proof -
have A2: "(λi. g (l i)) ⇢ A"
using A by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "λi. ereal (l i)"])
hence A3: "⋀i. g (l i) ≥ A"
by (intro decseq_ge, auto simp: decseq_def)
have B2: "(λi. g (u i)) ⇢ B"
using B by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "λi. ereal (u i)"])
hence B3: "⋀i. g (u i) ≤ B"
by (intro incseq_le, auto simp: incseq_def)
have "ereal (g (l 0)) ≤ ereal (g (u 0))"
by (auto simp: less_imp_le)
then show "A ≤ B"
by (meson A3 B3 order.trans)
{ fix x :: real
assume "A < x" and "x < B"
then have "eventually (λi. ereal (g (l i)) < x ∧ x < ereal (g (u i))) sequentially"
by (fast intro: eventually_conj order_tendstoD A2 B2)
hence "∃i. g (l i) < x ∧ x < g (u i)"
by (simp add: eventually_sequentially, auto)
} note AB = this
show "einterval A B = (⋃i. {g(l i)<..<g(u i)})"
proof
show "einterval A B ⊆ (⋃i. {g (l i)<..<g (u i)})"
by (auto simp: einterval_def AB)
show "(⋃i. {g (l i)<..<g (u i)}) ⊆ einterval A B"
using A3 B3 by (force simp: einterval_def intro: le_ereal_less ereal_le_less)
qed
qed
have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i
proof -
have "(LBINT x=l i.. u i. g' x *⇩R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
done
then show ?thesis
by (simp add: ac_simps)
qed
have incseq: "incseq (λi. {g (l i)<..<g (u i)})"
apply (clarsimp simp: incseq_def, intro conjI)
apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
using alu uleu approx(6) g_nondec less_le_trans by blast
have img: "∃c ≥ l i. c ≤ u i ∧ x = g c" if "g (l i) ≤ x" "x ≤ g (u i)" for x i
proof -
have "continuous_on {l i..u i} g"
by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
with that show ?thesis
using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
qed
have "continuous_on {g (l i)..g (u i)} f" for i
using contf img by (force simp add: intro!: continuous_at_imp_continuous_on)
then have int_f: "⋀i. set_integrable lborel {g (l i)<..<g (u i)} f"
by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
have integrable: "set_integrable lborel (⋃i. {g (l i)<..<g (u i)}) f"
proof (intro pos_integrable_to_top incseq int_f)
let ?l = "(LBINT x=a..b. f (g x) * g' x)"
have "(λi. LBINT x=l i..u i. f (g x) * g' x) ⇢ ?l"
by (intro assms interval_integral_Icc_approx_integrable [OF ‹a < b› approx])
hence "(λi. (LBINT y=g (l i)..g (u i). f y)) ⇢ ?l"
by (simp add: eq1)
then show "(λi. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) ⇢ ?l"
unfolding interval_lebesgue_integral_def by (auto simp: less_imp_le)
have "⋀x i. g (l i) ≤ x ⟹ x ≤ g (u i) ⟹ 0 ≤ f x"
using aless f_nonneg img lessb by blast
then show "⋀x i. x ∈ {g (l i)<..<g (u i)} ⟹ 0 ≤ f x"
using less_eq_real_def by auto
qed (auto simp: greaterThanLessThan_borel)
thus "set_integrable lborel (einterval A B) f"
by (simp add: un)
have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *⇩R f (g x))"
proof (rule interval_integral_substitution_integrable)
show "set_integrable lborel (einterval a b) (λx. g' x *⇩R f (g x))"
using integrable_fg by (simp add: ac_simps)
qed fact+
then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
by (simp add: ac_simps)
qed
syntax "_complex_lebesgue_borel_integral" :: "pttrn ⇒ real ⇒ complex"
(‹(‹indent=2 notation=‹binder CLBINT››CLBINT _. _)› [0,60] 60)
syntax_consts
"_complex_lebesgue_borel_integral" == complex_lebesgue_integral
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (λx. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn ⇒ real set ⇒ real ⇒ complex"
(‹(‹indent=3 notation=‹binder CLBINT››CLBINT _:_. _)› [0,60,61] 60)
syntax_consts
"_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
translations
"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (λx. f)"
abbreviation complex_interval_lebesgue_integral ::
"real measure ⇒ ereal ⇒ ereal ⇒ (real ⇒ complex) ⇒ complex" where
"complex_interval_lebesgue_integral M a b f ≡ interval_lebesgue_integral M a b f"
abbreviation complex_interval_lebesgue_integrable ::
"real measure ⇒ ereal ⇒ ereal ⇒ (real ⇒ complex) ⇒ bool" where
"complex_interval_lebesgue_integrable M a b f ≡ interval_lebesgue_integrable M a b f"
syntax
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn ⇒ ereal ⇒ ereal ⇒ real ⇒ complex"
(‹(‹indent=4 notation=‹binder CLBINT››CLBINT _=_.._. _)› [0,60,60,61] 60)
syntax_consts
"_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (λx. f)"
proposition interval_integral_norm:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}"
shows "interval_lebesgue_integrable lborel a b f ⟹ a ≤ b ⟹
norm (LBINT t=a..b. f t) ≤ LBINT t=a..b. norm (f t)"
using integral_norm_bound[of lborel "λx. indicator (einterval a b) x *⇩R f x"]
by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
proposition interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f ⟹
norm (LBINT t=a..b. f t) ≤ ¦LBINT t=a..b. norm (f t)¦"
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
next
case (le a b)
then have "¦LBINT t=a..b. norm (f t)¦ = LBINT t=a..b. norm (f t)"
using integrable_norm[of lborel "λx. indicator (einterval a b) x *⇩R f x"]
by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
intro!: integral_nonneg_AE abs_of_nonneg)
then show ?case
using le by (simp add: interval_integral_norm)
qed
lemma integral_cos: "t ≠ 0 ⟹ LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
apply (intro interval_integral_FTC_finite continuous_intros)
by (auto intro!: derivative_eq_intros simp: has_real_derivative_iff_has_vector_derivative[symmetric])
end