Theory Preliminaries_AC
theory Preliminaries_AC
imports "HOL-Library.Rewrite" "HOL-Probability.Probability"
begin
notation powr (infixr ‹.^› 80)
section ‹Preliminary Lemmas›
lemma vimage_compl_atMost:
fixes f :: "'a ⇒ 'b::linorder"
shows "-(f -` {..y}) = f -` {y<..}"
by fastforce
context linorder
begin
lemma Icc_minus_Ico:
fixes a b
assumes "a ≤ b"
shows "{a..b} - {a..<b} = {b}"
using assms by auto
lemma Icc_minus_Ioc:
fixes a b
assumes "a ≤ b"
shows "{a..b} - {a<..b} = {a}"
using assms by auto
lemma Int_atLeastAtMost_Unbounded[simp]: "{a..} Int {..b} = {a..b}"
by auto
lemma Int_greaterThanAtMost_Unbounded[simp]: "{a<..} Int {..b} = {a<..b}"
by auto
lemma Int_atLeastLessThan_Unbounded[simp]: "{a..} Int {..<b} = {a..<b}"
by auto
lemma Int_greaterThanLessThan_Unbounded[simp]: "{a<..} Int {..<b} = {a<..<b}"
by auto
end
lemma Ico_real_nat_disjoint:
"disjoint_family (λn::nat. {a + real n ..< a + real n + 1})" for a::real
unfolding disjoint_family_on_def by fastforce
corollary Ico_nat_disjoint: "disjoint_family (λn::nat. {real n ..< real n + 1})"
using Ico_real_nat_disjoint[of 0] by simp
lemma Ico_real_nat_union: "(⋃n::nat. {a + real n ..< a + real n + 1}) = {a..}" for a::real
proof
show "(⋃n::nat. {a + real n ..< a + real n + 1}) ⊆ {a..}" by auto
next
show "{a..} ⊆ (⋃n::nat. {a + real n ..< a + real n + 1})"
proof
fix x assume "x ∈ {a..}"
hence "a ≤ x" by simp
hence "nat ⌊x-a⌋ ≤ x-a ∧ x-a < nat ⌊x-a⌋ + 1" by linarith
hence "a + nat ⌊x-a⌋ ≤ x ∧ x < a + nat ⌊x-a⌋ + 1" by auto
thus "x ∈ (⋃n::nat. {a + real n ..< a + real n + 1})" by auto
qed
qed
corollary Ico_nat_union: "(⋃n::nat. {real n ..< real n + 1}) = {0..}"
using Ico_real_nat_union[of 0] by simp
lemma Ico_nat_union_finite: "(⋃(n::nat)<m. {real n ..< real n + 1}) = {0..<m}"
proof
show "(⋃(n::nat)<m. {real n ..< real n + 1}) ⊆ {0..<m}" by auto
next
show "{0..<m} ⊆ (⋃(n::nat)<m. {real n ..< real n + 1})"
proof
fix x::real
assume ⋆: "x ∈ {0..<m}"
hence "nat ⌊x⌋ < m" using of_nat_floor by fastforce
moreover with ⋆ have "nat ⌊x⌋ ≤ x ∧ x < nat ⌊x⌋ + 1"
by (metis Nat.add_0_right atLeastLessThan_iff le_nat_floor
less_one linorder_not_le nat_add_left_cancel_le of_nat_floor)
ultimately show "x ∈ (⋃(n::nat)<m. {real n ..< real n + 1})"
unfolding atLeastLessThan_def by force
qed
qed
lemma seq_part_multiple: fixes m n :: nat assumes "m ≠ 0" defines "A ≡ λi::nat. {i*m ..< (i+1)*m}"
shows "∀i j. i ≠ j ⟶ A i ∩ A j = {}" and "(⋃i<n. A i) = {..< n*m}"
proof -
{ fix i j :: nat
have "i ≠ j ⟹ A i ∩ A j = {}"
proof (erule contrapos_np)
assume "A i ∩ A j ≠ {}"
then obtain k where "k ∈ A i ∩ A j" by blast
hence "i*m < (j+1)*m ∧ j*m < (i+1)*m" unfolding A_def by force
hence "i < j+1 ∧ j < i+1" using mult_less_cancel2 by blast
thus "i = j" by force
qed }
thus "∀i j. i ≠ j ⟶ A i ∩ A j = {}" by blast
next
show "(⋃i<n. A i) = {..< n*m}"
proof
show "(⋃i<n. A i) ⊆ {..< n*m}"
proof
fix x::nat
assume "x ∈ (⋃i<n. A i)"
then obtain i where i_n: "i < n" and i_x: "x < (i+1)*m" unfolding A_def by force
hence "i+1 ≤ n" by linarith
hence "x < n*m" by (meson less_le_trans mult_le_cancel2 i_x)
thus "x ∈ {..< n*m}"
using diff_mult_distrib mult_1 i_n by auto
qed
next
show "{..< n*m} ⊆ (⋃i<n. A i)"
proof
fix x::nat
let ?i = "x div m"
assume "x ∈ {..< n*m}"
hence "?i < n" by (simp add: less_mult_imp_div_less)
moreover have "?i*m ≤ x ∧ x < (?i+1)*m"
using assms div_times_less_eq_dividend dividend_less_div_times by auto
ultimately show "x ∈ (⋃i<n. A i)" unfolding A_def by force
qed
qed
qed
lemma frontier_Icc_real: "frontier {a..b} = {a, b}" if "a ≤ b" for a b :: real
unfolding frontier_def using that by force
lemma(in field) divide_mult_cancel[simp]: fixes a b assumes "b ≠ 0"
shows "a / b * b = a"
by (simp add: assms)
lemma divide_powr: "(1/a).^b = a.^-b" for a b :: real
by (simp add: powr_divide powr_minus_divide)
lemma geometric_increasing_sum_aux: "(1-r)⇧2 * (∑k<n. (k+1)*r^k) = 1 - (n+1)*r^n + n*r^(n+1)"
for n::nat and r::real
proof (induct n)
case 0
thus ?case by simp
next
case (Suc n)
have "(1-r)⇧2 * (∑k < Suc n. (k+1)*r^k) = (1-r)⇧2 * (∑k<n. (k+1)*r^k) + (1-r)⇧2 * ((n+1)*r^n)"
using sum.lessThan_Suc by (simp add: field_simps)
also have "… = 1 - (n+1)*r^n + n*r^(n+1) + (1-r)⇧2 * ((n+1)*r^n)"
using Suc.hyps by simp
also have "… = 1 - (n+2)*r^(n+1) + (n+1)*r^(n+2)"
by (simp add: field_simps power2_eq_square)
finally show ?case by simp
qed
lemma geometric_increasing_sum: "(∑k<n. (k+1)*r^k) = (1 - (n+1)*r^n + n*r^(n+1)) / (1-r)^2"
if "r ≠ 1" for n::nat and r::real
by (rewrite geometric_increasing_sum_aux[THEN sym]) (simp add: that)
lemma LIM_zero_iff': "((λx. l - f x) ⤏ 0) F = (f ⤏ l) F"
for f :: "'a ⇒ 'b::real_normed_vector"
unfolding tendsto_iff dist_norm
by (rewrite minus_diff_eq[THEN sym], rewrite norm_minus_cancel) simp
lemma antimono_onI:
"(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r ≤ s ⟹ f r ≥ f s) ⟹ antimono_on A f"
by (rule monotone_onI)
lemma antimono_onD:
"⟦antimono_on A f; r ∈ A; s ∈ A; r ≤ s⟧ ⟹ f r ≥ f s"
by (rule monotone_onD)
lemma antimono_imp_mono_on: "antimono f ⟹ antimono_on A f"
by (simp add: antimonoD antimono_onI)
lemma antimono_on_subset: "antimono_on A f ⟹ B ⊆ A ⟹ antimono_on B f"
by (rule monotone_on_subset)
lemma mono_on_antimono_on:
fixes f :: "'a::order ⇒ 'b::ordered_ab_group_add"
shows "mono_on A f ⟷ antimono_on A (λr. - f r)"
by (simp add: monotone_on_def)
lemmas mono_antimono = mono_on_antimono_on[where A=UNIV]
lemma mono_on_at_top_le:
fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
and f :: "'a ⇒ 'b"
assumes f_mono: "mono_on {a..} f" and f_to_l: "(f ⤏ l) at_top"
shows "⋀x. x ∈ {a..} ⟹ f x ≤ l"
proof -
{ fix b assume b_a: "b ≥ a" and fb_l: "¬ f b ≤ l"
let ?eps = "f b - l"
have lim_top: "⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) at_top"
using assms tendsto_def by auto
have "eventually (λx. f x ∈ {l - ?eps <..< l + ?eps}) at_top"
using fb_l by (intro lim_top; force)
then obtain N where fn_in: "⋀n. n ≥ N ⟹ f n ∈ {l - ?eps <..< l + ?eps}"
using eventually_at_top_linorder by metis
let ?n = "max b N"
have "f ?n < f b" using fn_in by force
moreover have "f ?n ≥ f b" using f_mono b_a by (simp add: le_max_iff_disj mono_on_def)
ultimately have False by simp }
thus "⋀x. x ∈ {a..} ⟹ f x ≤ l"
by blast
qed
corollary mono_at_top_le:
fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder ⇒ 'b"
assumes "mono f" and "(f ⤏ b) at_top"
shows "f x ≤ b"
using mono_on_at_top_le assms by (metis atLeast_iff mono_imp_mono_on nle_le)
lemma mono_on_at_bot_ge:
fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
and f :: "'a ⇒ 'b"
assumes f_mono: "mono_on {..a} f" and f_to_l: "(f ⤏ l) at_bot"
shows "⋀x. x ∈ {..a} ⟹ f x ≥ l"
proof -
{ fix b assume b_a: "b ≤ a" and fb_l: "¬ f b ≥ l"
let ?eps = "l - f b"
have lim_bot: "⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) at_bot"
using assms tendsto_def by auto
have "eventually (λx. f x ∈ {l - ?eps <..< l + ?eps}) at_bot"
using fb_l by (intro lim_bot; force)
then obtain N where fn_in: "⋀n. n ≤ N ⟹ f n ∈ {l - ?eps <..< l + ?eps}"
using eventually_at_bot_linorder by metis
let ?n = "min b N"
have "f ?n > f b" using fn_in by force
moreover have "f ?n ≤ f b" using f_mono b_a by (simp add: min.coboundedI1 mono_onD)
ultimately have False by simp }
thus "⋀x. x ∈ {..a} ⟹ f x ≥ l"
by blast
qed
corollary mono_at_bot_ge:
fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder ⇒ 'b"
assumes "mono f" and "(f ⤏ b) at_bot"
shows "⋀x. f x ≥ b"
using mono_on_at_bot_ge assms by (metis atMost_iff mono_imp_mono_on nle_le)
lemma antimono_on_at_top_ge:
fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
and f :: "'a ⇒ 'b"
assumes f_antimono: "antimono_on {a..} f" and f_to_l: "(f ⤏ l) at_top"
shows "⋀x. x ∈ {a..} ⟹ f x ≥ l"
proof -
{ fix b assume b_a: "b ≥ a" and fb_l: "¬ f b ≥ l"
let ?eps = "l - f b"
have lim_top: "⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) at_top"
using assms tendsto_def by auto
have "eventually (λx. f x ∈ {l - ?eps <..< l + ?eps}) at_top"
using fb_l by (intro lim_top; force)
then obtain N where fn_in: "⋀n. n ≥ N ⟹ f n ∈ {l - ?eps <..< l + ?eps}"
using eventually_at_top_linorder by metis
let ?n = "max b N"
have "f ?n > f b" using fn_in by force
moreover have "f ?n ≤ f b" using f_antimono b_a
by (simp add: antimono_onD le_max_iff_disj)
ultimately have False by simp }
thus "⋀x. x ∈ {a..} ⟹ f x ≥ l"
by blast
qed
corollary antimono_at_top_le:
fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder ⇒ 'b"
assumes "antimono f" and "(f ⤏ b) at_top"
shows "⋀x. f x ≥ b"
using antimono_on_at_top_ge assms antimono_imp_mono_on by blast
lemma antimono_on_at_bot_ge:
fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
and f :: "'a ⇒ 'b"
assumes f_antimono: "antimono_on {..a} f" and f_to_l: "(f ⤏ l) at_bot"
shows "⋀x. x ∈ {..a} ⟹ f x ≤ l"
proof -
{ fix b assume b_a: "b ≤ a" and fb_l: "¬ f b ≤ l"
let ?eps = "f b - l"
have lim_bot: "⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) at_bot"
using assms tendsto_def by auto
have "eventually (λx. f x ∈ {l - ?eps <..< l + ?eps}) at_bot"
using fb_l by (intro lim_bot; force)
then obtain N where fn_in: "⋀n. n ≤ N ⟹ f n ∈ {l - ?eps <..< l + ?eps}"
using eventually_at_bot_linorder by metis
let ?n = "min b N"
have "f ?n < f b" using fn_in by force
moreover have "f ?n ≥ f b" using f_antimono b_a by (simp add: min.coboundedI1 antimono_onD)
ultimately have False by simp }
thus "⋀x. x ∈ {..a} ⟹ f x ≤ l"
using assms by blast
qed
corollary antimono_at_bot_ge:
fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder ⇒ 'b"
assumes "antimono f" and "(f ⤏ b) at_bot"
shows "⋀x. f x ≤ b"
using antimono_on_at_bot_ge assms antimono_imp_mono_on by blast
lemma indicator_Ici_right_continuous:
fixes a x :: real
shows "continuous (at_right x) (indicator {a..})"
proof (cases ‹a ≤ x›)
case True
hence "∀⇩F y in at_right x. indicator {a..} y = 1"
by (smt (verit, ccfv_threshold) Ioi_le_Ico eventually_at_right_less eventually_mono
greaterThan_iff indicator_eq_1_iff subset_iff)
with True show ?thesis
by (simp add: continuous_at_within_cong indicator_eq_1_iff)
next
case False
hence "∀⇩F y in at_right x. indicator {a..} y = 0"
by (metis (mono_tags, lifting) atLeast_iff eventually_at_right indicator_eq_0_iff not_le)
with False show ?thesis
by (simp add: continuous_at_within_cong indicator_eq_0_iff)
qed
lemma continuous_cdivide:
fixes c::"'a::real_normed_field"
assumes "c ≠ 0" "continuous F f"
shows "continuous F (λx. f x / c)"
using assms continuous_mult_right by (rewrite field_class.field_divide_inverse) auto
lemma continuous_mult_left_iff:
fixes c::"'a::real_normed_field"
assumes "c ≠ 0"
shows "continuous F f ⟷ continuous F (λx. c * f x)"
using assms continuous_cmult_left_iff by blast
lemma continuous_mult_right_iff:
fixes c::"'a::real_normed_field"
assumes "c ≠ 0"
shows "continuous F f ⟷ continuous F (λx. f x * c)"
using continuous_mult_right continuous_cdivide assms by force
lemma continuous_cdivide_iff:
fixes c::"'a::real_normed_field"
assumes "c ≠ 0"
shows "continuous F f ⟷ continuous F (λx. f x / c)"
proof
assume "continuous F f"
thus "continuous F (λx. f x / c)"
by (intro continuous_cdivide) (simp add: assms)
next
assume "continuous F (λx. f x / c)"
hence "continuous F (λx. f x / c * c)" using continuous_mult_right by fastforce
thus "continuous F f" using assms by force
qed
lemma continuous_within_shift:
fixes a x :: "'a :: {topological_ab_group_add, t2_space}"
and s :: "'a set"
and f :: "'a ⇒ 'b::topological_space"
shows "continuous (at x within s) (λx. f (x+a)) ⟷ continuous (at (x+a) within plus a ` s) f"
proof
assume "continuous (at x within s) (λx. f (x+a))"
moreover have "continuous (at (x+a) within plus a ` s) (plus (-a))"
by (simp add: continuous_at_imp_continuous_at_within)
moreover have "plus (-a) ` plus a ` s = s" by force
ultimately show "continuous (at (x+a) within plus a ` s) f"
using continuous_within_compose unfolding comp_def by force
next
assume "continuous (at (x+a) within plus a ` s) f"
moreover have "continuous (at x within s) (plus a)"
by (simp add: continuous_at_imp_continuous_at_within)
ultimately show "continuous (at x within s) (λx. f (x+a))"
using continuous_within_compose unfolding comp_def by (force simp add: add.commute)
qed
lemma isCont_shift:
fixes a x :: "'a :: {topological_ab_group_add, t2_space}"
and f :: "'a ⇒ 'b::topological_space"
shows "isCont (λx. f (x+a)) x ⟷ isCont f (x+a)"
using continuous_within_shift by force
lemma has_real_derivative_at_split:
"(f has_real_derivative D) (at x) ⟷
(f has_real_derivative D) (at_left x) ∧ (f has_real_derivative D) (at_right x)"
proof -
have "at x = at x within ({..<x} ∪ {x<..})" by (simp add: at_eq_sup_left_right at_within_union)
thus "(f has_real_derivative D) (at x) ⟷
(f has_real_derivative D) (at_left x) ∧ (f has_real_derivative D) (at_right x)"
using Lim_within_Un has_field_derivative_iff by fastforce
qed
lemma DERIV_cmult_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. c * f x) has_field_derivative c * D) (at x within s)"
proof
assume "(f has_field_derivative D) (at x within s)"
thus "((λx. c * f x) has_field_derivative c * D) (at x within s)" using DERIV_cmult by force
next
assume "((λx. c * f x) has_field_derivative c * D) (at x within s)"
hence "((λx. c * f x / c) has_field_derivative c * D / c) (at x within s)"
using DERIV_cdivide assms by blast
thus "(f has_field_derivative D) (at x within s)" by (simp add: assms field_simps)
qed
lemma DERIV_cmult_right_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. f x * c) has_field_derivative D * c) (at x within s)"
by (rewrite DERIV_cmult_iff[of c], simp_all add: assms mult_ac)
lemma DERIV_cdivide_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. f x / c) has_field_derivative D / c) (at x within s)"
by (simp add: DERIV_cmult_right_iff assms field_class.field_divide_inverse)
lemma DERIV_ln_divide_chain:
fixes f :: "real ⇒ real"
assumes "f x > 0" and "(f has_real_derivative D) (at x within s)"
shows "((λx. ln (f x)) has_real_derivative (D / f x)) (at x within s)"
proof -
have "DERIV ln (f x) :> 1 / f x" using assms by (intro DERIV_ln_divide) blast
thus ?thesis using DERIV_chain2 assms by fastforce
qed
corollary field_differentiable_at_ln_comp:
fixes f :: "real ⇒ real"
assumes "f x > 0" and "f field_differentiable (at x within s)"
shows "(λx. ln (f x)) field_differentiable (at x within s)"
using DERIV_ln_divide_chain assms unfolding field_differentiable_def by force
lemma inverse_fun_has_integral_ln:
fixes f :: "real ⇒ real" and f' :: "real ⇒ real"
assumes "a ≤ b" and
"⋀x. x∈{a..b} ⟹ f x > 0" and
"continuous_on {a..b} f" and
"⋀x. x∈{a<..<b} ⟹ (f has_real_derivative f' x) (at x)"
shows "((λx. f' x / f x) has_integral (ln (f b) - ln (f a))) {a..b}"
proof -
have "continuous_on {a..b} (λx. ln (f x))" using assms by (intro continuous_intros; force)
moreover have "⋀x. x∈{a<..<b} ⟹ ((λx. ln (f x)) has_vector_derivative f' x / f x) (at x)"
apply (rewrite has_real_derivative_iff_has_vector_derivative[THEN sym])
using assms by (intro DERIV_ln_divide_chain; simp)
ultimately show ?thesis using assms by (intro fundamental_theorem_of_calculus_interior; simp)
qed
lemma powr_at_top_at_top:
fixes a::real
assumes "a > 1"
shows "filterlim (λx. a.^x) at_top at_top"
proof -
have [simp]: "ln a > 0" using assms by simp
have "a ≠ 0" using assms by simp
moreover have "filterlim (λx. exp (ln a * x)) at_top at_top"
using assms
by(auto intro!: filterlim_compose[OF exp_at_top] filterlim_cmult_at_bot_at_top[OF ln_at_top]
ln_at_top filterlim_cmult_at_bot_at_top[OF filterlim_ident])
ultimately show ?thesis unfolding powr_def by(simp add: mult.commute)
qed
lemma powr_at_top_at_bot:
fixes a::real
assumes "0 < a" "a < 1"
shows "filterlim (λx. a.^x) at_top at_bot"
proof -
have "filterlim (λx. (1/a).^x) at_top at_top"
by (rule powr_at_top_at_top) (simp add: assms)
thus ?thesis
by (metis (no_types, lifting) ext inverse_powr filterlim_at_top_mirror
inverse_eq_divide minus_minus powr_minus)
qed
lemma powr_0_at_bot:
fixes a::real
assumes "a > 1"
shows "((λx. a.^x) ⤏ 0) at_bot"
proof -
have "⋀x. inverse ((1/a).^x) = a.^x"
using assms inverse_powr by (simp add: inverse_eq_divide)
moreover have "((λx. inverse ((1/a).^x)) ⤏ 0) at_bot"
apply (intro tendsto_inverse_0_at_top powr_at_top_at_bot)
using assms by simp_all
ultimately show ?thesis by simp
qed
lemma powr_0_at_top:
fixes a::real
assumes "0 < a" "a < 1"
shows "((λx. a.^x) ⤏ 0) at_top"
proof -
have "⋀x. inverse ((1/a).^x) = a.^x"
using assms inverse_powr by (simp add: inverse_eq_divide)
moreover have "((λx. inverse ((1/a).^x)) ⤏ 0) at_top"
by (intro tendsto_inverse_0_at_top powr_at_top_at_top) (simp add: assms)
ultimately show ?thesis by simp
qed
lemma DERIV_fun_powr2:
fixes a::real
assumes a_pos: "a > 0"
and f: "DERIV f x :> r"
shows "DERIV (λx. a.^(f x)) x :> a.^(f x) * r * ln a"
proof -
let ?g = "(λx. a)"
have g: "DERIV ?g x :> 0" by simp
have pos: "?g x > 0" by (simp add: a_pos)
show ?thesis
using DERIV_powr[OF g pos f] a_pos by (auto simp add: field_simps)
qed
lemma has_real_derivative_powr2:
assumes a_pos: "a > 0"
shows "((λx. a.^x) has_real_derivative a.^x * ln a) (at x)"
proof -
let ?f = "(λx. x::real)"
have f: "DERIV ?f x :> 1" by simp
thus ?thesis using DERIV_fun_powr2[OF a_pos f] by simp
qed
corollary has_real_derivative_powr2_ln:
assumes "a > 0" "a ≠ 1"
shows "((λx. a.^x / ln a) has_real_derivative a.^x) (at x)"
using assms by (intro derivative_eq_intros) (simp add: field_simps)+
lemma field_differentiable_shift:
"(f field_differentiable (at (x + z))) = ((λx. f (x + z)) field_differentiable (at x))"
unfolding field_differentiable_def using DERIV_shift by force
subsection ‹Lemmas on ‹indicator› for an Ordered Type›
lemma mono_indicator_Ici: "mono (indicator {a::'a::order..} :: ('a ⇒ 'b::linordered_semidom))"
by (smt (verit) atLeast_iff dual_order.trans indicator_def monoI nle_le split_of_bool
zero_less_eq_of_bool)
lemma mono_indicator_Ico: "mono (indicator {a::'a::order <..} :: ('a ⇒ 'b::linordered_semidom))"
by (metis (mono_tags, lifting) indicator_leI mono_greaterThan mono_set monotone_on_def)
lemma indicator_Icc_shift:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a..b} x = indicator {t+a..t+b} (t+x)"
by (simp add: indicator_def)
lemma indicator_Icc_shift_inverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a-t..b-t} x = indicator {a..b} (t+x)"
by (metis add.commute diff_add_cancel indicator_Icc_shift)
lemma indicator_Ici_shift:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a..} x = indicator {t+a..} (t+x)"
by (simp add: indicator_def)
lemma indicator_Ici_shift_inverse:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a-t..} x = indicator {a..} (t+x)"
by (metis add.commute diff_add_cancel indicator_Ici_shift)
lemma indicator_Iic_shift:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b} x = indicator {..t+b} (t+x)"
by (simp add: indicator_def)
lemma indicator_Iic_shift_inverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b-t} x = indicator {..b} (t+x)"
by (metis add.commute diff_add_cancel indicator_Iic_shift)
lemma indicator_Icc_reverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a..b} x = indicator {t-b..t-a} (t-x)"
by (metis add_le_cancel_left atLeastAtMost_iff diff_add_cancel indicator_simps le_diff_eq)
lemma indicator_Icc_reverse_inverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {t-b..t-a} x = indicator {a..b} (t-x)"
by (metis add_diff_cancel_left' diff_add_cancel indicator_Icc_reverse)
lemma indicator_Ici_reverse:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a..} x = indicator {..t-a} (t-x)"
by (simp add: indicator_def)
lemma indicator_Ici_reverse_inverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {t-b..} x = indicator {..b} (t-x)"
by (metis add_diff_cancel_left' diff_add_cancel indicator_Ici_reverse)
lemma indicator_Iic_reverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b} x = indicator {t-b..} (t-x)"
by (simp add: indicator_def)
lemma indicator_Iic_reverse_inverse:
fixes a t x :: "'a::linordered_field"
shows "indicator {..t-a} x = indicator {a..} (t-x)"
by (simp add: indicator_def)
lemma indicator_Icc_affine_pos:
fixes a b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {a..b} x = indicator {t+c*a..t+c*b} (t + c*x)"
unfolding indicator_def using assms by simp
lemma indicator_Icc_affine_pos_inverse:
fixes a b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {(a-t)/c..(b-t)/c} x = indicator {a..b} (t + c*x)"
using indicator_Icc_affine_pos[where a="(a-t)/c" and b="(b-t)/c" and c=c and t=t ] assms by simp
lemma indicator_Ici_affine_pos:
fixes a c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {a..} x = indicator {t+c*a..} (t + c*x)"
unfolding indicator_def using assms by simp
lemma indicator_Ici_affine_pos_inverse:
fixes a c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {(a-t)/c..} x = indicator {a..} (t + c*x)"
using indicator_Ici_affine_pos[where a="(a-t)/c" and c=c and t=t] assms by simp
lemma indicator_Iic_affine_pos:
fixes b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {..b} x = indicator {..t+c*b} (t + c*x)"
unfolding indicator_def using assms by simp
lemma indicator_Iic_affine_pos_inverse:
fixes b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {..(b-t)/c} x = indicator {..b} (t + c*x)"
using indicator_Iic_affine_pos[where b="(b-t)/c" and c=c and t=t] assms by simp
lemma indicator_Icc_affine_neg:
fixes a b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {a..b} x = indicator {t+c*b..t+c*a} (t + c*x)"
unfolding indicator_def using assms by auto
lemma indicator_Icc_affine_neg_inverse:
fixes a b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {(b-t)/c..(a-t)/c} x = indicator {a..b} (t + c*x)"
using indicator_Icc_affine_neg[where a="(b-t)/c" and b="(a-t)/c" and c=c and t=t] assms by simp
lemma indicator_Ici_affine_neg:
fixes a c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {a..} x = indicator {..t+c*a} (t + c*x)"
unfolding indicator_def using assms by simp
lemma indicator_Ici_affine_neg_inverse:
fixes b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {(b-t)/c..} x = indicator {..b} (t + c*x)"
using indicator_Ici_affine_neg[where a="(b-t)/c" and c=c and t=t] assms by simp
lemma indicator_Iic_affine_neg:
fixes b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {..b} x = indicator {t+c*b..} (t + c*x)"
unfolding indicator_def using assms by simp
lemma indicator_Iic_affine_neg_inverse:
fixes a c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {..(a-t)/c} x = indicator {a..} (t + c*x)"
using indicator_Iic_affine_neg[where b="(a-t)/c" and c=c and t=t] assms by simp
section ‹Additional Lemmas for the ‹HOL-Analysis› Library›
lemma differentiable_eq_field_differentiable_real:
fixes f :: "real ⇒ real"
shows "f differentiable F ⟷ f field_differentiable F"
unfolding field_differentiable_def differentiable_def has_real_derivative
using has_real_derivative_iff by presburger
lemma differentiable_on_eq_field_differentiable_real:
fixes f :: "real ⇒ real"
shows "f differentiable_on s ⟷ (∀x∈s. f field_differentiable (at x within s))"
unfolding differentiable_on_def using differentiable_eq_field_differentiable_real by simp
lemma differentiable_on_cong :
assumes "⋀x. x∈s ⟹ f x = g x" and "f differentiable_on s"
shows "g differentiable_on s"
proof -
{ fix x assume "x∈s"
hence "f differentiable at x within s" using assms unfolding differentiable_on_def by simp
from this obtain D where "(f has_derivative D) (at x within s)"
unfolding differentiable_def by blast
hence "(g has_derivative D) (at x within s)"
using has_derivative_transform assms ‹x∈s› by metis
hence "g differentiable at x within s" unfolding differentiable_def by blast }
hence "∀x∈s. g differentiable at x within s" by simp
thus ?thesis unfolding differentiable_on_def by simp
qed
lemma C1_differentiable_imp_deriv_continuous_on:
"f C1_differentiable_on S ⟹ continuous_on S (deriv f)"
using C1_differentiable_on_eq field_derivative_eq_vector_derivative by auto
lemma deriv_shift:
assumes "f field_differentiable at (x+a)"
shows "deriv f (x+a) = deriv (λs. f (x+s)) a"
proof -
have "(f has_field_derivative deriv f (x+a)) (at (x+a))"
using DERIV_deriv_iff_field_differentiable assms
by force
hence "((λs. f (x+s)) has_field_derivative deriv f (x+a)) (at a)"
using DERIV_at_within_shift has_field_derivative_at_within by blast
moreover have "((λs. f (x+s)) has_field_derivative deriv (λs. f (x+s)) a) (at a)"
using DERIV_imp_deriv calculation by fastforce
ultimately show ?thesis using DERIV_unique by force
qed
lemma piecewise_differentiable_on_cong:
assumes "f piecewise_differentiable_on i"
and "⋀x. x ∈ i ⟹ f x = g x"
shows "g piecewise_differentiable_on i"
proof -
have "continuous_on i g"
using continuous_on_cong_simp assms piecewise_differentiable_on_imp_continuous_on by force
moreover have "∃S. finite S ∧ (∀x ∈ i - S. g differentiable (at x within i))"
proof -
from assms piecewise_differentiable_on_def
obtain S where fin: "finite S" and "∀x ∈ i - S. f differentiable (at x within i)" by metis
hence "⋀x. x ∈ i - S ⟹ f differentiable (at x within i)" by simp
hence "⋀x. x ∈ i - S ⟹ g differentiable (at x within i)"
using has_derivative_transform assms by (metis DiffD1 differentiable_def)
with fin show ?thesis by blast
qed
ultimately show ?thesis unfolding piecewise_differentiable_on_def by simp
qed
lemma differentiable_piecewise:
assumes "continuous_on i f"
and "f differentiable_on i"
shows "f piecewise_differentiable_on i"
unfolding piecewise_differentiable_on_def using assms differentiable_onD by auto
lemma piecewise_differentiable_scaleR:
assumes "f piecewise_differentiable_on S"
shows "(λx. a *⇩R f x) piecewise_differentiable_on S"
proof -
from assms obtain T where fin: "finite T" "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
hence "⋀x. x ∈ S - T ⟹ (λx. a *⇩R f x) differentiable at x within S"
using differentiable_scaleR by simp
moreover have "continuous_on S (λx. a *⇩R f x)"
using assms continuous_on_scaleR continuous_on_const piecewise_differentiable_on_def by blast
ultimately show "(λx. a *⇩R f x) piecewise_differentiable_on S"
using fin piecewise_differentiable_on_def by blast
qed
lemma differentiable_on_piecewise_compose:
assumes "f piecewise_differentiable_on S"
and "g differentiable_on f ` S"
shows "g ∘ f piecewise_differentiable_on S"
proof -
from assms obtain T where fin: "finite T" "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
hence "⋀x. x ∈ S - T ⟹ g ∘ f differentiable at x within S"
by (meson DiffD1 assms differentiable_chain_within differentiable_onD image_eqI)
hence "∃T. finite T ∧ (∀x∈S-T. g ∘ f differentiable at x within S)" using fin by blast
moreover have "continuous_on S (g ∘ f)"
using assms continuous_on_compose differentiable_imp_continuous_on
unfolding piecewise_differentiable_on_def by blast
ultimately show ?thesis
unfolding piecewise_differentiable_on_def by force
qed
lemma MVT_order_free:
fixes r h :: real
defines "I ≡ {r..r+h} ∪ {r+h..r}"
assumes "continuous_on I f" and "f differentiable_on interior I"
obtains t where "t ∈ {0<..<1}" and "f (r+h) - f r = h * deriv f (r + t*h)"
proof -
consider (h_pos) "h > 0" | (h_0) "h = 0" | (h_neg) "h < 0" by force
thus ?thesis
proof cases
case h_pos
hence "r < r+h" "I = {r..r+h}" unfolding I_def by simp_all
moreover hence "interior I = {r<..<r+h}" by simp
moreover hence "⋀x. ⟦r < x; x < r+h⟧ ⟹ f differentiable (at x)"
using assms by (simp add: differentiable_on_eq_differentiable_at)
ultimately obtain z where "r < z ∧ z < r+h ∧ f (r+h) - f r = h * deriv f z"
using MVT assms by (smt (verit) DERIV_imp_deriv)
moreover hence "(z-r) / h ∈ {0<..<1}" by simp
moreover have "z = r + (z-r)/h * h" using h_pos by simp
ultimately show ?thesis using that by presburger
next
case h_0
have "1/2 ∈ {0::real<..<1}" by simp
moreover have "f (r+h) - f r = 0" using h_0 by simp
moreover have "h * deriv f (r + (1/2)*h) = 0" using h_0 by simp
ultimately show ?thesis using that by presburger
next case h_neg
hence "r+h < r" "I = {r+h..r}" unfolding I_def by simp_all
moreover hence "interior I = {r+h<..<r}" by simp
moreover hence "⋀x. ⟦r+h < x; x < r⟧ ⟹ f differentiable (at x)"
using assms by (simp add: differentiable_on_eq_differentiable_at)
ultimately obtain z where "r+h < z ∧ z < r ∧ f r - f (r+h) = -h * deriv f z"
using MVT assms by (smt (verit) DERIV_imp_deriv)
moreover hence "(z-r) / h ∈ {0<..<1}" by (simp add: neg_less_divide_eq)
moreover have "z = r + (z-r)/h * h" using h_neg by simp
ultimately show ?thesis using that mult_minus_left by fastforce
qed
qed
lemma integral_combine2:
fixes f :: "real ⇒ 'a::banach"
assumes "a ≤ c" "c ≤ b"
and "f integrable_on {a..c}" "f integrable_on {c..b}"
shows "integral {a..c} f + integral {c..b} f = integral {a..b} f"
by (meson Henstock_Kurzweil_Integration.integrable_combine
Henstock_Kurzweil_Integration.integral_combine assms)
lemma has_integral_null_interval: fixes a b :: real and f::"real ⇒ real" assumes "a ≥ b"
shows "(f has_integral 0) {a..b}"
using assms content_real_eq_0 by blast
lemma has_integral_interval_reverse: fixes f :: "real ⇒ real" and a b :: real
assumes "a ≤ b"
and "continuous_on {a..b} f"
shows "((λx. f (a+b-x)) has_integral (integral {a..b} f)) {a..b}"
proof -
let ?g = "λx. a + b - x"
let ?g' = "λx. -1"
have "continuous_on {a..b} ?g" using continuous_on_op_minus by simp
moreover have "⋀x. x∈{a..b} ⟹ (?g has_field_derivative ?g' x) (at x within {a..b})"
by (auto intro!: derivative_eq_intros)
ultimately have "((λx. -1 * f (a+b-x)) has_integral integral {b..a} f - integral {a..b} f) {a..b}"
using has_integral_substitution_general[of "{}" a b ?g a b f] assms by force
thus ?thesis
by (simp add: has_integral_null_interval[OF ‹a ≤ b›, THEN integral_unique] has_integral_neg_iff)
qed
lemma FTC_real_deriv_has_integral:
fixes F :: "real ⇒ real"
assumes "a ≤ b"
and "F piecewise_differentiable_on {a<..<b}"
and "continuous_on {a..b} F"
shows "(deriv F has_integral F b - F a) {a..b}"
proof -
obtain S where fin: "finite S" and
diff: "⋀x. x ∈ {a<..<b} - S ⟹ F differentiable at x within {a<..<b} - S"
using assms unfolding piecewise_differentiable_on_def
by (meson Diff_subset differentiable_within_subset)
hence "⋀x. x ∈ {a<..<b} - S ⟹ (F has_real_derivative deriv F x) (at x)"
proof -
fix x assume x_in: "x ∈ {a<..<b} - S"
have "open ({a<..<b} - S)"
using fin finite_imp_closed by (metis open_Diff open_greaterThanLessThan)
hence "at x within {a<..<b} - S = at x" by (meson x_in at_within_open)
hence "F differentiable at x" using diff x_in by (smt (verit))
thus "(F has_real_derivative deriv F x) (at x)"
using DERIV_deriv_iff_real_differentiable by simp
qed
thus ?thesis
by (intro fundamental_theorem_of_calculus_interior_strong[OF countable_finite, where S=S];
simp add: assms fin has_real_derivative_iff_has_vector_derivative)
qed
lemma integrable_spike_cong:
assumes "negligible S" "⋀x. x ∈ T - S ⟹ g x = f x"
shows "f integrable_on T ⟷ g integrable_on T"
using integrable_spike assms by force
lemma has_integral_powr2_from_0:
fixes a c :: real
assumes a_pos: "a > 0" and a_neq_1: "a ≠ 1" and c_nneg: "c ≥ 0"
shows "((λx. a.^x) has_integral ((a.^c - 1) / (ln a))) {0..c}"
proof -
have "((λx. a.^x) has_integral ((a.^c)/(ln a) - (a.^0)/(ln a))) {0..c}"
apply (rule fundamental_theorem_of_calculus[OF c_nneg])
apply (rule has_vector_derivative_within_subset[where S=UNIV and T="{0..c}"])
using has_real_derivative_iff_has_vector_derivative has_real_derivative_powr2_ln assms by simp+
thus ?thesis
using assms by (simp add: field_simps)
qed
lemma integrable_on_powr2_from_0:
fixes a c :: real
assumes a_pos: "a > 0" and a_neq_1: "a ≠ 1" and c_nneg: "c ≥ 0"
shows "(λx. a.^x) integrable_on {0..c}"
using has_integral_powr2_from_0[OF assms] unfolding integrable_on_def by blast
lemma integrable_on_powr2_from_0_general:
fixes a c :: real
assumes a_pos: "a > 0" and c_nneg: "c ≥ 0"
shows "(λx. a.^x) integrable_on {0..c}"
proof (cases "a = 1")
case True
thus ?thesis
using has_integral_const_real by auto
next
case False
thus ?thesis
using has_integral_powr2_from_0 False assms by auto
qed
lemma nn_integral_FTC_atMost:
fixes f :: "real ⇒ real"
assumes f_borel: "f ∈ borel_measurable borel"
assumes f: "⋀x. x ≤ b ⟹ DERIV F x :> f x"
assumes nonneg: "⋀x. x ≤ b ⟹ 0 ≤ f x"
assumes lim: "(F ⤏ U) at_bot"
shows "(∫⇧+x. ennreal (f x) * indicator {.. b} x ∂lborel) = F b - U"
proof -
let ?f = "λ(i::nat) (x::real). ennreal (f x) * indicator {b - real i .. b} x"
let ?fR = "λx. ennreal (f x) * indicator {.. b} x"
have F_mono: "y ≤ b ⟹ x ≤ y ⟹ F x ≤ F y" for x y
using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
then have F_ge_U: "x ≤ b ⟹ F x ≥ U" for x
by (intro tendsto_upperbound[OF lim])
(auto simp: eventually_at_bot_linorder)
have "(SUP i. ?f i x) = ?fR x" for x
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
obtain n where "b - x < real n"
using reals_Archimedean2[of "b - x"] ..
then have "eventually (λn. ?f n x = ?fR x) sequentially"
by (auto simp: frequently_def intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
then show "(λn. ?f n x) ⇢ ?fR x"
by (rule tendsto_eventually)
qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
then have "integral⇧N lborel ?fR = (∫⇧+ x. (SUP i. ?f i x) ∂lborel)"
by simp
also have "… = (SUP i. (∫⇧+ x. ?f i x ∂lborel))"
proof (rule nn_integral_monotone_convergence_SUP)
show "incseq ?f"
using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
show "⋀i. (?f i) ∈ borel_measurable lborel"
using f_borel by auto
qed
also have "… = (SUP i. ennreal (F b - F (b - real i)))"
by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
also have "… = F b - U"
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
have "LIM n sequentially. b - real n :> at_bot"
by real_asymp
then have "(λn. F (b - real n)) ⇢ U"
using filterlim_compose lim by force
then show "(λn. ennreal (F b - F (b - real n)) ) ⇢ ennreal (F b - U)"
by (simp add: F_mono F_ge_U tendsto_diff)
qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
finally show ?thesis .
qed
lemma has_bochner_integral_power:
fixes a b :: real and k :: nat
assumes "a ≤ b"
shows "has_bochner_integral lborel (λx. x^k * indicator {a..b} x) ((b^(k+1) - a^(k+1)) / (k+1))"
proof -
have "⋀x. ((λx. x^(k+1) / (k+1)) has_real_derivative x^k) (at x)"
using DERIV_pow by (intro derivative_eq_intros) auto
hence "has_bochner_integral lborel (λx. x^k * indicator {a..b} x) (b^(k+1)/(k+1) - a^(k+1)/(k+1))"
by (intro has_bochner_integral_FTC_Icc_real; simp add: assms)
thus ?thesis by (simp add: diff_divide_distrib)
qed
corollary integrable_power: "(a::real) ≤ b ⟹ integrable lborel (λx. x^k * indicator {a..b} x)"
using has_bochner_integral_power integrable.intros by blast
lemma nn_integral_powr_Icc:
fixes a b c :: real
assumes "a ≤ b" "0 < c" "c ≠ 1"
shows "(∫⇧+x∈{a..b}. c.^x ∂lborel) = (c.^b - c.^a) / ln c"
proof -
let ?F = "λx. c.^x / ln c"
have "⋀x. DERIV ?F x :> c.^x"
proof -
fix x
have "DERIV ?F x :> ?F x * ln c"
using DERIV_fun_powr2 assms by (intro derivative_eq_intros) simp+
thus "DERIV ?F x :> c.^x"
using assms by simp
qed
thus ?thesis
using assms by (rewrite nn_integral_FTC_Icc[where F="?F"]; simp add: field_simps)
qed
lemma nn_integral_powr_Icc_gen:
fixes a b c :: real
assumes "0 < c" "c ≠ 1"
shows "(∫⇧+x∈{a..b}. c.^x ∂lborel) = (if a ≤ b then (c.^b - c.^a) / ln c else 0)"
proof (cases ‹a ≤ b›)
case True
thus ?thesis using nn_integral_powr_Icc assms by simp
next
case False
thus ?thesis by simp
qed
lemma nn_integral_powr_Icc_finite:
fixes a b c :: real
assumes "0 < c"
shows "(∫⇧+x∈{a..b}. c.^x ∂lborel) < ⊤"
proof (cases ‹c = 1›)
case True
hence "(∫⇧+x∈{a..b}. c.^x ∂lborel) = (∫⇧+x∈{a..b}. 1 ∂lborel)" by simp
also have "… = emeasure lborel {a..b}" using nn_integral_indicator by simp
also have "… < ⊤" by (simp add: emeasure_lborel_Icc_eq)
finally show ?thesis .
next
case False
thus ?thesis by (rewrite nn_integral_powr_Icc_gen; simp add: assms)
qed
lemma nn_integral_powr_Ico_finite:
fixes a b c :: real
assumes "0 < c"
shows "(∫⇧+x∈{a..<b}. c.^x ∂lborel) < ⊤"
proof -
have "(∫⇧+x∈{a..<b}. c.^x ∂lborel) ≤ (∫⇧+x∈{a..b}. c.^x ∂lborel)"
by (rule nn_set_integral_set_mono) force
also have "… < ⊤"
using nn_integral_powr_Icc_finite assms by simp
finally show ?thesis .
qed
lemma nn_integral_powr_Ioc_finite:
fixes a b c :: real
assumes "0 < c"
shows "(∫⇧+x∈{a<..b}. c.^x ∂lborel) < ⊤"
proof -
have "(∫⇧+x∈{a<..b}. c.^x ∂lborel) ≤ (∫⇧+x∈{a..b}. c.^x ∂lborel)"
by (rule nn_set_integral_set_mono) force
also have "… < ⊤"
using nn_integral_powr_Icc_finite assms by simp
finally show ?thesis .
qed
lemma nn_integral_powr_Ici:
fixes a c :: real
assumes "0 < c" "c < 1"
shows "(∫⇧+x∈{a..}. c.^x ∂lborel) = - (c.^a / ln c)"
proof -
have "((λx. c.^x / ln c) ⤏ 0 / ln c) at_top"
using assms by (intro tendsto_intros; simp add: powr_0_at_top)
with has_real_derivative_powr2_ln show ?thesis
using assms by (rewrite nn_integral_FTC_atLeast) simp_all+
qed
lemma nn_integral_powr_Iic:
fixes b c :: real
assumes "1 < c"
shows "(∫⇧+x∈{..b}. c.^x ∂lborel) = c.^b / ln c"
proof -
have "((λx. c.^x / ln c) ⤏ 0 / ln c) at_bot"
using assms by (intro tendsto_intros; simp add: powr_0_at_bot)
with has_real_derivative_powr2_ln show ?thesis
using assms by (rewrite nn_integral_FTC_atMost) simp_all+
qed
lemma nn_set_integral_eq_set_integral2:
assumes [measurable]:"set_integrable M A f"
and "AE x ∈ A in M. 0 ≤ f x" "A ∈ sets M"
shows "(∫⇧+x∈A. f x ∂M) = (∫x∈A. f x ∂M)"
proof -
have "integrable M (λx. indicat_real A x * f x)"
using assms unfolding set_integrable_def by simp
moreover have "AE x ∈ A in M. 0 ≤ indicat_real A x * f x"
using assms by simp
ultimately have "(∫x∈A. indicat_real A x * f x ∂M) = (∫⇧+x∈A. indicat_real A x * f x ∂M)"
using nn_set_integral_eq_set_integral[of M "λx. indicat_real A x * f x"] ‹A ∈ sets M›
unfolding set_lebesgue_integral_def by simp
moreover have "(∫x∈A. indicat_real A x * f x ∂M) = (∫x∈A. f x ∂M)"
by (rule set_lebesgue_integral_cong; simp add: assms)
moreover have "(∫⇧+x∈A. indicat_real A x * f x ∂M) = (∫⇧+x∈A. f x ∂M)"
by (rule set_nn_integral_cong; simp)
ultimately show ?thesis by simp
qed
lemma set_integrable_iff_bounded:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "A ∈ sets M"
shows "set_integrable M A f ⟷ set_borel_measurable M A f ∧ (∫⇧+x∈A. norm (f x) ∂M) < ∞"
unfolding set_integrable_def set_borel_measurable_def using integrable_iff_bounded
by (smt (verit, ccfv_threshold) indicator_mult_ennreal indicator_pos_le
mult.commute nn_integral_cong norm_scaleR)
lemma set_integrable_powr_Icc:
fixes a b c :: real
assumes "0 < c"
shows "set_integrable lborel {a..b} (λx. c.^x)"
proof -
have "set_borel_measurable lborel {a..b} (λx. c.^x)" unfolding set_borel_measurable_def by simp
moreover have "(∫⇧+x∈{a..b}. c.^x ∂lborel) < ⊤" using assms nn_integral_powr_Icc_finite by simp
ultimately show ?thesis by (rewrite set_integrable_iff_bounded; simp)
qed
lemma set_integrable_powr_Ici:
fixes a c :: real
assumes "0 < c" "c < 1"
shows "set_integrable lborel {a..} (λx. c.^x)"
proof -
have "set_borel_measurable lborel {a..} (λx. c.^x)" unfolding set_borel_measurable_def by simp
moreover have "(∫⇧+x∈{a..}. c.^x ∂lborel) < ⊤" using assms nn_integral_powr_Ici by simp
ultimately show ?thesis by (rewrite set_integrable_iff_bounded; simp)
qed
lemma set_integrable_powr_Iic:
fixes b c :: real
assumes "c > 1"
shows "set_integrable lborel {..b} (λx. c.^x)"
proof -
have "set_borel_measurable lborel {..b} (λx. c.^x)" unfolding set_borel_measurable_def by simp
moreover have "(∫⇧+x∈{..b}. c.^x ∂lborel) < ⊤" using assms nn_integral_powr_Iic by simp
ultimately show ?thesis by (rewrite set_integrable_iff_bounded; simp)
qed
lemma LBINT_powr_Icc:
fixes a b c :: real
assumes "a ≤ b" "0 < c" "c ≠ 1"
shows "(LBINT x:{a..b}. c.^x) = (c.^b - c.^a) / ln c"
proof -
have "ennreal (LBINT x:{a..b}. c.^x) = (∫⇧+x∈{a..b}. c.^x ∂lborel)"
using set_integrable_powr_Icc assms by (rewrite nn_set_integral_eq_set_integral2; simp)
also have "… = ennreal ((c.^b - c.^a) / ln c)"
using nn_integral_powr_Icc assms by simp
moreover have "0 ≤ (LBINT x:{a..b}. c.^x)"
unfolding set_lebesgue_integral_def apply (rule Bochner_Integration.integral_nonneg)
using powr_ge_zero by simp
moreover have "0 ≤ (c.^b - c.^a) / ln c"
using assms by (smt (verit, best) ln_le_zero_iff powr_less_cancel powr_mono' zero_le_divide_iff)
ultimately show ?thesis
using ennreal_inj by simp
qed
lemma LBINT_powr_Ici:
fixes a c :: real
assumes "0 < c" "c < 1"
shows "(LBINT x:{a..}. c.^x) = - (c.^a / ln c)"
proof -
have "ennreal (LBINT x:{a..}. c.^x) = (∫⇧+x∈{a..}. c.^x ∂lborel)"
using set_integrable_powr_Ici assms by (rewrite nn_set_integral_eq_set_integral2; simp)
also have "… = ennreal (- (c.^a / ln c))"
using nn_integral_powr_Ici assms by simp
moreover have "0 ≤ (LBINT x:{a..}. c.^x)"
unfolding set_lebesgue_integral_def apply (rule Bochner_Integration.integral_nonneg)
using powr_ge_zero by simp
moreover have "0 ≤ - (c.^a / ln c)"
using assms by (simp add: divide_nonneg_neg)
ultimately show ?thesis
using ennreal_inj by simp
qed
lemma LBINT_powr_Iic:
fixes b c :: real
assumes "1 < c"
shows "(LBINT x:{..b}. c.^x) = c.^b / ln c"
proof -
have "ennreal (LBINT x:{..b}. c.^x) = (∫⇧+x∈{..b}. c.^x ∂lborel)"
using set_integrable_powr_Iic assms by (rewrite nn_set_integral_eq_set_integral2; simp)
also have "… = ennreal (c.^b / ln c)"
using nn_integral_powr_Iic assms by simp
moreover have "0 ≤ (LBINT x:{..b}. c.^x)"
unfolding set_lebesgue_integral_def apply (rule Bochner_Integration.integral_nonneg)
using powr_ge_zero by simp
moreover have "0 ≤ c.^b / ln c"
using assms by (simp add: divide_nonneg_neg)
ultimately show ?thesis
using ennreal_inj by simp
qed
lemma has_integral_set_integral_real:
fixes f::"'a::euclidean_space ⇒ real" and A :: "'a set"
assumes f: "set_integrable lborel A f"
shows "(f has_integral (set_lebesgue_integral lborel A f)) A"
using assms has_integral_integral_real[where f="λx. indicat_real A x * f x"]
by (simp add: has_integral_iff set_borel_integral_eq_integral)
lemma set_borel_measurable_UNIV[simp]:
fixes f :: "'a :: real_vector ⇒ real"
shows "set_borel_measurable M UNIV f ⟷ f ∈ borel_measurable M"
unfolding set_borel_measurable_def by simp
lemma set_borel_measurable_lborel:
"set_borel_measurable lborel A f ⟷ set_borel_measurable borel A f"
unfolding set_borel_measurable_def by simp
lemma restrict_space_whole[simp]: "restrict_space M (space M) = M"
unfolding restrict_space_def by (simp add: measure_of_of_measure)
lemma deriv_measurable_real:
fixes f :: "real ⇒ real"
assumes "f differentiable_on S" "open S" "f ∈ borel_measurable borel"
shows "set_borel_measurable borel S (deriv f)"
proof -
have "⋀x. x ∈ S ⟹ deriv f x = lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i))"
proof -
fix x assume x_S: "x ∈ S"
hence "f field_differentiable (at x within S)"
using differentiable_on_eq_field_differentiable_real assms by simp
hence "(f has_field_derivative deriv f x) (at x)"
using assms DERIV_deriv_iff_field_differentiable x_S at_within_open by force
hence "(λh. (f (x+h) - f x) / h) ─0→ deriv f x" using DERIV_def by auto
hence "∀d. (∀i. d i ∈ UNIV-{0::real}) ⟶ d ⇢ 0 ⟶
((λh. (f (x+h) - f x) / h) ∘ d) ⇢ deriv f x"
using tendsto_at_iff_sequentially by blast
moreover have "∀i. 1 / Suc i ∈ UNIV - {0::real}" by simp
moreover have "(λi. 1 / Suc i) ⇢ 0" using LIMSEQ_Suc lim_const_over_n by blast
ultimately have "((λh. (f (x+h) - f x) / h) ∘ (λi. 1 / Suc i)) ⇢ deriv f x" by auto
thus "deriv f x = lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i))"
unfolding comp_def by (simp add: limI)
qed
moreover have "(λx. indicator S x * lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i)))
∈ borel_measurable borel"
using assms by (measurable, simp, measurable)
ultimately show ?thesis
unfolding set_borel_measurable_def measurable_cong
by simp (smt (verit) indicator_simps(2) measurable_cong mult_eq_0_iff)
qed
corollary deriv_measurabe_real_UNIV:
fixes f :: "real ⇒ real"
assumes "f differentiable_on UNIV" "f ∈ borel_measurable borel"
shows "deriv f ∈ borel_measurable borel"
using deriv_measurable_real[where S=UNIV] assms by simp
lemma piecewise_differentiable_on_deriv_measurable_real:
fixes f :: "real ⇒ real"
assumes "f piecewise_differentiable_on S" "open S" "f ∈ borel_measurable borel"
shows "set_borel_measurable borel S (deriv f)"
proof -
from assms obtain T where fin: "finite T" and
diff: "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
with assms have "open (S - T)" using finite_imp_closed by blast
moreover hence "f differentiable_on (S - T)"
unfolding differentiable_on_def using assms by (metis Diff_iff at_within_open diff)
ultimately have "set_borel_measurable borel (S - T) (deriv f)"
by (intro deriv_measurable_real; simp add: assms)
moreover have "x ∉ T ⟹ indicat_real (S - T) x = indicat_real S x" for x
by(simp add: indicator_diff)
ultimately show ?thesis
using fin
by(auto intro!: measurable_discrete_difference[where f="λx. indicat_real (S - T) x * deriv f x"]
countable_finite simp: set_borel_measurable_def)
qed
corollary piecewise_differentiable_on_deriv_measurable_real_UNIV:
fixes f :: "real ⇒ real"
assumes "f piecewise_differentiable_on UNIV" "f ∈ borel_measurable borel"
shows "(deriv f) ∈ borel_measurable borel"
using piecewise_differentiable_on_deriv_measurable_real[where S=UNIV] assms by simp
lemma borel_measurable_antimono:
fixes f :: "real ⇒ real"
shows "antimono f ⟹ f ∈ borel_measurable borel"
using borel_measurable_mono[of "λx. - f x"] by (simp add: antimonoD monoI)
lemma set_borel_measurable_restrict_space_iff:
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ set_borel_measurable M Ω f"
using assms borel_measurable_restrict_space_iff set_borel_measurable_def by blast
lemma set_integrable_restrict_space_iff:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "A ∈ sets M"
shows "set_integrable M A f ⟷ integrable (restrict_space M A) f"
unfolding set_integrable_def using assms
by (rewrite integrable_restrict_space; simp)
lemma set_lebesgue_integral_restrict_space:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "A ∈ sets M"
shows "set_lebesgue_integral M A f = integral⇧L (restrict_space M A) f"
unfolding set_lebesgue_integral_def using assms integral_restrict_space
by (metis (mono_tags) sets.Int_space_eq2)
lemma distr_borel_lborel: "distr M borel f = distr M lborel f"
by (metis distr_cong sets_lborel)
lemma AE_translation:
assumes "AE x in lborel. P x" shows "AE x in lborel. P (a+x)"
proof -
from assms obtain N where P: "⋀x. x ∈ space lborel - N ⟹ P x" and null: "N ∈ null_sets lborel"
using AE_E3 by blast
hence "{y. a+y ∈ N} ∈ null_sets lborel"
using null_sets_translation[of N "-a"] by (simp add: add.commute)
moreover have "⋀y. y ∈ space lborel - {y. a+y ∈ N} ⟹ P (a+y)" using P by force
ultimately show "AE y in lborel. P (a+y)"
by (metis (no_types, lifting) Collect_mono P UNIV_I eventually_ae_filter
Diff_iff space_borel space_lborel)
qed
lemma set_AE_translation:
assumes "AE x∈S in lborel. P x" shows "AE x ∈ plus (-a) ` S in lborel. P (a+x)"
proof -
have "AE x in lborel. a+x ∈ S ⟶ P (a+x)" using assms by (rule AE_translation)
moreover have "⋀x. a+x ∈ S ⟷ x ∈ plus (-a) ` S" by force
ultimately show ?thesis by simp
qed
lemma AE_scale_measure_iff:
assumes "r > 0"
shows "(AE x in (scale_measure r M). P x) ⟷ (AE x in M. P x)"
unfolding ae_filter_def null_sets_def
using assms by(auto intro!: arg_cong[where f="λA. eventually P (Inf A)"] simp: space_scale_measure)
lemma nn_set_integral_cong2:
assumes "AE x∈A in M. f x = g x"
shows "(∫⇧+x∈A. f x ∂M) = (∫⇧+x∈A. g x ∂M)"
using assms by(auto intro!: nn_integral_cong_AE)
lemma nn_integral_minus_null:
assumes "A ∈ sets M" "B ∈ sets M" "B ∈ null_sets M"
shows "(∫⇧+x ∈ A. f x ∂M) = (∫⇧+x ∈ A - B. f x ∂M)"
proof -
have "sym_diff A (A - B) = A ∩ B" by force
moreover have "A ∩ B ∈ null_sets M" using assms null_set_Int1 by blast
ultimately show ?thesis using assms by (rewrite nn_integral_null_delta; simp)
qed
lemma set_lebesgue_integral_cong_AE2:
assumes [measurable]: "A ∈ sets M" "set_borel_measurable M A f" "set_borel_measurable M A g"
assumes "AE x ∈ A in M. f x = g x"
shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
using assms
by(auto simp: set_lebesgue_integral_def set_borel_measurable_def
intro!: Bochner_Integration.integral_cong_AE)
proposition set_nn_integral_eq_set_integral:
assumes "AE x∈A in M. 0 ≤ f x" "set_integrable M A f"
shows "(∫⇧+x∈A. f x ∂M) = (∫x∈A. f x ∂M)"
proof -
have "(∫⇧+x∈A. f x ∂M) = ∫⇧+x. ennreal (f x * indicator A x) ∂M"
using nn_integral_set_ennreal by blast
also have "… = ∫x. f x * indicator A x ∂M"
using assms unfolding set_integrable_def
by (rewrite nn_integral_eq_integral; force simp add: mult.commute)
also have "… = (∫x∈A. f x ∂M)" unfolding set_lebesgue_integral_def by (simp add: mult.commute)
finally show ?thesis .
qed
proposition nn_integral_disjoint_family_on_finite:
assumes [measurable]: "f ∈ borel_measurable M" "⋀(n::nat). n ∈ S ⟹ B n ∈ sets M"
and "disjoint_family_on B S" "finite S"
shows "(∫⇧+x ∈ (⋃n∈S. B n). f x ∂M) = (∑n∈S. (∫⇧+x ∈ B n. f x ∂M))"
proof -
let ?A = "λn::nat. if n ∈ S then B n else {}"
have "⋀n::nat. ?A n ∈ sets M" by simp
moreover have "disjoint_family ?A"
unfolding disjoint_family_on_def
proof -
{ fix m n :: nat
assume "m ≠ n"
hence "(if m ∈ S then B m else {}) ∩ (if n ∈ S then B n else {}) = {}"
using assms unfolding disjoint_family_on_def by simp }
thus "∀m::nat∈UNIV. ∀n::nat∈UNIV. m ≠ n ⟶
(if m ∈ S then B m else {}) ∩ (if n ∈ S then B n else {}) = {}"
by blast
qed
ultimately have "set_nn_integral M (⋃ (range ?A)) f = (∑n. set_nn_integral M (?A n) f)"
by (rewrite nn_integral_disjoint_family; simp)
moreover have "set_nn_integral M (⋃ (range ?A)) f = (∫⇧+x ∈ (⋃n∈S. B n). f x ∂M)"
proof -
have "⋃ (range ?A) = (⋃n∈S. B n)" by simp
thus ?thesis by simp
qed
moreover have "(∑n. set_nn_integral M (?A n) f) = (∑n∈S. set_nn_integral M (B n) f)"
by (rewrite suminf_finite[of S]; simp add: assms)
ultimately show ?thesis by simp
qed
lemma set_nn_integral_monotone_convergence_SUP:
assumes "incseq f" and "⋀i. f i ∈ borel_measurable M" and "A ∈ sets M"
shows "(∫⇧+x∈A. (SUP i. f i x) ∂M) = (SUP i. (∫⇧+x∈A. f i x ∂M))"
proof -
have "⋀x. (SUP i. f i x) * indicator A x = (SUP i. f i x * indicator A x)"
using SUP_mult_right_ennreal by blast
hence "(∫⇧+x∈A. (SUP i. f i x) ∂M) = (∫⇧+ x. (SUP i. f i x * indicator A x) ∂M)" by simp
moreover have "incseq (λi. (λx. f i x * indicator A x))"
using assms unfolding incseq_def le_fun_def by (simp add: mult_right_mono)
moreover have "⋀i. (λx. f i x * indicator A x) ∈ borel_measurable M" using assms by simp
ultimately show ?thesis using nn_integral_monotone_convergence_SUP by force
qed
lemma set_nn_integral_sum:
assumes "⋀i. i ∈ P ⟹ f i ∈ borel_measurable M" and "A ∈ sets M"
shows "(∫⇧+x∈A. (∑i∈P. f i x) ∂M) = (∑i∈P. ∫⇧+x∈A. f i x ∂M)" (is "?LHS = ?RHS")
proof -
have "?LHS = ∫⇧+x. (∑i∈P. f i x * indicator A x) ∂M" by (simp add: sum_distrib_right)
also have "… = ?RHS" using assms by (rewrite nn_integral_sum; simp)
finally show ?thesis .
qed
lemma set_nn_integral_indicator:
assumes "A ∈ sets M" "B ∈ sets M"
shows "set_nn_integral M A (indicator B) = emeasure M (B ∩ A)"
using assms nn_integral_indicator
by (metis (no_types, lifting) indicator_inter_arith nn_integral_cong sets.Int)
lemma nn_integral_distr_set:
assumes [measurable]:"T ∈ measurable M M'" and [measurable]:"f ∈ borel_measurable (distr M M' T)"
and [measurable]:"A ∈ sets M'" and "⋀x. x ∈ space M ⟹ T x ∈ A"
shows "integral⇧N (distr M M' T) f = set_nn_integral (distr M M' T) A f"
proof -
have *:"⋀x. x ∈ space M ⟹ f (T x) * indicator (space M') (T x) = f (T x) * indicator A (T x)"
using assms measurable_space[of T M M'] by(simp add: indicator_def)
have "integral⇧N (distr M M' T) f = (∫⇧+x∈(space M'). f x ∂(distr M M' T))"
by (rewrite nn_set_integral_space[THEN sym], simp)
also have "… = (∫⇧+x∈A. f x ∂(distr M M' T))"
by(auto simp add: nn_integral_distr * intro!: nn_integral_cong)
finally show ?thesis .
qed
lemma measure_eqI_Ioc:
fixes M N :: "real measure"
assumes sets: "sets M = sets borel" "sets N = sets borel"
assumes fin: "⋀a b. a ≤ b ⟹ emeasure M {a<..b} < ∞"
assumes eq: "⋀a b. a ≤ b ⟹ emeasure M {a<..b} = emeasure N {a<..b}"
shows "M = N"
proof (rule measure_eqI_generator_eq_countable)
let ?Ioc = "λ(a::real,b::real). {a<..b}" let ?E = "range ?Ioc"
show "Int_stable ?E" using Int_stable_def Int_greaterThanAtMost by force
show "?E ⊆ Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E"
unfolding sets by (auto simp add: borel_sigma_sets_Ioc)
show "⋀I. I ∈ ?E ⟹ emeasure M I = emeasure N I"
proof -
fix I assume "I ∈ ?E"
then obtain a b where "I = {a<..b}" by auto
thus "emeasure M I = emeasure N I" by (smt (verit, best) eq greaterThanAtMost_empty)
qed
show "?Ioc ` (Rats × Rats) ⊆ ?E" "(⋃i∈(Rats×Rats). ?Ioc i) = UNIV"
using Rats_no_bot_less Rats_no_top_le by auto
show "countable (?Ioc ` (Rats × Rats))" using countable_rat by blast
show "⋀I. I ∈ ?Ioc ` (Rats × Rats) ⟹ emeasure M I ≠ ∞"
proof -
fix I assume "I ∈ ?Ioc ` (Rats × Rats)"
then obtain a b where "(a,b) ∈ (Rats × Rats)" "I = {a<..b}" by blast
thus "emeasure M I ≠ ∞" by (smt (verit, best) Ioc_inj fin order.strict_implies_not_eq)
qed
qed
lemma (in finite_measure) distributed_measure:
assumes "distributed M N X f"
and f_nn: "⋀x. x ∈ space N ⟹ f x ≥ 0"
and [measurable]:"A ∈ sets N"
shows "measure M (X -` A ∩ space M) = (∫x. indicator A x * f x ∂N)"
proof -
have [measurable]:"f ∈ borel_measurable N"
using assms distributed_real_measurable by blast
have "emeasure M (X -` A ∩ space M) = (∫⇧+x∈A. ennreal (f x) ∂N)"
by (rule distributed_emeasure; simp add: assms)
moreover have "enn2real (∫⇧+x∈A. ennreal (f x) ∂N) = ∫x. indicator A x * f x ∂N"
by(subst integral_eq_nn_integral)
(use f_nn in "auto simp: mult.commute nn_integral_set_ennreal")
ultimately show ?thesis using measure_def by metis
qed
lemma set_integrable_const[simp]:
"A ∈ sets M ⟹ emeasure M A < ∞ ⟹ set_integrable M A (λ_. c)"
using has_bochner_integral_indicator unfolding set_integrable_def by simp
lemma set_integral_const[simp]:
"A ∈ sets M ⟹ emeasure M A < ∞ ⟹ set_lebesgue_integral M A (λ_. c) = measure M A *⇩R c"
unfolding set_lebesgue_integral_def using has_bochner_integral_indicator by force
lemma set_integral_empty_0[simp]: "set_lebesgue_integral M {} f = 0"
unfolding set_lebesgue_integral_def by simp
lemma set_integral_nonneg[simp]:
fixes f :: "'a ⇒ real" and A :: "'a set"
shows "(⋀x. x ∈ A ⟹ 0 ≤ f x) ⟹ 0 ≤ set_lebesgue_integral M A f"
unfolding set_lebesgue_integral_def by (simp add: indicator_times_eq_if)
lemma
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
assumes "A ∈ sets M" "set_borel_measurable M A f"
"⋀i. set_borel_measurable M A (s i)" "set_integrable M A w"
assumes lim: "AE x∈A in M. (λi. s i x) ⇢ f x"
assumes bound: "⋀i::nat. AE x∈A in M. norm (s i x) ≤ w x"
shows set_integrable_dominated_convergence: "set_integrable M A f"
and set_integrable_dominated_convergence2: "⋀i. set_integrable M A (s i)"
and set_integral_dominated_convergence:
"(λi. set_lebesgue_integral M A (s i)) ⇢ set_lebesgue_integral M A f"
proof -
have "(λx. indicator A x *⇩R f x) ∈ borel_measurable M" and
"⋀i. (λx. indicator A x *⇩R s i x) ∈ borel_measurable M" and
"integrable M (λx. indicator A x *⇩R w x)"
using assms unfolding set_borel_measurable_def set_integrable_def by simp_all
moreover have "AE x in M. (λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof -
obtain N where N_null: "N ∈ null_sets M" and
si_f: "⋀x. x ∈ space M - N ⟹ x ∈ A ⟶ (λi. s i x) ⇢ f x"
using lim AE_E3 by (smt (verit))
hence "⋀x. x ∈ space M - N ⟹ (λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof -
fix x assume asm: "x ∈ space M - N"
thus "(λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof (cases ‹x ∈ A›)
case True
with si_f asm show ?thesis by simp
next
case False
thus ?thesis by simp
qed
qed
thus ?thesis
by(auto intro!: AE_I'[OF N_null])
qed
moreover have "⋀i. AE x in M. norm (indicator A x *⇩R s i x) ≤ indicator A x *⇩R w x"
proof -
fix i
from bound obtain N where N_null: "N ∈ null_sets M" and
"⋀x. x ∈ space M - N ⟹ x ∈ A ⟶ norm (s i x) ≤ w x"
using AE_E3 by (smt (verit))
hence "⋀x. x ∈ space M - N ⟹ norm (indicator A x *⇩R s i x) ≤ indicator A x *⇩R w x"
by (simp add: indicator_scaleR_eq_if)
with N_null show "AE x in M. norm (indicator A x *⇩R s i x) ≤ indicator A x *⇩R w x"
by (smt (verit) DiffI eventually_ae_filter mem_Collect_eq subsetI)
qed
ultimately show "set_integrable M A f" "⋀i. set_integrable M A (s i)"
"(λi. set_lebesgue_integral M A (s i)) ⇢ set_lebesgue_integral M A f"
unfolding set_integrable_def set_lebesgue_integral_def
by (rule integrable_dominated_convergence, rule integrable_dominated_convergence2,
rule integral_dominated_convergence)
qed
lemma absolutely_integrable_on_iff_set_integrable:
fixes f :: "'a::euclidean_space ⇒ real"
assumes [measurable]:"f ∈ borel_measurable lborel" "S ∈ sets lborel"
shows "set_integrable lborel S f ⟷ f absolutely_integrable_on S"
by(simp add: integrable_completion set_integrable_def)
corollary integrable_on_iff_set_integrable_nonneg:
fixes f :: "'a::euclidean_space ⇒ real"
assumes "⋀x. x ∈ S ⟹ f x ≥ 0" "f ∈ borel_measurable lborel"
and "S ∈ sets lborel"
shows "set_integrable lborel S f ⟷ f integrable_on S"
using absolutely_integrable_on_iff_set_integrable assms
by (metis absolutely_integrable_on_iff_nonneg)
lemma integrable_on_iff_set_integrable_nonneg_AE:
fixes f :: "'a::euclidean_space ⇒ real"
assumes "AE x∈S in lborel. f x ≥ 0"
and [measurable]:"f ∈ borel_measurable lborel" "S ∈ sets lborel"
shows "set_integrable lborel S f ⟷ f integrable_on S"
proof -
from assms obtain N where nonneg: "⋀x. x ∈ S - N ⟹ f x ≥ 0" and null: "N ∈ null_sets lborel"
using AE_E3 by force
let ?g = "λx. if x ∈ N then 0 else f x"
have [simp]: "negligible N" using null negligible_iff_null_sets null_sets_completionI by blast
have "N ∈ sets lborel" using null by auto
hence [simp]: "?g ∈ borel_measurable borel" using assms by force
have "set_integrable lborel S f ⟷ set_integrable lborel S ?g"
proof -
have "AE x∈S in lborel. f x = ?g x"
by(auto intro!: AE_I'[OF null])
thus ?thesis using assms by (intro set_integrable_cong_AE[of f _ ?g S]; simp)
qed
also have "… ⟷ ?g integrable_on S"
using assms by (intro integrable_on_iff_set_integrable_nonneg; simp add: nonneg)
also have "… ⟷ f integrable_on S" by (rule integrable_spike_cong[of N]; simp)
finally show ?thesis .
qed
lemma set_borel_integral_eq_integral_nonneg:
fixes f :: "'a::euclidean_space ⇒ real"
assumes "⋀x. x ∈ S ⟹ f x ≥ 0" "f ∈ borel_measurable borel" "S ∈ sets borel"
shows "(LINT x : S | lborel. f x) = integral S f"
proof (cases ‹set_integrable lborel S f›)
case True
thus ?thesis using set_borel_integral_eq_integral by force
next
case False
hence "(LINT x : S | lborel. f x) = 0"
unfolding set_lebesgue_integral_def set_integrable_def
by (rewrite not_integrable_integral_eq; simp)
moreover have "integral S f = 0"
apply (rule not_integrable_integral)
using False assms by (rewrite in asm integrable_on_iff_set_integrable_nonneg; simp)
ultimately show ?thesis ..
qed
lemma set_borel_integral_eq_integral_nonneg_AE:
fixes f :: "'a::euclidean_space ⇒ real"
assumes "AE x∈S in lborel. f x ≥ 0" "f ∈ borel_measurable borel" "S ∈ sets borel"
shows "(LINT x : S | lborel. f x) = integral S f"
proof (cases ‹set_integrable lborel S f›)
case True
thus ?thesis using set_borel_integral_eq_integral by force
next
case False
hence "(LINT x : S | lborel. f x) = 0"
unfolding set_lebesgue_integral_def set_integrable_def
by (rewrite not_integrable_integral_eq; simp)
moreover have "integral S f = 0"
apply (rule not_integrable_integral)
using False assms by (rewrite in asm integrable_on_iff_set_integrable_nonneg_AE; simp)
ultimately show ?thesis ..
qed
subsection ‹Set Lebesgue Integrability on Affine Transformation›
lemma set_integrable_Icc_affine_pos_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b c t :: real
assumes [arith]:"c > 0"
shows "set_integrable lborel {(a-t)/c..(b-t)/c} (λx. f (t + c*x))
⟷ set_integrable lborel {a..b} f"
unfolding set_integrable_def indicator_Icc_affine_pos_inverse[OF assms]
by(intro lborel_integrable_real_affine_iff) simp
corollary set_integrable_Icc_shift:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b t :: real
shows "set_integrable lborel {a-t..b-t} (λx. f (t+x)) ⟷ set_integrable lborel {a..b} f"
using set_integrable_Icc_affine_pos_iff[where c=1] by simp
lemma set_integrable_Ici_affine_pos_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a c t :: real
assumes [arith]:"c > 0"
shows "set_integrable lborel {(a-t)/c..} (λx. f (t + c*x))
⟷ set_integrable lborel {a..} f"
unfolding set_integrable_def indicator_Ici_affine_pos_inverse[OF assms]
by (rule lborel_integrable_real_affine_iff) simp
corollary set_integrable_Ici_shift:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a t :: real
shows "set_integrable lborel {a-t..} (λx. f (t+x)) ⟷ set_integrable lborel {a..} f"
using set_integrable_Ici_affine_pos_iff[where c=1] by simp
lemma set_integrable_Iic_affine_pos_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b c t :: real
assumes [arith]:"c > 0"
shows "set_integrable lborel {..(b-t)/c} (λx. f (t + c*x))
⟷ set_integrable lborel {..b} f"
unfolding set_integrable_def indicator_Iic_affine_pos_inverse[OF assms]
by (rule lborel_integrable_real_affine_iff) simp
corollary set_integrable_Iic_shift:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b t :: real
shows "set_integrable lborel {..b-t} (λx. f (t+x)) ⟷ set_integrable lborel {..b} f"
using set_integrable_Iic_affine_pos_iff[where c=1] by simp
lemma set_integrable_Icc_affine_neg_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b c t :: real
assumes [arith]:"c < 0"
shows "set_integrable lborel {(b-t)/c..(a-t)/c} (λx. f (t + c*x))
⟷ set_integrable lborel {a..b} f"
unfolding set_integrable_def indicator_Icc_affine_neg_inverse[OF assms]
by (rule lborel_integrable_real_affine_iff) simp
corollary set_integrable_Icc_reverse:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b t :: real
shows "set_integrable lborel {t-b..t-a} (λx. f (t-x)) ⟷ set_integrable lborel {a..b} f"
using set_integrable_Icc_affine_neg_iff[where c="-1"] by simp
lemma set_integrable_Ici_affine_neg_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b c t :: real
assumes [arith]:"c < 0"
shows "set_integrable lborel {(b-t)/c..} (λx. f (t + c*x))
⟷ set_integrable lborel {..b} f"
unfolding set_integrable_def indicator_Ici_affine_neg_inverse[OF assms]
by (rule lborel_integrable_real_affine_iff) simp
corollary set_integrable_Ici_reverse:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b t :: real
shows "set_integrable lborel {t-b..} (λx. f (t-x)) ⟷ set_integrable lborel {..b} f"
using set_integrable_Ici_affine_neg_iff[where c="-1"] by simp
lemma set_integrable_Iic_affine_neg_iff:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a c t :: real
assumes [arith]:"c < 0"
shows "set_integrable lborel {..(a-t)/c} (λx. f (t + c*x))
⟷ set_integrable lborel {a..} f"
unfolding set_integrable_def indicator_Iic_affine_neg_inverse[OF assms]
by (rule lborel_integrable_real_affine_iff) simp
corollary set_integrable_Iic_reverse:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a t :: real
shows "set_integrable lborel {..t-a} (λx. f (t-x)) ⟷ set_integrable lborel {a..} f"
using set_integrable_Iic_affine_neg_iff[where c="-1"] by simp
subsection ‹Set Lebesgue Integral on Affine Transformation›
lemma lborel_set_integral_Icc_affine_pos:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b c :: real
assumes [arith]:"c > 0"
shows "(∫x∈{a..b}. f x ∂lborel) = c *⇩R (∫x∈{(a-t)/c..(b-t)/c}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Icc_affine_pos_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Icc_shift:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b :: real
shows "(∫x∈{a..b}. f x ∂lborel) = (∫x∈{a-t..b-t}. f (t+x) ∂lborel)"
using lborel_set_integral_Icc_affine_pos[where c=1] by simp
lemma lborel_set_integral_Ici_affine_pos:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a c :: real
assumes [arith]:"c > 0"
shows "(∫x∈{a..}. f x ∂lborel) = c *⇩R (∫x∈{(a-t)/c..}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Ici_affine_pos_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Ici_shift:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a::real
shows "(∫x∈{a..}. f x ∂lborel) = (∫x∈{a-t..}. f (t+x) ∂lborel)"
using lborel_set_integral_Ici_affine_pos[where c=1] by simp
lemma lborel_set_integral_Iic_affine_pos:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b c :: real
assumes [arith]:"c > 0"
shows "(∫x∈{..b}. f x ∂lborel) = c *⇩R (∫x∈{..(b-t)/c}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Iic_affine_pos_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Iic_shift:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b::real
shows "(∫x∈{..b}. f x ∂lborel) = (∫x∈{..b-t}. f (t+x) ∂lborel)"
using lborel_set_integral_Iic_affine_pos[where c=1] by simp
lemma lborel_set_integral_Icc_affine_neg:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b c :: real
assumes [arith]:"c < 0"
shows "(∫x∈{a..b}. f x ∂lborel) = -c *⇩R (∫x∈{(b-t)/c..(a-t)/c}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Icc_affine_neg_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Icc_reverse:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b :: real
shows "(∫x∈{a..b}. f x ∂lborel) = (∫x∈{t-b..t-a}. f (t-x) ∂lborel)"
using lborel_set_integral_Icc_affine_neg[where c="-1"] by simp
lemma lborel_set_integral_Ici_affine_neg:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b c :: real
assumes [arith]:"c < 0"
shows "(∫x∈{..b}. f x ∂lborel) = -c *⇩R (∫x∈{(b-t)/c..}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Ici_affine_neg_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Ici_reverse:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b::real
shows "(∫x∈{..b}. f x ∂lborel) = (∫x∈{t-b..}. f (t-x) ∂lborel)"
using lborel_set_integral_Ici_affine_neg[where c="-1"] by simp
lemma lborel_set_integral_Iic_affine_neg:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a c :: real
assumes [arith]:"c < 0"
shows "(∫x∈{a..}. f x ∂lborel) = -c *⇩R (∫x∈{..(a-t)/c}. f (t + c*x) ∂lborel)"
unfolding set_lebesgue_integral_def indicator_Iic_affine_neg_inverse[OF assms]
using lborel_integral_real_affine[where c=c] by force
corollary lborel_set_integral_Iic_reverse:
fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a::real
shows "(∫x∈{a..}. f x ∂lborel) = (∫x∈{..t-a}. f (t-x) ∂lborel)"
using lborel_set_integral_Iic_affine_neg[where c="-1"] by simp
lemma set_integrable_Ici_equiv_aux:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b :: real
assumes "⋀c d. set_integrable lborel {c..d} f" "a ≤ b"
shows "set_integrable lborel {a..} f ⟷ set_integrable lborel {b..} f"
proof
assume "set_integrable lborel {a..} f"
thus "set_integrable lborel {b..} f" by (rule set_integrable_subset; simp add: assms)
next
assume "set_integrable lborel {b..} f"
moreover have "set_integrable lborel {a..b} f" using assms by blast
moreover have "{a..} = {a..b} ∪ {b..}" using assms by auto
ultimately show "set_integrable lborel {a..} f" using set_integrable_Un by force
qed
corollary set_integrable_Ici_equiv:
fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b :: real
assumes "⋀c d. set_integrable lborel {c..d} f"
shows "set_integrable lborel {a..} f ⟷ set_integrable lborel {b..} f"
using set_integrable_Ici_equiv_aux assms by (metis linorder_linear)
lemma set_integrable_Iic_equiv:
fixes f :: "real ⇒ real" and a b :: real
assumes "⋀c d. set_integrable lborel {c..d} f"
shows "set_integrable lborel {..a} f ⟷ set_integrable lborel {..b} f" (is "?LHS ⟷ ?RHS")
proof -
have "?LHS ⟷ set_integrable lborel {-a..} (λx. f (-x))"
using set_integrable_Ici_reverse[where t=0] by force
also have "… ⟷ set_integrable lborel {-b..} (λx. f (-x))"
proof -
have "⋀c d. set_integrable lborel {c..d} (λx. f (-x))"
apply (rewrite at "{⌑.._}" minus_minus[THEN sym])
apply (rewrite at "{_..⌑}" minus_minus[THEN sym])
using assms set_integrable_Icc_reverse[where t=0] by force
thus ?thesis by (rule set_integrable_Ici_equiv)
qed
also have "… ⟷ ?RHS" using set_integrable_Ici_reverse[where t=0] by force
finally show ?thesis .
qed
subsection ‹Alternative Integral Test›
lemma nn_integral_suminf_Ico_real_nat:
fixes a::real and f :: "real ⇒ ennreal"
assumes "f ∈ borel_measurable lborel"
shows "(∫⇧+x∈{a..}. f x ∂lborel) = (∑k. ∫⇧+x∈{a+k..<a+k+1}. f x ∂lborel)"
apply (rewrite Ico_real_nat_union[THEN sym])
using Ico_real_nat_disjoint assms by (intro nn_integral_disjoint_family; simp)
theorem set_integrable_iff_summable:
fixes a::real and f :: "real ⇒ real"
assumes "antimono_on {a..} f" and f_nn: "⋀x. a ≤ x ⟹ f x ≥ 0"
and [measurable]:"f ∈ borel_measurable lborel"
shows "set_integrable lborel {a..} f ⟷ summable (λk. f (a+k))"
proof
assume asm: "set_integrable lborel {a..} f"
have "∀k≥0. norm (f (a+(k+1::nat))) ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)"
proof -
{ fix k::nat
have "norm (f (a+(k+1::nat))) = f (a+k+1)"
using assms by (smt (verit) of_nat_0_le_iff of_nat_1 of_nat_add real_norm_def)
also have "… = (∫x∈{a+k..<a+k+1}. f (a+k+1) ∂lborel)"
unfolding set_lebesgue_integral_def by simp
also have "… ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)"
using assms(1)
by(intro set_integral_mono[OF _ set_integrable_restrict_space[of lborel "{a..}"]])
(auto simp: asm sets_restrict_space monotone_on_def)
finally have "norm (f (a+(k+1::nat))) ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)" . }
thus ?thesis by simp
qed
moreover have "summable (λk. ∫x∈{a+k..<a+k+1}. f x ∂lborel)"
proof -
have "(∫⇧+x∈{a..}. ennreal (f x) ∂lborel) ≠ ∞"
using asm unfolding set_integrable_def
by (metis (no_types, lifting) ext mult.commute indicator_mult_ennreal
integrableD(2) real_scaleR_def)
moreover have "(∑i. (∫⇧+x∈{a + real i..<a + real i + 1}. ennreal (f x) ∂lborel))
= (∑i. ennreal (set_lebesgue_integral lborel {a + real i..<a + real i + 1} f))"
using f_nn by(auto intro!: suminf_cong set_nn_integral_eq_set_integral set_integrable_subset[OF asm])
ultimately show ?thesis
by(auto simp: nn_integral_suminf_Ico_real_nat
intro!: summable_suminf_not_top set_integral_nonneg f_nn)
qed
ultimately have "summable (λk. f (a+(k+1::nat)))"
using summable_comparison_test by (metis (no_types, lifting))
thus "summable (λk. f (a+k))" using summable_iff_shift by blast
next
assume asm: "summable (λk. f (a+k))"
hence "(∫⇧+x∈{a..}. ennreal ¦f x¦ ∂lborel) < ∞"
proof -
have "(∫⇧+x∈{a..}. ennreal ¦f x¦ ∂lborel) = (∫⇧+x∈{a..}. ennreal (f x) ∂lborel)"
using assms by (metis abs_of_nonneg atLeast_iff indicator_simps(2) mult_eq_0_iff)
also have "… = (∑k. ∫⇧+x∈{a+k..<a+k+1}. ennreal (f x) ∂lborel)"
using assms by (rewrite nn_integral_suminf_Ico_real_nat; simp)
also have "… ≤ (∑k. ∫⇧+x∈{a+k..<a+k+1}. ennreal (f (a+k)) ∂lborel)"
proof -
have "⋀(k::nat) x. x∈{a+k..<a+k+1} ⟹ f x ≤ f (a+k)"
using assms unfolding monotone_on_def by auto
thus ?thesis
by(intro suminf_le nn_integral_mono)
(auto simp: indicator_def intro!: ennreal_leI)
qed
also have "… = (∑k. ennreal (f (a+k)))"
apply (rule suminf_cong)
by (rewrite nn_integral_cmult_indicator; simp)
also have "… < ∞"
unfolding infinity_ennreal_def apply (rewrite less_top[THEN sym])
using asm assms
by (metis (mono_tags, lifting) ennreal_suminf_neq_top le_add_same_cancel1
of_nat_0_le_iff suminf_cong)
finally show ?thesis .
qed
moreover have "set_borel_measurable lborel {a..} f"
using assms unfolding set_borel_measurable_def by simp
ultimately show "set_integrable lborel {a..} f" by (rewrite set_integrable_iff_bounded) auto
qed
subsection ‹Interchange of Differentiation and Lebesgue Integration›
definition measurable_extension :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
"measurable_extension M N f ≡ (SOME g. g ∈ M →⇩M N ∧ (AE x in M. f x = g x))"
lemma measurable_extension_def2:
"measurable_extension M N f = (SOME g. g ∈ M →⇩M N ∧ (∃S∈(null_sets M). {x ∈ space M. f x ≠ g x} ⊆ S))"
by(simp add: measurable_extension_def eventually_ae_filter)
lemma
fixes f g
assumes "g ∈ M →⇩M N" "AE x in M. f x = g x"
shows measurable_extensionI: "AE x in M. f x = measurable_extension M N f x"
(is "AE x in M. f x = ?me x")
and measurable_extensionI2: "AE x in M. g x = measurable_extension M N f x"
and measurable_extension_measurable: "measurable_extension M N f ∈ measurable M N"
proof -
have "?me ∈ M →⇩M N ∧ (AE x in M. f x = ?me x)"
unfolding measurable_extension_def
by(rule someI[where P="λh. h ∈ M →⇩M N ∧ (AE x in M. f x = h x)"]) (use assms in auto)
thus "AE x in M. f x = ?me x" "AE x in M. g x = ?me x" "?me ∈ M →⇩M N"
using assms by auto
qed
lemma measurable_extension_measurable'[measurable]:
assumes "f ∈ M →⇩M N"
shows "measurable_extension M N f ∈ M →⇩M N"
using assms by(auto intro!: measurable_extension_measurable)
lemma measurable_extensionI'[simp]:
assumes "f ∈ M →⇩M N"
shows "AE x in M. f x = measurable_extension M N f x"
using assms by(auto intro!: measurable_extensionI)
corollary measurable_measurable_extension_AE:
fixes f
assumes "f ∈ M →⇩M N"
shows "AE x in M. f x = measurable_extension M N f x"
by (rule measurable_extensionI[where g=f]; simp add: assms)
abbreviation borel_measurable_extension ::
"'a measure ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b" where
"borel_measurable_extension M f ≡ measurable_extension M borel f"
definition set_borel_measurable_extension ::
"'a measure ⇒ 'a set ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b"
where "set_borel_measurable_extension M A f = borel_measurable_extension (restrict_space M A) f"
lemma
fixes f g :: "'a ⇒ 'b::real_normed_vector" and A
assumes [measurable]:"A ∈ sets M" "set_borel_measurable M A g" "AE x∈A in M. f x = g x"
shows set_borel_measurable_extensionI:
"AE x∈A in M. f x = set_borel_measurable_extension M A f x" and
set_borel_measurable_extensionI2:
"AE x∈A in M. g x = set_borel_measurable_extension M A f x" and
set_borel_measurable_extension_measurable:
"set_borel_measurable M A (set_borel_measurable_extension M A f)"
using assms measurable_extensionI2[where g=g] measurable_extensionI[where g=g]
measurable_extension_measurable
by(auto simp: set_borel_measurable_extension_def AE_restrict_space_iff[symmetric]
set_borel_measurable_restrict_space_iff[symmetric])
corollary set_borel_measurable_measurable_extension_AE:
fixes f::"'a ⇒ 'b::real_normed_vector" and A
assumes "set_borel_measurable M A f" "A ∈ sets M"
shows "AE x∈A in M. f x = set_borel_measurable_extension M A f x"
by (simp add: assms set_borel_measurable_extensionI2)
proposition interchange_deriv_LINT_general:
fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real"
assumes f_integ: "⋀r. r∈{a<..<b} ⟹ integrable M (f r)" and
f_diff: "AE x in M. (λr. f r x) differentiable_on {a<..<b}" and
Df_bound: "AE x in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "integrable M g"
shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x. f r x ∂M) has_real_derivative
∫x. borel_measurable_extension M (λx. deriv (λr. f r x) r) x ∂M) (at r)"
proof -
text ‹Preparation›
have f_msr[measurable]: "⋀r. a < r ⟹ r <b ⟹ f r ∈ borel_measurable M" using f_integ by auto
from AE_E3 f_diff obtain N1 where N1_null: "N1 ∈ null_sets M" and
"⋀x. x ∈ space M - N1 ⟹ (λs. f s x) differentiable_on {a<..<b}"
by metis
hence f_diffN1: "⋀x. x ∈ space M - N1 ⟹ (λs. f s x) differentiable_on {a<..<b}"
by (meson Diff_iff sets.sets_into_space subset_eq)
from Df_bound obtain N2 where N2_null: "N2 ∈ null_sets M" and
"⋀x. x ∈ space M - N2 ⟹ ∀r∈{a<..<b}. ¦deriv (λs. f s x) r¦ ≤ g x"
by (auto simp: eventually_ae_filter)
hence Df_boundN2:"⋀x. x ∈ space M - N2 ⟹ ∀r∈{a<..<b}. ¦deriv (λs. f s x) r¦ ≤ g x"
by (meson Diff_iff sets.sets_into_space subset_eq)
define N where "N ≡ N1 ∪ N2"
let ?CN = "space M - N"
have N_null: "N ∈ null_sets M" and N_msr[measurable]: "N ∈ sets M"
unfolding N_def using N1_null N2_null by auto
have f_diffCN: "⋀x. x∈?CN ⟹ (λs. f s x) differentiable_on {a<..<b}"
unfolding N_def using f_diffN1 by simp
define Df :: "real ⇒ 'a ⇒ real" where
"Df r x ≡ indicator ({a<..<b}×?CN) (r,x) * deriv (λs. f s x) r" for r x
have Df_boundCN: "⋀x. x∈?CN ⟹ ∀r∈{a<..<b}. ¦Df r x¦ ≤ g x"
unfolding Df_def N_def using Df_boundN2 by simp
text ‹Main Part of the Proof›
fix r assume r_ab: "r∈{a<..<b}"
then obtain e where e_pos: "e > 0" and ball_ab: "ball r e ⊆ {a<..<b}"
by (meson openE open_greaterThanLessThan)
have "⋀d::nat⇒real. ⟦∀i. d i ∈ UNIV-{0}; d ⇢ 0⟧ ⟹
((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
proof -
fix d::"nat⇒real" assume d_neq0: "∀i. d i ∈ UNIV-{0}" and d_to0: "d ⇢ 0"
then obtain m where "∀i≥m. ¦d i - 0¦ < e" using LIMSEQ_def e_pos dist_real_def by metis
hence rd_ab: "⋀n. r + d (n+m) ∈ {a<..<b}" using dist_real_def ball_ab by (simp add: subset_eq)
have limf_Df: "⋀x. x∈?CN ⟹ (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢ Df r x"
proof -
fix x assume x_CN: "x∈?CN"
hence "(λs. f s x) field_differentiable (at r)"
using f_diffCN r_ab
by (metis at_within_open differentiable_on_eq_field_differentiable_real
open_greaterThanLessThan)
hence "((λh. (f (r+h) x - f r x) / h) ⤏ Df r x) (at 0)"
using r_ab x_CN by (simp add: Df_def DERIV_def DERIV_deriv_iff_field_differentiable[symmetric])
hence "(λi. (f (r + d i) x - f r x) / d i) ⇢ Df r x"
using d_neq0 d_to0 by(simp add: tendsto_at_iff_sequentially comp_def)
thus "(λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢ Df r x"
by (rule LIMSEQ_ignore_initial_segment[where k=m])
qed
have Df_eq:
"Df r = (λx. indicator ?CN x * lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)))"
proof
fix x
show "Df r x = indicator ?CN x * lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))"
proof (cases ‹x∈?CN›)
case True
hence "lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x"
by (intro limI, rule limf_Df)
thus ?thesis using True by simp
next
case False
thus ?thesis unfolding Df_def by simp
qed
qed
hence Df_msr[measurable]: "Df r ∈ borel_measurable M"
using r_ab rd_ab by(simp add: Df_eq)
have "((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M"
proof -
have "(λn. ∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M) ⇢
∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M"
proof -
have "AE x in M. (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢
lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))"
using limf_Df Df_eq N_null by (smt (verit) DiffI AE_I' limI mem_Collect_eq subset_eq)
moreover have "⋀n. AE x in M. norm ((f (r + d (n+m)) x - f r x) / d (n+m)) ≤ g x"
proof -
fix n
{ fix x assume x_CN: "x∈?CN"
let ?I = "{r..(r + d (n+m))} ∪ {(r + d (n+m))..r}"
have f_diffI: "(λs. f s x) differentiable_on ?I"
apply (rule differentiable_on_subset[where t="{a<..<b}"], rule f_diffCN, rule x_CN)
using r_ab rd_ab[of n] by (rewrite Un_subset_iff, auto)
hence "continuous_on ?I (λs. f s x)" "(λs. f s x) differentiable_on interior ?I"
apply -
using differentiable_imp_continuous_on apply blast
by (metis differentiable_on_subset interior_subset)
then obtain t where t_01: "t∈{0<..<1}" and
f_MVT: "f (r + d (n+m)) x - f r x = d (n+m) * deriv (λs. f s x) (r + t * (d (n+m)))"
by (rule MVT_order_free)
hence rtd_ab: "r + t * d (n+m) ∈ {a<..<b}"
using r_ab rd_ab[of n]
by simp (smt (verit, ccfv_threshold) mult_less_cancel_left mult_less_cancel_right2)
have "d (n+m) * deriv (λs. f s x) (r + t * (d (n+m))) =
d (n+m) * Df (r + t * (d (n+m))) x"
proof -
have "r + t * (d (n+m)) ∈ {a<..<b}"
using r_ab rd_ab[of n] t_01 rtd_ab by blast
thus ?thesis unfolding Df_def using x_CN by simp
qed
with f_MVT have "(f (r + d (n+m)) x - f r x) / d (n+m) = Df (r + t * (d (n+m))) x"
using d_neq0 by simp
moreover have "¦Df (r + t * (d (n+m))) x¦ ≤ g x" using Df_boundCN x_CN rtd_ab by simp
ultimately have "¦(f (r + d (n+m)) x - f r x) / d (n+m)¦ ≤ g x" by simp }
thus "AE x in M. norm ((f (r + d (n+m)) x - f r x) / d (n+m)) ≤ g x"
unfolding real_norm_def by(auto intro!: AE_I'[OF N_null])
qed
ultimately show "((λn. ∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M) ⇢
∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M)"
using Df_bound rd_ab r_ab
by(intro integral_dominated_convergence[where w=g]) simp_all
qed
moreover have "⋀n. ((∫x. f (r + d (n+m)) x ∂M) - ∫x. f r x ∂M) / d (n+m) =
∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M"
using d_neq0 rd_ab r_ab f_integ by simp
ultimately show ?thesis
unfolding comp_def using d_neq0
by (auto simp: LIMSEQ_offset[where k=m])
qed
moreover have "(∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M) =
∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
proof -
have "(∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M) = ∫x. Df r x ∂M"
proof -
have "AE x in M. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x"
proof -
{ fix x assume x_CN: "x∈?CN"
hence "lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x" by (simp add: Df_eq) }
thus ?thesis using AE_I' N_null by (smt (verit, del_insts) DiffI mem_Collect_eq subsetI)
qed
thus ?thesis
using r_ab rd_ab by (intro integral_cong_AE) auto
qed
also have "… = ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
proof -
have "AE x in M. Df r x = borel_measurable_extension M (λy. deriv (λs. f s y) r) x" and
"borel_measurable_extension M (λy. deriv (λs. f s y) r) ∈ borel_measurable M"
proof -
have "{x ∈ space M. deriv (λs. f s x) r ≠ Df r x} ⊆ N"
proof -
{ fix x assume "x∈?CN"
hence "deriv (λs. f s x) r = Df r x" unfolding Df_def using r_ab by simp }
thus ?thesis by blast
qed
hence *:"AE x in M. deriv (λs. f s x) r = Df r x"
using N_null eventually_ae_filter by blast
thus "AE x in M. Df r x = borel_measurable_extension M (λy. deriv (λs. f s y) r) x" and
"borel_measurable_extension M (λy. deriv (λs. f s y) r) ∈ borel_measurable M"
by(auto intro!: measurable_extensionI2[OF _ *] measurable_extension_measurable[OF _ *])
qed
thus ?thesis using Df_msr by (intro integral_cong_AE; simp)
qed
finally show ?thesis .
qed
ultimately show "((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
using tendsto_cong_limit by simp
qed
thus "((λs. ∫x. f s x ∂M) has_real_derivative
∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M) (at r)"
by (rewrite DERIV_def, rewrite tendsto_at_iff_sequentially) simp
qed
proposition interchange_deriv_LINT:
fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real"
assumes "⋀r. r∈{a<..<b} ⟹ integrable M (f r)" and
"AE x in M. (λr. f r x) differentiable_on {a<..<b}" and
"⋀r. r∈{a<..<b} ⟹ (λx. (deriv (λr. f r x) r)) ∈ borel_measurable M" and
"AE x in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "integrable M g"
shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x. f r x ∂M) has_real_derivative
∫x. deriv (λr. f r x) r ∂M) (at r)"
proof -
fix r assume r_ab: "r∈{a<..<b}"
hence Df_msr[measurable]: "(λx. deriv (λs. f s x) r) ∈ borel_measurable M"
using assms by simp
have "((λs. ∫x. f s x ∂M) has_real_derivative
(∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M)) (at r)"
using assms r_ab by (intro interchange_deriv_LINT_general; simp)
moreover have "(∫x. deriv (λs. f s x) r ∂M) =
(∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M)"
by(auto intro!: integral_cong_AE)
ultimately show "((λr. ∫x. f r x ∂M) has_real_derivative ∫x. deriv (λr. f r x) r ∂M) (at r)"
by simp
qed
proposition interchange_deriv_LINT_set_general:
fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real" and A :: "'a set"
assumes A_msr: "A ∈ sets M" and
f_integ: "⋀r. r∈{a<..<b} ⟹ set_integrable M A (f r)" and
f_diff: "AE x∈A in M. (λr. f r x) differentiable_on {a<..<b}" and
Df_bound: "AE x∈A in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "set_integrable M A g"
shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
(∫x∈A. set_borel_measurable_extension M A (λx. deriv (λr. f r x) r) x ∂M)) (at r)"
proof -
let ?M_A = "restrict_space M A"
have "⋀r. r∈{a<..<b} ⟹ integrable ?M_A (f r)"
using A_msr f_integ set_integrable_restrict_space_iff by auto
moreover have "AE x in ?M_A. (λr. f r x) differentiable_on {a<..<b}"
using AE_restrict_space_iff A_msr f_diff by (metis sets.Int_space_eq2)
moreover have "AE x in ?M_A. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" and
"integrable ?M_A g"
using A_msr Df_bound set_integrable_restrict_space_iff
by (auto simp add: AE_restrict_space_iff)
ultimately have "⋀r. r∈{a<..<b} ⟹ ((λr. integral⇧L ?M_A (f r)) has_real_derivative
integral⇧L ?M_A (borel_measurable_extension ?M_A (λx. deriv (λr. f r x) r))) (at r)"
by (rule interchange_deriv_LINT_general[where M="restrict_space M A"]) auto
thus "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
(∫x∈A. set_borel_measurable_extension M A (λx. deriv (λr. f r x) r) x ∂M)) (at r)"
unfolding set_borel_measurable_extension_def using assms
by(simp add: set_lebesgue_integral_restrict_space)
qed
proposition interchange_deriv_LINT_set:
fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real" and A :: "'a set"
assumes [measurable]:"A ∈ sets M" and
"⋀r. r∈{a<..<b} ⟹ set_integrable M A (f r)" and
"AE x∈A in M. (λr. f r x) differentiable_on {a<..<b}" and
"⋀r. r∈{a<..<b} ⟹ set_borel_measurable M A (λx. (deriv (λr. f r x) r))" and
"AE x∈A in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "set_integrable M A g"
shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
(∫x∈A. deriv (λr. f r x) r ∂M)) (at r)"
proof -
fix r assume r_ab: "r∈{a<..<b}"
hence [simp]: "set_borel_measurable M A (λx. deriv (λs. f s x) r)"
using assms by simp
have [measurable]: "⋀h N L. h ∈ N →⇩M L ⟹ measurable_extension N L h ∈ N →⇩M L"
by(rule measurable_extension_measurable) auto
have "((λs. ∫x∈A. f s x ∂M) has_real_derivative
(∫x∈A. set_borel_measurable_extension M A (λy. deriv (λs. f s y) r) x ∂M)) (at r)"
using assms r_ab by (intro interchange_deriv_LINT_set_general; simp)
moreover have "(∫x∈A. deriv (λs. f s x) r ∂M) =
(∫x∈A. set_borel_measurable_extension M A (λy. deriv (λs. f s y) r) x ∂M)"
by(auto intro!: set_lebesgue_integral_cong_AE2 set_borel_measurable_measurable_extension_AE
set_borel_measurable_extension_measurable[where g="λy. deriv (λs. f s y) r"])
ultimately show
"((λr. ∫x∈A. f r x ∂M) has_real_derivative (∫x∈A. deriv (λr. f r x) r ∂M)) (at r)"
by simp
qed
section ‹Additional Lemmas for the ‹HOL-Probability› Library›
lemma (in finite_borel_measure)
fixes F :: "real ⇒ real"
assumes nondecF : "⋀ x y. x ≤ y ⟹ F x ≤ F y" and
right_cont_F : "⋀a. continuous (at_right a) F" and
lim_F_at_bot : "(F ⤏ 0) at_bot" and
lim_F_at_top : "(F ⤏ m) at_top" and
m : "0 ≤ m"
shows emeasure_interval_measure_Ioi: "emeasure (interval_measure F) {x<..} = m - F x"
and measure_interval_measure_Ioi: "measure (interval_measure F) {x<..} = m - F x"
proof -
interpret F_FM: finite_measure "interval_measure F"
using finite_borel_measure.axioms(1) finite_borel_measure_interval_measure lim_F_at_bot
lim_F_at_top m nondecF right_cont_F by blast
have "UNIV = {..x} ∪ {x<..}" by auto
moreover have "{..x} ∩ {x<..} = {}" by auto
ultimately have "emeasure (interval_measure F) UNIV =
emeasure (interval_measure F) {..x} + emeasure (interval_measure F) {x<..}"
by (simp add: plus_emeasure)
moreover have "emeasure (interval_measure F) UNIV = m"
using assms interval_measure_UNIV by presburger
ultimately show ⋆: "emeasure (interval_measure F) {x<..} = m - F x"
using assms emeasure_interval_measure_Iic
by (metis ennreal_add_diff_cancel_left ennreal_minus measure_interval_measure_Iic
measure_nonneg top_neq_ennreal)
hence "ennreal (measure (interval_measure F) {x<..}) = m - F x"
using emeasure_eq_measure by (metis emeasure_eq_ennreal_measure top_neq_ennreal)
moreover have "⋀x. F x ≤ m"
using lim_F_at_top nondecF by (intro mono_at_top_le[where f=F]; simp add: mono_def)
ultimately show "measure (interval_measure F) {x<..} = m - F x"
using ennreal_inj F_FM.emeasure_eq_measure by force
qed
lemma (in prob_space) cond_prob_nonneg[simp]: "cond_prob M P Q ≥ 0"
by (auto simp: cond_prob_def)
lemma (in prob_space) cond_prob_whole_1: "cond_prob M P P = 1" if "prob {ω ∈ space M. P ω} ≠ 0"
unfolding cond_prob_def using that by simp
lemma (in prob_space) cond_prob_0_null: "cond_prob M P Q = 0" if "prob {ω ∈ space M. Q ω} = 0"
unfolding cond_prob_def using that by simp
lemma (in prob_space) cond_prob_AE_prob:
assumes "{ω ∈ space M. P ω} ∈ events" "{ω ∈ space M. Q ω} ∈ events"
and "AE ω in M. Q ω"
shows "cond_prob M P Q = prob {ω ∈ space M. P ω}"
proof -
let ?setP = "{ω ∈ space M. P ω}"
let ?setQ = "{ω ∈ space M. Q ω}"
have [simp]: "prob ?setQ = 1" using assms prob_Collect_eq_1 by simp
hence "cond_prob M P Q = prob (?setP ∩ ?setQ)"
unfolding cond_prob_def by (simp add: Collect_conj_eq2)
also have "… = prob ?setP"
proof (rule antisym)
show "prob (?setP ∩ ?setQ) ≤ prob ?setP"
using assms finite_measure_mono inf_sup_ord by blast
next
show "prob ?setP ≤ prob (?setP ∩ ?setQ)"
proof -
have "prob (?setP ∩ ?setQ) = prob ?setP + prob ?setQ - prob (?setP ∪ ?setQ)"
using assms by (smt (verit) finite_measure_Diff' finite_measure_Union' sup_commute)
also have "… = prob ?setP + (1 - prob (?setP ∪ ?setQ))" by simp
also have "… ≥ prob ?setP" by simp
finally show ?thesis .
qed
qed
finally show ?thesis .
qed
subsection ‹More Properties of ‹cdf›'s›
context finite_borel_measure
begin
lemma cdf_diff_eq2:
assumes "x ≤ y"
shows "cdf M y - cdf M x = measure M {x<..y}"
proof (cases ‹x = y›)
case True
thus ?thesis by force
next
case False
hence "x < y" using assms by simp
thus ?thesis by (rule cdf_diff_eq)
qed
end
context prob_space
begin
lemma cdf_distr_measurable [measurable]:
assumes [measurable]: "random_variable borel X"
shows "cdf (distr M borel X) ∈ borel_measurable borel"
by(auto intro!: cdf_distribution.measurable_C simp: cdf_distribution_def)
lemma cdf_distr_P:
assumes [measurable]:"random_variable borel X"
shows "cdf (distr M borel X) x = 𝒫(ω in M. X ω ≤ x)"
by(auto simp: measure_distr cdf_def intro!: arg_cong[where f=prob])
lemma cdf_continuous_distr_P_lt:
assumes [measurable]:"random_variable borel X" "isCont (cdf (distr M borel X)) x"
shows "cdf (distr M borel X) x = 𝒫(ω in M. X ω < x)"
proof -
have "𝒫(ω in M. X ω < x) = measure (distr M borel X) {..<x}"
by (auto simp: measure_distr intro!: arg_cong[where f=prob])
also have "… = measure (distr M borel X) ({..<x} ∪ {x})"
by(rule finite_measure.measure_zero_union[symmetric])
(use assms in
"auto intro!: finite_measure_distr finite_borel_measure.isCont_cdf[THEN iffD1]
real_distribution.finite_borel_measure_M")
also have "… = measure (distr M borel X) {..x}" by (metis ivl_disj_un_singleton(2))
also have "… = cdf (distr M borel X) x" unfolding cdf_def by simp
finally show ?thesis by simp
qed
lemma cdf_distr_diff_P:
assumes "x ≤ y"
and [measurable]:"random_variable borel X"
shows "cdf (distr M borel X) y - cdf (distr M borel X) x = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
have "cdf (distr M borel X) y - cdf (distr M borel X) x = measure (distr M borel X) {x<..y}"
by (rewrite distrX_FBM.cdf_diff_eq2; simp add: assms)
also have "… = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
by(auto simp: measure_distr intro!: arg_cong[where f=prob])
finally show ?thesis .
qed
lemma cdf_distr_max:
fixes c::real
assumes [measurable]: "random_variable borel X"
shows "cdf (distr M borel (λx. max (X x) c)) u = cdf (distr M borel X) u * indicator {c..} u"
proof (cases ‹c ≤ u›)
case True
thus ?thesis
by(auto simp: measure_distr cdf_def intro!: arg_cong[where f=prob])
next
case h:False
hence "(λx. max (X x) c) -` {..u} ∩ space M = {}"
by fastforce
thus ?thesis
using h by(auto simp: measure_distr cdf_def)
qed
lemma cdf_distr_min:
fixes c::real
assumes [measurable]: "random_variable borel X"
shows "cdf (distr M borel (λx. min (X x) c)) u =
1 - (1 - cdf (distr M borel X) u) * indicator {..<c} u"
proof (cases ‹c ≤ u›)
case h:True
hence *:"(λx. min (X x) c) -` {..u} ∩ space M = space M"
by fastforce
thus ?thesis
using h by(simp add: cdf_def measure_distr prob_space)
next
case h:False
then have "(λx. min (X x) c) -` {..u} ∩ space M = X -` {..u} ∩ space M"
by fastforce
thus ?thesis
using h by(simp add: cdf_def measure_distr)
qed
lemma cdf_distr_floor_P:
fixes X :: "'a ⇒ real"
assumes [measurable]: "random_variable borel X"
shows "cdf (distr M borel (λx. ⌊X x⌋)) u = 𝒫(x in M. X x < ⌊u⌋ + 1)"
using floor_le_iff le_floor_iff
by(auto simp: cdf_def measure_distr vimage_def intro!: arg_cong[where f=prob])
lemma expectation_nonneg_tail:
assumes [measurable]: "random_variable borel X"
and X_nonneg: "⋀x. x ∈ space M ⟹ X x ≥ 0"
defines "F u ≡ cdf (distr M borel X) u"
shows "(∫⇧+x. X x ∂M) = (∫⇧+u∈{0..}. 1 - F u ∂lborel)"
proof -
let ?distrX = "distr M borel X"
text ‹preparation›
have [simp]: "⋀u::real. u∈{0..} ⟹ ennreal u = (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel)"
by (auto simp: inf.commute simp flip: indicator_inter_arith)
have [simp]: "space M - X -` {..x} ∩ space M = X -` {x<..} ∩ space M" for x
by auto
have [measurable]: "Measurable.pred (borel ⨂⇩M borel) (λz::real×real. fst z ∈ {..< snd z})"
by auto
have [measurable]:"⋀v::real. Measurable.pred borel (λu. v ∈ {..<u})"
by simp
text ‹main part of the proof›
have "(∫⇧+x. X x ∂M) = (∫⇧+u. u ∂?distrX)"
by (simp add: nn_integral_distr)
also have "… = (∫⇧+u∈{0..}. u ∂?distrX)"
by (rule nn_integral_distr_set; simp add: X_nonneg)
also have "… = (∫⇧+u∈{0..}. (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel) ∂?distrX)"
by (rule set_nn_integral_cong; simp)
also have "… = (∫⇧+v∈{0..}. (∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) ∂lborel)"
proof -
have "(∫⇧+u∈{0..}. (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel) ∂?distrX) =
∫⇧+u. (∫⇧+v. indicator {..<u} v * indicator {0..} v * indicator {0..} u ∂lborel) ∂?distrX"
by (rewrite nn_integral_multc; simp)
also have "… =
∫⇧+v. (∫⇧+u. indicator {..<u} v * indicator {0..} v * indicator {0..} u ∂?distrX) ∂lborel"
by (auto intro!: pair_sigma_finite.Fubini' pair_sigma_finite.intro
simp: lborel.sigma_finite_measure_axioms prob_space_imp_sigma_finite[OF prob_space_distr])
also have "… = (∫⇧+v∈{0..}. (∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) ∂lborel)"
apply (rule nn_integral_cong)
apply (rewrite nn_integral_multc[THEN sym])
apply (rule borel_measurable_times_ennreal; measurable)
by (rule nn_integral_cong) (simp add: field_simps)
finally show ?thesis .
qed
also have "… = (∫⇧+v∈{0..}. 1 - F v ∂lborel)"
proof -
{ fix v::real assume "v ∈ {0..}"
hence "(∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) = (∫⇧+u. indicator {v<..} u ∂?distrX)"
unfolding indicator_def by (intro nn_integral_cong; simp)
also have "… = emeasure M (X -` {v<..} ∩ space M)"
apply (rewrite nn_integral_indicator, simp)
by (rewrite emeasure_distr; simp)
also have "… = 1 - F v"
unfolding F_def cdf_def
by (rewrite emeasure_eq_measure) (rewrite measure_distr; simp flip: prob_compl)
finally have "(∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) = 1 - F v" .}
thus ?thesis
by (intro set_nn_integral_cong; simp)
qed
finally show ?thesis .
qed
lemma expectation_nonpos_tail:
assumes [measurable]: "random_variable borel X"
and X_nonpos: "⋀x. x ∈ space M ⟹ X x ≤ 0"
defines "F u ≡ cdf (distr M borel X) u"
shows "(∫⇧+x. - X x ∂M) = (∫⇧+u∈{..<0}. F u ∂lborel)"
proof -
let ?distrX = "distr M borel X"
text ‹preparation›
have [simp]: "{..<0::real} ∩ {0..} = {}"
by force
have [simp]: "{..<0::real} ∪ {0..} = UNIV"
by force
have [simp]: "⋀u::real. u < 0 ⟹ - u = (∫⇧+v∈{..<0}. indicator {u..} v ∂lborel)"
by (rewrite indicator_inter_arith[THEN sym]; simp)
have [measurable]: "⋀v::real. Measurable.pred borel (λu. v ∈ {u..})"
by simp
text ‹main part of the proof›
have "(∫⇧+x. - X x ∂M) = (∫⇧+u. -u ∂?distrX)"
by (rewrite nn_integral_distr; simp)
also have "(∫⇧+u. -u ∂?distrX) = (∫⇧+u∈{..<0}. -u ∂?distrX) + (∫⇧+u∈{0..}. -u ∂?distrX)"
by (rewrite nn_integral_disjoint_pair[THEN sym]; simp)
also have "… = (∫⇧+u∈{..<0}. -u ∂?distrX)"
apply (rewrite nn_integral_zero'[of "λu. ennreal (-u) * indicator {0..} u"])
apply (rule AE_I2)
unfolding indicator_def using ennreal_lt_0 not_le by force+
also have "… = (∫⇧+u∈{..<0}. (∫⇧+v∈{..<0}. indicator {u..} v ∂lborel) ∂?distrX)"
by (rule set_nn_integral_cong; simp)
also have "… = (∫⇧+v∈{..<0}. (∫⇧+u∈{..<0}. indicator {u..} v ∂?distrX) ∂lborel)"
proof -
have "(∫⇧+u∈{..<0}. (∫⇧+v∈{..<0}. indicator {u..} v ∂lborel) ∂?distrX) =
∫⇧+u. (∫⇧+v. indicator {u..} v * indicator {..<0} v * indicator {..<0} u ∂lborel) ∂?distrX"
by (rewrite nn_integral_multc; simp)
also have "… =
∫⇧+v. (∫⇧+u. indicator {u..} v * indicator {..<0} v * indicator {..<0} u ∂?distrX) ∂lborel"
apply (rewrite pair_sigma_finite.Fubini')
apply (intro pair_sigma_finite.intro;
simp add: prob_space_distr prob_space_imp_sigma_finite sigma_finite_lborel)
using borel_measurable_times_ennreal by measurable simp_all
also have "… = (∫⇧+v∈{..<0}. (∫⇧+u∈{..<0}. indicator {u..} v ∂?distrX) ∂lborel)"
apply (rule nn_integral_cong)
apply (rewrite nn_integral_multc[THEN sym])
apply (rule borel_measurable_times_ennreal; measurable)
by (rule nn_integral_cong) (simp add: field_simps)
finally show ?thesis .
qed
also have "… = (∫⇧+v∈{..<0}. F v ∂lborel)"
proof -
{ fix v::real assume "v ∈ {..<0}"
hence "(∫⇧+u∈{..<0}. indicator {u..} v ∂?distrX) = (∫⇧+u. indicator {..v} u ∂?distrX)"
unfolding indicator_def apply (intro nn_integral_cong) by simp
also have "… = emeasure M (X -` {..v} ∩ space M)"
apply (rewrite nn_integral_indicator, simp)
by (rewrite emeasure_distr; simp)
also have "… = F v"
unfolding F_def cdf_def
by (rewrite emeasure_eq_measure) (rewrite measure_distr; simp)
finally have "(∫⇧+u∈{..<0}. indicator {u..} v ∂?distrX) = F v" . }
thus ?thesis
by (intro set_nn_integral_cong; simp)
qed
finally show ?thesis .
qed
proposition expectation_tail:
assumes [measurable]: "integrable M X"
defines "F u ≡ cdf (distr M borel X) u"
shows "expectation X = (LBINT u:{0..}. 1 - F u) - (LBINT u:{..<0}. F u)"
proof -
have "⋀x. X x = max (X x) 0 + min (X x) 0"
by simp
hence "expectation X = expectation (λx. max (X x) 0) + expectation (λx. min (X x) 0)"
using integrable_max integrable_min
by (rewrite Bochner_Integration.integral_add[THEN sym]; measurable)
also have "… = expectation (λx. max (X x) 0) - expectation (λx. - min (X x) 0)"
by force
moreover have "expectation (λx. max (X x) 0) = (LBINT u:{0..}. 1 - F u)"
proof -
have "expectation (λx. max (X x) 0) = enn2real (∫⇧+x. max (X x) 0 ∂M)"
by (rule integral_eq_nn_integral; simp)
also have "… = enn2real (∫⇧+u. (indicator {0..} u) * (1 - F u) ∂lborel)"
proof -
have "(∫⇧+u∈{0..}. 1 - cdf (distr M borel (λx. max (X x) 0)) u ∂lborel) =
∫⇧+u. (indicat_real {0..} u) * (1 - F u) ∂lborel"
apply (rule nn_integral_cong)
unfolding F_def indicator_def by (rewrite cdf_distr_max; simp)
thus ?thesis
by (rewrite expectation_nonneg_tail; simp)
qed
also have "… = (LBINT u:{0..}. 1 - F u)"
unfolding F_def set_lebesgue_integral_def using real_distribution.cdf_bounded_prob
by (rewrite integral_eq_nn_integral[THEN sym]; simp)
finally show ?thesis .
qed
moreover have "expectation (λx. - min (X x) 0) = (LBINT u:{..<0}. F u)"
proof -
have "expectation (λx. - min (X x) 0) = enn2real (∫⇧+x. - min (X x) 0 ∂M)"
by (rule integral_eq_nn_integral; simp)
also have "… = enn2real (∫⇧+u. (indicator {..<0} u) * F u ∂lborel)"
proof -
have "(∫⇧+u∈{..<0}. cdf (distr M borel (λx. min (X x) 0)) u ∂lborel) =
∫⇧+u. indicat_real {..<0} u * F u ∂lborel"
apply (rule nn_integral_cong)
unfolding F_def indicator_def by (rewrite cdf_distr_min; simp)
thus ?thesis
by (rewrite expectation_nonpos_tail; simp)
qed
also have "… = (LBINT u:{..<0}. F u)"
unfolding F_def set_lebesgue_integral_def
apply (rewrite integral_eq_nn_integral, measurable)
using cdf_def by simp_all
finally show ?thesis .
qed
ultimately show ?thesis
by simp
qed
proposition distributed_deriv_cdf:
assumes [measurable]: "random_variable borel X"
defines "F u ≡ cdf (distr M borel X) u"
assumes "countable S" "⋀x. x ∉ S ⟹ (F has_real_derivative f x) (at x)"
and "continuous_on UNIV F" "f ∈ borel_measurable lborel"
shows "distributed M lborel X f"
proof -
have FBM: "finite_borel_measure (distr M borel X)"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
then interpret distrX_FBM: finite_borel_measure "distr M borel X" .
have FBMl: "finite_borel_measure (distr M lborel X)" using FBM distr_borel_lborel by metis
then interpret distrlX_FBM: finite_borel_measure "distr M lborel X" .
have [simp]: "(λx. ennreal (f x)) ∈ borel_measurable borel" using assms by simp
moreover have "distr M lborel X = density lborel f"
proof -
have "⋀a b. a ≤ b ⟹ emeasure (distr M lborel X) {a<..b} < ⊤"
using distrlX_FBM.emeasure_real less_top_ennreal by blast
moreover have "⋀a b. a ≤ b ⟹
emeasure (distr M lborel X) {a<..b} = emeasure (density lborel f) {a<..b}"
proof -
fix a b :: real assume ab: "a ≤ b"
hence [simp]: "sym_diff {a<..b} {a..b} = {a}" by force
have "emeasure (density lborel f) {a<..b} = (∫⇧+x∈{a<..b}. ennreal (f x) ∂lborel)"
by (rewrite emeasure_density; simp)
also have "… = (∫⇧+x∈{a..b}. ennreal (f x) ∂lborel)"
by (rewrite nn_integral_null_delta, auto)
also have "… = ∫⇧+x. ennreal (indicat_real {a..b} x * f x) ∂lborel"
by (metis indicator_mult_ennreal mult.commute)
also have "… = ennreal (F b - F a)"
proof -
define g where "g x = (if x ∈ S then 0 else f x)" for x :: real
have "(∫⇧+x. ennreal (indicat_real {a..b} x * f x) ∂lborel)
= ∫⇧+x. ennreal (indicat_real {a..b} x * g x) ∂lborel"
apply (rule nn_integral_cong_AE)
apply (rule AE_mp[where P="λx. x ∉ S"])
using assms countable_imp_null_set_lborel AE_not_in apply blast
unfolding g_def by simp
also have "… = ennreal (F b - F a)"
proof -
have "⋀x. g x ≥ 0"
unfolding g_def if_split apply safe
using assms distrX_FBM.cdf_nondecreasing
by (intro mono_on_imp_deriv_nonneg[of UNIV F]; simp add: monoI)
moreover have "⋀x. x ∉ S ⟹ (F has_vector_derivative g x) (at x within {a..b})"
using assms has_real_derivative_iff_has_vector_derivative g_def
by (metis has_vector_derivative_at_within)
moreover have "continuous_on {a..b} F"
using assms continuous_on_subset by blast
ultimately show ?thesis
apply (rewrite nn_integral_has_integral_lebesgue, simp)
unfolding F_def
by (rule fundamental_theorem_of_calculus_strong[where S=S]) (auto simp add: ab assms)
qed
finally show ?thesis .
qed
also have "… = emeasure (distr M lborel X) {a <.. b}"
using ab
by (rewrite distrlX_FBM.emeasure_Ioc)
(auto simp: F_def cdf_def ennreal_minus[symmetric] distr_borel_lborel)
finally show "emeasure (distr M lborel X) {a<..b} = emeasure (density lborel f) {a<..b}"
by simp
qed
ultimately show ?thesis by (intro measure_eqI_Ioc; simp)
qed
ultimately show ?thesis unfolding distributed_def by auto
qed
end
text ‹
Define the conditional probability space.
This is obtained by rescaling the restricted space of a probability space.
›
subsection ‹Conditional Probability Space›
lemma restrict_prob_space:
assumes "measure_space Ω A μ" "a ∈ A"
and "0 < μ a" "μ a < ∞"
shows "prob_space (scale_measure (1 / μ a) (restrict_space (measure_of Ω A μ) a))"
proof
let ?M = "measure_of Ω A μ"
let ?Ma = "restrict_space ?M a"
let ?rMa = "scale_measure (1 / μ a) ?Ma"
have "emeasure ?rMa (space ?rMa) = 1 / μ a * emeasure ?Ma (space ?rMa)" by simp
also have "… = 1 / μ a * emeasure ?M (space ?rMa)"
using assms
by (rewrite emeasure_restrict_space;
simp add: measure_space_def sigma_algebra.sets_measure_of_eq
space_restrict_space space_scale_measure)
also have "… = 1 / μ a * emeasure ?M (space ?Ma)" by (rewrite space_scale_measure) simp
also have "… = 1 / μ a * emeasure ?M a"
using assms
by (rewrite space_restrict_space2) (auto simp add: measure_space_closed)
also have "… = 1"
using assms measure_space_def
by (rewrite emeasure_measure_of_sigma) (auto simp add: ennreal_divide_times)
finally show "emeasure ?rMa (space ?rMa) = 1" .
qed
definition cond_prob_space :: "'a measure ⇒ 'a set ⇒ 'a measure" (infix ‹⇂› 200)
where "M⇂A ≡ scale_measure (1 / emeasure M A) (restrict_space M A)"
context prob_space
begin
lemma cond_prob_space_whole[simp]: "M ⇂ space M = M"
unfolding cond_prob_space_def using emeasure_space_1 by simp
lemma cond_prob_space_correct:
assumes "A ∈ events" "prob A > 0"
shows "prob_space (M⇂A)"
using restrict_prob_space[OF measure_space[of M]] assms
by(auto simp: cond_prob_space_def emeasure_eq_measure measure_of_of_measure)
lemma space_cond_prob_space:
assumes "A ∈ events"
shows "space (M⇂A) = A"
unfolding cond_prob_space_def using assms by (simp add: space_scale_measure)
lemma sets_cond_prob_space: "sets (M⇂A) = (∩) A ` events"
unfolding cond_prob_space_def by (metis sets_restrict_space sets_scale_measure)
lemma measure_cond_prob_space:
assumes "A ∈ events" "B ∈ events"
and "prob A > 0"
shows "measure (M⇂A) (B ∩ A) = prob (B ∩ A) / prob A"
proof -
have "1 / emeasure M A = ennreal (1 / prob A)"
using assms by (smt (verit) divide_ennreal emeasure_eq_measure ennreal_1)
hence "measure (M⇂A) (B ∩ A) = (1 / prob A) * measure (restrict_space M A) (B ∩ A)"
unfolding cond_prob_space_def using measure_scale_measure by force
also have "… = (1 / prob A) * prob (B ∩ A)"
using measure_restrict_space assms by (metis inf.cobounded2 sets.Int_space_eq2)
also have "… = prob (B ∩ A) / prob A" by simp
finally show ?thesis .
qed
corollary measure_cond_prob_space_subset:
assumes "A ∈ events" "B ∈ events" "B ⊆ A"
and "prob A > 0"
shows "measure (M⇂A) B = prob B / prob A"
proof -
have "B = B ∩ A" using assms by auto
moreover have "measure (M⇂A) (B ∩ A) = prob (B ∩ A) / prob A"
using assms measure_cond_prob_space by simp
ultimately show ?thesis by auto
qed
lemma cond_cond_prob_space:
assumes [measurable]: "A ∈ events" "B ∈ events" "B ⊆ A" "prob B > 0"
shows "(M⇂A)⇂B = M⇂B"
proof (rule measure_eqI)
have pA_pos[simp]: "prob A > 0" using assms by (smt (verit, ccfv_SIG) finite_measure_mono)
interpret MA_PS: prob_space "M⇂A" using cond_prob_space_correct assms by simp
interpret MB_PS: prob_space "M⇂B" using cond_prob_space_correct assms by simp
have "1 / emeasure M A = ennreal (1 / prob A)"
using pA_pos by (smt (verit, ccfv_SIG) divide_ennreal emeasure_eq_measure ennreal_1)
hence [simp]: "0 < MA_PS.prob B"
using assms pA_pos
by (metis divide_eq_0_iff measure_cond_prob_space_subset zero_less_measure_iff)
have [simp]: "B ∈ MA_PS.events"
using assms by (rewrite sets_cond_prob_space) (auto simp: image_def)
have [simp]: "finite_measure ((M⇂A)⇂B)"
by (auto intro!: prob_space.finite_measure prob_space.cond_prob_space_correct
simp: prob_space_axioms)
show sets_MAB: "sets ((M⇂A)⇂B) = sets (M⇂B)"
apply (rewrite prob_space.sets_cond_prob_space)
using MA_PS.prob_space_axioms apply presburger
apply (rewrite sets_cond_prob_space, unfold image_def)+
using assms by blast
show "⋀C. C ∈ sets ((M⇂A)⇂B) ⟹ emeasure ((M⇂A)⇂B) C = emeasure (M⇂B) C"
proof -
fix C assume "C ∈ sets ((M⇂A)⇂B)"
hence "C ∈ sets (M⇂B)" using sets_MAB by simp
from this obtain D where "D ∈ events" "C = B ∩ D"
by (rewrite in asm sets_cond_prob_space, auto)
hence [simp]: "C ∈ events" and [simp]: "C ⊆ B" and [simp]: "C ⊆ A" using assms by auto
hence [simp]: "C ∈ MA_PS.events"
using assms by (rewrite sets_cond_prob_space, unfold image_def) blast
have "Sigma_Algebra.measure ((M⇂A)⇂B) C = MA_PS.prob C / MA_PS.prob B"
by (rewrite prob_space.measure_cond_prob_space_subset; simp add: MA_PS.prob_space_axioms)
also have "MA_PS.prob C = prob C / prob A"
by (simp add: measure_cond_prob_space_subset)
also have "MA_PS.prob B = prob B / prob A"
by (simp add: assms measure_cond_prob_space_subset)
finally have "Sigma_Algebra.measure ((M⇂A)⇂B) C = (prob C / prob A) / (prob B / prob A)" .
also have "… = prob C / prob B"
using pA_pos by (smt (verit) divide_divide_eq_right divide_mult_cancel)
also have "… = MB_PS.prob C"
by (rewrite prob_space.measure_cond_prob_space_subset; simp add: prob_space_axioms assms)
finally have "Sigma_Algebra.measure ((M ⇂ A) ⇂ B) C = MB_PS.prob C" .
thus "emeasure ((M⇂A)⇂B) C = emeasure (M⇂B) C"
by (rewrite finite_measure.emeasure_eq_measure, simp)+ simp
qed
qed
lemma cond_prob_space_prob:
assumes[measurable]: "Measurable.pred M P" "Measurable.pred M Q"
and "𝒫(x in M. Q x) > 0"
shows "measure (M ⇂ {x ∈ space M. Q x}) {x ∈ space M. P x ∧ Q x} = 𝒫(x in M. P x ¦ Q x)"
proof -
let ?SetP = "{x ∈ space M. P x}"
let ?SetQ = "{x ∈ space M. Q x}"
have "measure (M⇂?SetQ) {x ∈ space M. P x ∧ Q x} = measure (M⇂?SetQ) (?SetP ∩ ?SetQ)"
by (smt (verit, ccfv_SIG) Collect_cong Int_def mem_Collect_eq)
also have "… = prob (?SetP ∩ ?SetQ) / prob ?SetQ"
using assms by (rewrite measure_cond_prob_space) simp_all
also have "… = 𝒫(x in M. P x ¦ Q x)"
unfolding cond_prob_def assms by (smt (verit) Collect_cong Int_def mem_Collect_eq)
finally show ?thesis .
qed
lemma cond_prob_space_cond_prob:
assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
and "𝒫(x in M. Q x) > 0"
shows "𝒫(x in M. P x ¦ Q x) = 𝒫(x in (M ⇂ {x ∈ space M. Q x}). P x)"
proof -
let ?setQ = "{x ∈ space M. Q x}"
have "𝒫(x in M. P x ¦ Q x) = measure (M⇂?setQ) {x ∈ space M. P x ∧ Q x}"
using cond_prob_space_prob assms by simp
also have "… = 𝒫(x in (M⇂?setQ). P x)"
proof -
have "{x ∈ space M. P x ∧ Q x} = {x ∈ space (M⇂?setQ). P x}"
using space_cond_prob_space assms by force
thus ?thesis by simp
qed
finally show ?thesis .
qed
lemma cond_prob_neg:
assumes[measurable]: "Measurable.pred M P" "Measurable.pred M Q"
and "𝒫(x in M. Q x) > 0"
shows "𝒫(x in M. ¬ P x ¦ Q x) = 1 - 𝒫(x in M. P x ¦ Q x)"
proof -
let ?setP = "{x ∈ space M. P x}"
let ?setQ = "{x ∈ space M. Q x}"
interpret setQ_PS: prob_space "M⇂?setQ" using cond_prob_space_correct assms by simp
have [simp]: "{x ∈ space (M⇂?setQ). P x} ∈ setQ_PS.events"
proof -
have "{x ∈ space (M⇂?setQ). P x} = ?setQ ∩ ?setP" using space_cond_prob_space by force
thus ?thesis using sets_cond_prob_space by simp
qed
have "𝒫(x in M. ¬ P x ¦ Q x) = 𝒫(x in M⇂?setQ. ¬ P x)"
by (rewrite cond_prob_space_cond_prob; simp add: assms)
also have "… = 1 - 𝒫(x in M⇂?setQ. P x)" by (rewrite setQ_PS.prob_neg) (simp_all add: assms)
also have "… = 1 - 𝒫(x in M. P x ¦ Q x)"
by (rewrite cond_prob_space_cond_prob; simp add: assms)
finally show ?thesis .
qed
lemma random_variable_cond_prob_space:
fixes A :: "'a set"
assumes [measurable]: "random_variable borel X"
shows "X ∈ borel_measurable (M⇂A)"
by(auto intro!: measurable_restrict_space1 simp: cond_prob_space_def cong: measurable_cong_sets)
lemma AE_cond_prob_space_iff:
assumes "A ∈ events" "prob A > 0"
shows "(AE x in M⇂A. P x) ⟷ (AE x in M. x ∈ A ⟶ P x)"
unfolding cond_prob_space_def
apply (rewrite AE_scale_measure_iff)
using assms divide_ennreal emeasure_eq_measure ennreal_1
apply (simp add: ennreal_zero_less_divide)
by (rewrite AE_restrict_space_iff; simp add: assms)
lemma integral_cond_prob_space_nn:
assumes [measurable]:"A ∈ events" "prob A > 0"
and [measurable]: "random_variable borel X"
and nonneg: "AE x in M. x ∈ A ⟶ 0 ≤ X x"
shows "integral⇧L (M⇂A) X = expectation (λx. indicator A x * X x) / prob A"
proof -
have [measurable]: "X ∈ borel_measurable (M⇂A)"
by (rule random_variable_cond_prob_space; simp add: assms)
have [simp]: "AE x in (M⇂A). 0 ≤ X x"
by (rewrite AE_cond_prob_space_iff; simp add: assms)
have [measurable]: "random_variable borel (λx. indicat_real A x * X x)"
using borel_measurable_indicator assms by force
have [simp]: "AE x in M. 0 ≤ indicat_real A x * X x" using nonneg by fastforce
have "integral⇧L (M⇂A) X = enn2real (∫⇧+ x. ennreal (X x) ∂(M⇂A))"
by (rewrite integral_eq_nn_integral; simp)
also have "… = enn2real (1 / prob A * (∫⇧+ x. ennreal (X x) ∂(restrict_space M A)))"
using divide_ennreal assms
by(auto simp: nn_integral_scale_measure cond_prob_space_def measurable_restrict_space1
emeasure_eq_measure ennreal_1[symmetric] simp del: ennreal_1)
also have "… = enn2real (1 / prob A * (∫⇧+ x. ennreal (indicator A x * X x) ∂M))"
by (simp add: assms nn_integral_restrict_space nn_integral_set_ennreal mult.commute)
also have "… = integral⇧L M (λx. indicator A x * X x) / prob A"
by (simp add: divide_nonneg_pos enn2real_mult integral_eq_nn_integral)
finally show ?thesis by simp
qed
end
text ‹
Define the complementary cumulative distribution function, also known as tail distribution.
The theory presented below is a slight modification of the subsection "Properties of cdf's"
in the theory ‹Distribution_Functions›.
›
subsection ‹Complementary Cumulative Distribution Function›
definition ccdf :: "real measure ⇒ real ⇒ real"
where "ccdf M ≡ λx. measure M {x<..}"
lemma ccdf_def2: "ccdf M x = measure M {x<..}"
by (simp add: ccdf_def)
context finite_borel_measure
begin
lemma add_cdf_ccdf: "cdf M x + ccdf M x = measure M (space M)"
proof -
have "{..x} ∪ {x<..} = UNIV" by auto
moreover have "{..x} ∩ {x<..} = {}" by auto
ultimately have "emeasure M {..x} + emeasure M {x<..} = emeasure M UNIV"
using plus_emeasure M_is_borel atMost_borel greaterThan_borel by metis
hence "measure M {..x} + measure M {x<..} = measure M UNIV"
using finite_emeasure_space emeasure_eq_measure ennreal_inj
by (metis measure_def enn2real_plus ennreal_less_top)
thus ?thesis unfolding cdf_def ccdf_def using borel_UNIV by simp
qed
lemma ccdf_cdf: "ccdf M = (λx. measure M (space M) - cdf M x)"
by (rule ext) (smt (verit) add_cdf_ccdf)
lemma cdf_ccdf: "cdf M = (λx. measure M (space M) - ccdf M x)"
by (rule ext) (smt (verit) add_cdf_ccdf)
lemma isCont_cdf_ccdf: "isCont (cdf M) x ⟷ isCont (ccdf M) x"
proof
show "isCont (cdf M) x ⟹ isCont (ccdf M) x" by (rewrite ccdf_cdf) auto
next
show "isCont (ccdf M) x ⟹ isCont (cdf M) x" by (rewrite cdf_ccdf) auto
qed
lemma isCont_ccdf: "isCont (ccdf M) x ⟷ measure M {x} = 0"
using isCont_cdf_ccdf isCont_cdf by simp
lemma continuous_cdf_ccdf:
shows "continuous F (cdf M) ⟷ continuous F (ccdf M)"
(is "?LHS ⟷ ?RHS")
proof
assume ?LHS
thus ?RHS using continuous_diff continuous_const by (rewrite ccdf_cdf) blast
next
assume ?RHS
thus ?LHS using continuous_diff continuous_const by (rewrite cdf_ccdf) blast
qed
lemma has_real_derivative_cdf_ccdf:
"(cdf M has_real_derivative D) F ⟷ (ccdf M has_real_derivative -D) F"
proof
assume "(cdf M has_real_derivative D) F"
thus "(ccdf M has_real_derivative -D) F"
using ccdf_cdf DERIV_const Deriv.field_differentiable_diff by fastforce
next
assume "(ccdf M has_real_derivative -D) F"
thus "(cdf M has_real_derivative D) F"
using cdf_ccdf DERIV_const Deriv.field_differentiable_diff by fastforce
qed
lemma differentiable_cdf_ccdf: "(cdf M differentiable F) ⟷ (ccdf M differentiable F)"
by (metis differentiable_def has_real_derivative_cdf_ccdf has_real_derivative_iff
minus_equation_iff)
lemma deriv_cdf_ccdf:
assumes "cdf M differentiable at x"
shows "deriv (cdf M) x = - deriv (ccdf M) x"
using has_real_derivative_cdf_ccdf differentiable_cdf_ccdf assms
by (simp add: DERIV_deriv_iff_real_differentiable DERIV_imp_deriv)
lemma ccdf_diff_eq2:
assumes "x ≤ y"
shows "ccdf M x - ccdf M y = measure M {x<..y}"
proof -
have "ccdf M x - ccdf M y = cdf M y - cdf M x"
using add_cdf_ccdf by (metis add_diff_cancel_left add_diff_cancel_right)
also have "… = measure M {x<..y}" using cdf_diff_eq2 assms by simp
finally show ?thesis .
qed
lemma ccdf_nonincreasing: "x ≤ y ⟹ ccdf M x ≥ ccdf M y"
using ccdf_cdf cdf_nondecreasing by auto
lemma ccdf_nonneg: "ccdf M x ≥ 0"
by (simp add: ccdf_def)
lemma ccdf_bounded: "ccdf M x ≤ measure M (space M)"
by (simp add: ccdf_def bounded_measure)
lemma ccdf_lim_at_top: "(ccdf M ⤏ 0) at_top"
proof -
have "((λx. measure M (space M) - cdf M x) ⤏ measure M (space M) - measure M (space M)) at_top"
by (intro tendsto_intros cdf_lim_at_top)
thus ?thesis
by (rewrite ccdf_cdf) simp
qed
lemma ccdf_lim_at_bot: "(ccdf M ⤏ measure M (space M)) at_bot"
proof -
have "((λx. measure M (space M) - cdf M x) ⤏ measure M (space M) - 0) at_bot"
by (intro tendsto_intros cdf_lim_at_bot)
thus ?thesis
by (rewrite ccdf_cdf) simp
qed
lemma ccdf_is_right_cont: "continuous (at_right a) (ccdf M)"
proof -
have "continuous (at_right a) (λx. measure M (space M) - cdf M x)"
by (intro continuous_intros cdf_is_right_cont)
thus ?thesis by (rewrite ccdf_cdf) simp
qed
end
context prob_space
begin
lemma ccdf_distr_measurable [measurable]:
assumes [measurable]: "random_variable borel X"
shows "ccdf (distr M borel X) ∈ borel_measurable borel"
using real_distribution.finite_borel_measure_M by (rewrite finite_borel_measure.ccdf_cdf; simp)
lemma ccdf_distr_P:
assumes [measurable]:"random_variable borel X"
shows "ccdf (distr M borel X) x = 𝒫(ω in M. X ω > x)"
by(auto simp: measure_distr ccdf_def intro!: arg_cong[where f=prob])
lemma ccdf_continuous_distr_P_ge:
assumes "random_variable borel X" "isCont (ccdf (distr M borel X)) x"
shows "ccdf (distr M borel X) x = 𝒫(ω in M. X ω ≥ x)"
proof -
have "ccdf (distr M borel X) x = measure (distr M borel X) {x<..}"
unfolding ccdf_def by simp
moreover have "Sigma_Algebra.measure (distr M borel X) {x} = 0"
using finite_borel_measure.isCont_ccdf real_distribution.finite_borel_measure_M assms by blast
ultimately have "ccdf (distr M borel X) x = measure (distr M borel X) ({x<..} ∪ {x})"
by (rewrite finite_measure.measure_zero_union; simp add: assms finite_measure_distr)
also have "… = measure (distr M borel X) {x..}"
by (metis Un_commute ivl_disj_un_singleton(1))
also have "… = 𝒫(ω in M. X ω ≥ x)"
apply (rewrite measure_distr, (simp_all add: assms)[2])
unfolding vimage_def by simp (smt (verit) Collect_cong Int_def mem_Collect_eq)
finally show ?thesis .
qed
lemma ccdf_distr_diff_P:
assumes "x ≤ y"
and [measurable]:"random_variable borel X"
shows "ccdf (distr M borel X) x - ccdf (distr M borel X) y = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
have "ccdf (distr M borel X) x - ccdf (distr M borel X) y = measure (distr M borel X) {x<..y}"
by (rewrite distrX_FBM.ccdf_diff_eq2; simp add: assms)
also have "… = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
by(auto simp: measure_distr intro!: arg_cong[where f=prob])
finally show ?thesis .
qed
end
context real_distribution
begin
lemma ccdf_bounded_prob: "⋀x. ccdf M x ≤ 1"
by (subst prob_space[THEN sym], rule ccdf_bounded)
lemma ccdf_lim_at_bot_prob: "(ccdf M ⤏ 1) at_bot"
by (subst prob_space[THEN sym], rule ccdf_lim_at_bot)
end
text ‹Introduce the hazard rate. This notion will be used to define the force of mortality.›
subsection ‹Hazard Rate›
context prob_space
begin
definition hazard_rate :: "('a ⇒ real) ⇒ real ⇒ real"
where "hazard_rate X t ≡
Lim (at_right 0) (λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt)"
lemma hazard_rate_0_ccdf_0:
assumes [measurable]: "random_variable borel X"
and "ccdf (distr M borel X) t = 0"
shows "hazard_rate X t = 0"
proof -
have "⋀dt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) = 0"
unfolding cond_prob_def using ccdf_distr_P assms by simp
hence "hazard_rate X t = Lim (at_right 0) (λdt::real. 0)"
unfolding hazard_rate_def by (rewrite Lim_cong; simp)
also have "… = 0" by (rule tendsto_Lim; simp)
finally show ?thesis .
qed
lemma hazard_rate_deriv_cdf:
assumes [measurable]: "random_variable borel X"
and "(cdf (distr M borel X)) differentiable at t"
shows "hazard_rate X t = deriv (cdf (distr M borel X)) t / ccdf (distr M borel X) t"
proof (cases ‹ccdf (distr M borel X) t = 0›)
case True
with hazard_rate_0_ccdf_0 show ?thesis by simp
next
case False
let ?F = "cdf (distr M borel X)"
have "⋀dt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) =
𝒫(x in M. t < X x ∧ X x ≤ t + dt) / 𝒫(x in M. t < X x)"
unfolding cond_prob_def by (metis (mono_tags, lifting) Collect_cong)
hence "∀⇩F dt in at_right 0. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt =
(?F (t + dt) - ?F t) / dt / ccdf (distr M borel X) t"
using cdf_distr_diff_P ccdf_distr_P by (intro eventually_at_rightI[where b=1]; simp)
moreover have "((λdt. (?F (t + dt) - ?F t) / dt) ⤏ deriv ?F t) (at_right 0)"
apply (rule Lim_at_imp_Lim_at_within)
using DERIV_deriv_iff_real_differentiable assms DERIV_def by blast
moreover have "((λdt. (?F (t + dt) - ?F t) / dt / ccdf (distr M borel X) t) ⤏
deriv ?F t / ccdf (distr M borel X) t) (at_right 0)"
proof -
have "((λdt. (?F (t + dt) - ?F t) / dt) ⤏ deriv ?F t) (at_right 0)"
apply (rule Lim_at_imp_Lim_at_within)
using DERIV_deriv_iff_real_differentiable assms DERIV_def by blast
thus ?thesis
by (rule tendsto_intros; simp add: False)
qed
ultimately show ?thesis
unfolding hazard_rate_def using tendsto_cong by (intro tendsto_Lim; fastforce)
qed
lemma deriv_cdf_hazard_rate:
assumes Xrv: "random_variable borel X"
and "(cdf (distr M borel X)) differentiable at t"
shows "deriv (cdf (distr M borel X)) t = ccdf (distr M borel X) t * hazard_rate X t"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
show ?thesis
proof (cases ‹ccdf (distr M borel X) t = 0›)
case True
hence "cdf (distr M borel X) t = 1"
using distrX_FBM.cdf_ccdf
by (metis Xrv diff_0_right prob_space.prob_space prob_space_distr)
moreover obtain D where "(cdf (distr M borel X) has_real_derivative D) (at t)"
using assms real_differentiable_def by blast
ultimately have "(cdf (distr M borel X) has_real_derivative 0) (at t)"
using assms
by (smt (verit) DERIV_local_max real_distribution.cdf_bounded_prob real_distribution_distr)
thus ?thesis using True by (simp add: DERIV_imp_deriv)
next
case False
thus ?thesis using hazard_rate_deriv_cdf assms by simp
qed
qed
lemma hazard_rate_deriv_ccdf:
assumes [measurable]: "random_variable borel X"
and "(ccdf (distr M borel X)) differentiable at t"
shows "hazard_rate X t = - deriv (ccdf (distr M borel X)) t / ccdf (distr M borel X) t"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
show ?thesis
using hazard_rate_deriv_cdf distrX_FBM.deriv_cdf_ccdf assms distrX_FBM.differentiable_cdf_ccdf
by presburger
qed
lemma deriv_ccdf_hazard_rate:
assumes [measurable]: "random_variable borel X"
and "(ccdf (distr M borel X)) differentiable at t"
shows "deriv (ccdf (distr M borel X)) t = - ccdf (distr M borel X) t * hazard_rate X t"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
show ?thesis
using deriv_cdf_hazard_rate distrX_FBM.deriv_cdf_ccdf assms distrX_FBM.differentiable_cdf_ccdf
by simp
qed
lemma hazard_rate_deriv_ln_ccdf:
assumes [measurable]: "random_variable borel X"
and "(ccdf (distr M borel X)) differentiable at t"
and "ccdf (distr M borel X) t ≠ 0"
shows "hazard_rate X t = - deriv (λt. ln (ccdf (distr M borel X) t)) t"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
let ?srvl = "ccdf (distr M borel X)"
have "?srvl t > 0" using distrX_FBM.ccdf_nonneg assms
by (meson add_strict_increasing add_strict_increasing2 less_add_same_cancel1
linorder_neqE_linordered_idom)
moreover have "(?srvl has_real_derivative (deriv ?srvl t)) (at t)"
using DERIV_deriv_iff_real_differentiable assms by blast
ultimately have "((λt. ln (?srvl t)) has_real_derivative 1 / ?srvl t * deriv ?srvl t) (at t)"
by (rule derivative_intros)
hence "deriv (λt. ln (?srvl t)) t = deriv ?srvl t / ?srvl t" by (simp add: DERIV_imp_deriv)
also have "… = - hazard_rate X t" using hazard_rate_deriv_ccdf assms by simp
finally show ?thesis by simp
qed
lemma hazard_rate_has_integral:
assumes [measurable]: "random_variable borel X"
and "t ≤ u"
and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
and "continuous_on {t..u} (ccdf (distr M borel X))"
and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
shows
"(hazard_rate X has_integral ln (ccdf (distr M borel X) t / ccdf (distr M borel X) u)) {t..u}"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
let ?srvl = "ccdf (distr M borel X)"
have [simp]: "⋀s. t ≤ s ∧ s ≤ u ⟹ ?srvl s > 0"
using distrX_FBM.ccdf_nonneg assms by (smt (verit) atLeastAtMost_iff)
from assms obtain S0 where S0_fin: "finite S0" and
diff_S0: "⋀s. s ∈ {t<..<u} - S0 ⟹ ?srvl differentiable at s within {t<..<u}"
unfolding piecewise_differentiable_on_def by blast
obtain S where
S_fin: "finite S" and diff_S: "⋀s. s ∈ {t..u} - S ⟹ ?srvl differentiable at s"
proof (atomize_elim)
let ?S = "S0 ∪ {t, u}"
have "finite ?S" using S0_fin by simp
moreover have "∀s. s ∈ {t..u} - ?S ⟶ ?srvl differentiable at s"
proof -
{ fix s assume s_in: "s ∈ {t..u} - ?S"
hence "?srvl differentiable at s within {t<..<u}" using diff_S0 by simp
hence "?srvl differentiable at s"
using s_in by (rewrite at_within_open[THEN sym]; simp) }
thus ?thesis by blast
qed
ultimately show "∃S. finite S ∧ (∀s. s ∈ {t..u} - S ⟶ ?srvl differentiable at s)"
by blast
qed
hence ln_srvl_diff: "⋀s. s ∈ {t..u} - S ⟹ (λr. ln (?srvl r)) differentiable at s"
apply (rewrite differentiable_eq_field_differentiable_real)
using assms differentiable_eq_field_differentiable_real
by (intro field_differentiable_at_ln_comp; simp)
have "(deriv (λs. - ln (?srvl s)) has_integral - ln (?srvl u) - - ln (?srvl t)) {t..u}"
proof -
have C0: "continuous_on {t..u} (λs. - ln (?srvl s))"
by (intro continuous_intros continuous_on_ln) (auto simp add: assms)
moreover have "(λs. - ln (?srvl s)) piecewise_differentiable_on {t<..<u}"
proof -
have "⋀r. r ∈ {t<..<u} - S ⟹ (λs. - ln (?srvl s)) differentiable at r within {t<..<u}"
using ln_srvl_diff by (intro derivative_intros; simp add: differentiable_at_withinI)
thus ?thesis
unfolding piecewise_differentiable_on_def apply safe
apply (rule continuous_on_subset[of "{t..u}"]; force simp add: C0)
using S_fin by blast
qed
ultimately show ?thesis
by (intro FTC_real_deriv_has_integral; simp add: assms)
qed
hence "(deriv (λs. - ln (?srvl s)) has_integral ln (?srvl t / ?srvl u)) {t..u}"
by (rewrite ln_div; force simp: assms)
moreover have "⋀r. r ∈ {t..u} - S ⟹ deriv (λs. - ln (?srvl s)) r = hazard_rate X r"
proof -
fix r assume r_in : "r ∈ {t..u} - S"
hence "ln differentiable at (?srvl r)"
using assms
by (smt (verit) DERIV_ln_divide Diff_iff distrX_FBM.ccdf_nonneg real_differentiable_def)
hence "deriv (λs. - ln (?srvl s)) r = - deriv (λs. ln (?srvl s)) r"
using ln_srvl_diff r_in differentiable_eq_field_differentiable_real deriv_minus by simp
thus "deriv (λs. - ln (?srvl s)) r = hazard_rate X r"
using assms r_in diff_S by (rewrite hazard_rate_deriv_ln_ccdf; simp)
qed
ultimately show "((hazard_rate X) has_integral ln (?srvl t / ?srvl u)) {t..u}"
by (rewrite has_integral_spike_finite_eq [of S _ "deriv (λs. - ln (?srvl s))"]; simp add: S_fin)
qed
corollary hazard_rate_integrable:
assumes [measurable]: "random_variable borel X"
and "t ≤ u"
and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
and "continuous_on {t..u} (ccdf (distr M borel X))"
and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
shows "hazard_rate X integrable_on {t..u}"
using has_integral_integrable hazard_rate_has_integral assms by blast
lemma ccdf_exp_cumulative_hazard:
assumes [measurable]: "random_variable borel X"
and "t ≤ u"
and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
and "continuous_on {t..u} (ccdf (distr M borel X))"
and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
shows "ccdf (distr M borel X) u / ccdf (distr M borel X) t =
exp (- integral {t..u} (hazard_rate X))"
proof -
interpret distrX_FBM: finite_borel_measure "distr M borel X"
using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
let ?srvl = "ccdf (distr M borel X)"
have [simp]: "⋀s. t ≤ s ∧ s ≤ u ⟹ ?srvl s > 0"
using distrX_FBM.ccdf_nonneg assms
by (metis atLeastAtMost_iff less_eq_real_def)
have "integral {t..u} (hazard_rate X) = ln (?srvl t / ?srvl u)"
using hazard_rate_has_integral has_integral_integrable_integral assms by auto
also have "… = - ln (?srvl u / ?srvl t)" using ln_div assms by simp
finally have "- integral {t..u} (hazard_rate X) = ln (?srvl u / ?srvl t)" by simp
thus ?thesis using assms by simp
qed
lemma hazard_rate_density_ccdf:
assumes "distributed M lborel X f"
and "⋀s. f s ≥ 0" "t < u" "continuous_on {t..u} f"
shows "hazard_rate X t = f t / ccdf (distr M borel X) t"
proof (cases ‹ccdf (distr M borel X) t = 0›)
case True
thus ?thesis
using assms
by (rewrite hazard_rate_0_ccdf_0)
(auto dest: distributed_measurable)
next
case False
have [simp]: "t ≤ u" using assms by simp
have [measurable]: "random_variable borel X"
using assms distributed_measurable measurable_lborel1 by blast
have [measurable]: "f ∈ borel_measurable lborel"
using assms distributed_real_measurable by metis
have [simp]: "integrable lborel f"
proof -
have "prob (X -` UNIV ∩ space M) = LINT x|lborel. indicat_real UNIV x * f x"
by (rule distributed_measure; simp add: assms)
thus ?thesis
using prob_space not_integrable_integral_eq by fastforce
qed
have "((λdt. (LBINT s:{t..t+dt}. f s) / dt) ⤏ f t) (at_right 0)"
proof -
have "⋀dt. (∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) < ∞"
proof -
fix dt :: real
have "(∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) =
set_nn_integral lborel {t..t+dt} f"
by (metis indicator_mult_ennreal mult.commute)
moreover have "emeasure M (X -` {t..t+dt} ∩ space M) = set_nn_integral lborel {t..t+dt} f"
by (rule distributed_emeasure; simp add: assms)
moreover have "emeasure M (X -` {t..t+dt} ∩ space M) < ∞"
using emeasure_eq_measure ennreal_less_top infinity_ennreal_def by presburger
ultimately show "(∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) < ∞" by simp
qed
hence "⋀dt. (LBINT s:{t..t+dt}. f s) = integral {t..t+dt} f"
by (auto intro!: set_borel_integral_eq_integral integrableI_nonneg
simp: set_integrable_def assms)
moreover have "((λdt. (integral {t..t+dt} f) / dt) ⤏ f t) (at_right 0)"
proof -
have "((λx. integral {t..x} f) has_real_derivative f t) (at t within {t..u})"
by (rule integral_has_real_derivative; simp add: assms)
moreover have "(at t within {t..u}) = (at (t+0) within (+)t ` {0..u-t})" by simp
ultimately have
"((λx. integral {t..x} f) ∘ (+)t has_real_derivative f t) (at 0 within {0..u-t})"
by (metis DERIV_at_within_shift_lemma)
hence "((λdt. (integral {t..t+dt} f) / dt) ⤏ f t) (at 0 within {0..u-t})"
using has_field_derivative_iff by force
thus ?thesis using at_within_Icc_at_right assms
by (metis (lifting) diff_gt_0_iff_gt)
qed
ultimately show ?thesis by simp
qed
moreover have "⋀dt. dt > 0 ⟹ 𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t..t+dt}. f s)"
proof -
fix dt :: real assume "dt > 0"
hence [simp]: "sym_diff {t<..t + dt} {t..t + dt} = {t}" by force
have "(∫s. indicator {t<..t+dt} s * f s ∂lborel) = prob (X -` {t<..t+dt} ∩ space M)"
by (rule distributed_measure[THEN sym]; simp add: assms)
hence "𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t<..t+dt}. f s)"
by(auto intro!: arg_cong[where f=prob] simp: set_lebesgue_integral_def)
moreover have "(LBINT s:{t<..t+dt}. f s) = (LBINT s:{t..t+dt}. f s)"
by (rule set_integral_null_delta; force)
ultimately show "𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t..t+dt}. f s)" by simp
qed
ultimately have "((λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt) / dt) ⤏ f t) (at_right 0)"
by (auto intro!: Lim_cong_within
[where f="λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt) / dt"
and g="λdt. (LBINT s:{t..t+dt}. f s) / dt",THEN iffD2])
hence "((λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt) ⤏
f t / ccdf (distr M borel X) t) (at_right 0)"
unfolding cond_prob_def apply (rewrite ccdf_distr_P[THEN sym], simp)
unfolding conj.assoc divide_divide_eq_left
apply (rewrite mult.commute, rewrite divide_divide_eq_left[THEN sym])
apply(rule tendsto_intros)
by (auto intro!: Lim_cong_within
[where f="λx. prob {ω ∈ space M. t < X ω ∧ X ω ≤ t + x ∧ t < X ω} / x"
and g="λdt. prob {x ∈ space M. t < X x ∧ X x ≤ t + dt} / dt", THEN iffD2]
arg_cong[where f=prob] False)
thus ?thesis unfolding hazard_rate_def by (intro tendsto_Lim; simp)
qed
end
end