theory Preliminaries imports "HOL-Library.Rewrite" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Extended_Real" "HOL-Probability.Probability" begin declare [[show_types]] notation powr (infixr ".^" 80) section ‹Preliminary Lemmas› lemma Collect_conj_eq2: "{x ∈ A. P x ∧ Q x} = {x ∈ A. P x} ∩ {x ∈ A. Q x}" by blast 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}" proof { fix x assume "x ∈ {a..b} - {a..<b}" hence "x ∈ {b}" by force } thus "{a..b} - {a..<b} ⊆ {b}" by blast next show "{b} ⊆ {a..b} - {a..<b}" using assms by simp qed lemma Icc_minus_Ioc: fixes a b assumes "a ≤ b" shows "{a..b} - {a<..b} = {a}" proof { fix x assume "x ∈ {a..b} - {a<..b}" hence "x ∈ {a}" by force } thus "{a..b} - {a<..b} ⊆ {a}" by blast next show "{a} ⊆ {a..b} - {a<..b}" using assms by simp qed (* subsubsection ‹Intersection› in Set_Interval.thy *) 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 proof - { fix m n :: nat assume "{a + real m ..< a + real m + 1} ∩ {a + real n ..< a + real n + 1} ≠ {}" then obtain x::real where "x ∈ {a + real m ..< a + real m + 1} ∩ {a + real n ..< a + real n + 1}" by force hence "m = n" by simp } thus ?thesis unfolding disjoint_family_on_def by blast qed 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 inverse_powr: "(1/a).^b = a.^-b" if "a > 0" for a b :: real by (smt that powr_divide powr_minus_divide powr_one_eq_one) lemma powr_eq_one_iff_gen[simp]: "a.^x = 1 ⟷ x = 0" if "a > 0" "a ≠ 1" for a x :: real by (metis powr_eq_0_iff powr_inj powr_zero_eq_one that) lemma powr_less_cancel2: "0 < a ⟹ 0 < x ⟹ 0 < y ⟹ x.^a < y.^a ⟹ x < y" for a x y ::real proof - assume a_pos: "0 < a" and x_pos: "0 < x" and y_pos: "0 < y" show "x.^a < y.^a ⟹ x < y" proof (erule contrapos_pp) assume "¬ x < y" hence "x ≥ y" by fastforce hence "x.^a ≥ y.^a" proof (cases "x = y") case True thus ?thesis by simp next case False hence "x.^a > y.^a" using ‹x ≥ y› powr_less_mono2 a_pos y_pos by auto thus ?thesis by auto qed thus "¬ x.^a < y.^a" by fastforce qed qed 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) thus ?case apply (simp only: sum.lessThan_Suc) apply (subst distrib_left) apply (subst Suc.hyps) by (subst power2_diff, simp add: field_simps power2_eq_square) 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 (subst geometric_increasing_sum_aux[THEN sym], simp add: that) lemma Reals_UNIV[simp]: "ℝ = {x::real. True}" unfolding Reals_def by auto lemma Lim_cong: assumes "∀⇩_{F}x in F. f x = g x" shows "Lim F f = Lim F g" unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce 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) corollary mono_antimono: fixes f :: "'a::order ⇒ 'b::ordered_ab_group_add" shows "mono f ⟷ antimono (λr. - f r)" by (rule mono_on_antimono_on) 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 (unfold atomize_ball) { 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∈{a..}. f x ≤ l" apply - by (rule notnotD, rewrite Set.ball_simps) auto 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 "⋀x. 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 (unfold atomize_ball) { 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∈{..a}. f x ≥ l" apply - by (rule notnotD, rewrite Set.ball_simps) auto 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 (unfold atomize_ball) { 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∈{a..}. f x ≥ l" apply - by (rule notnotD, rewrite Set.ball_simps) auto 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 (unfold atomize_ball) { 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∈{..a}. f x ≤ l" apply - by (rule notnotD, rewrite Set.ball_simps) auto 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 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 continuous_mult_left continuous_cdivide assms by force 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_cong: assumes "eventually (λx. f x = g x) F" "f (Lim F (λx. x)) = g (Lim F (λx. x))" shows "continuous F f ⟷ continuous F g" unfolding continuous_def using assms filterlim_cong by force lemma continuous_at_within_cong: assumes "f x = g x" "eventually (λx. f x = g x) (at x within s)" shows "continuous (at x within s) f ⟷ continuous (at x within s) g" proof (cases ‹x ∈ closure (s - {x})›) case True thus ?thesis using assms apply (intro continuous_cong, simp) by (rewrite Lim_ident_at, simp add: at_within_eq_bot_iff)+ simp next case False hence "at x within s = bot" using not_trivial_limit_within by blast thus ?thesis by simp 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)" apply (rewrite field_class.field_divide_inverse)+ using DERIV_cmult_right_iff assms inverse_nonzero_iff_nonzero by blast 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 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 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 to DERIV_shift *) 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 a Linearly Ordered Type› 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" apply (rule integral_unique[THEN sym]) apply (rule has_integral_combine[of a c b], simp_all add: assms) using has_integral_integral assms by auto 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 g_C0: "continuous_on {a..b} ?g" using continuous_on_op_minus by simp have Dg_g': "⋀x. x∈{a..b} ⟹ (?g has_field_derivative ?g' x) (at x within {a..b})" by (auto intro!: derivative_eq_intros) show ?thesis using has_integral_substitution_general [of "{}" a b ?g a b f, simplified, OF assms g_C0 Dg_g', simplified] apply (simp add: has_integral_null_interval[OF assms(1), THEN integral_unique]) by (simp add: 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 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[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}" proof (rule fundamental_theorem_of_calculus[OF c_nneg]) fix x::real assume "x ∈ {0..c}" show "((λy. a.^y / ln a) has_vector_derivative a.^x) (at x within {0..c})" apply (insert has_real_derivative_powr2[OF a_pos, of x]) apply (drule DERIV_cdivide[where c = "ln a"], simp add: assms) apply (rule has_vector_derivative_within_subset[where S=UNIV and T="{0..c}"], auto) by (rule iffD1[OF has_real_derivative_iff_has_vector_derivative]) qed thus ?thesis using assms powr_zero_eq_one 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 (* Stronger Version of lemma integral_power *) 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 (* Analogue for lemma has_integral_integral_real *) 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"] unfolding set_integrable_def set_lebesgue_integral_def by simp (smt (verit, ccfv_SIG) has_integral_cong has_integral_restrict_UNIV indicator_times_eq_if) 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 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) thus ?thesis unfolding set_borel_measurable_def apply simp apply (rule measurable_discrete_difference [where X=T and f="λx. indicat_real (S - T) x * deriv f x"], simp_all) using fin uncountable_infinite apply blast by (simp add: indicator_diff) qed lemma borel_measurable_antimono: fixes f :: "real ⇒ real" shows "antimono f ⟹ f ∈ borel_measurable borel" using borel_measurable_mono by (smt (verit, del_insts) borel_measurable_uminus_eq monotone_on_def) 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", simplified] 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 (smt (verit, del_insts) Diff_iff eventually_ae_filter mem_Collect_eq subsetI) 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 apply (rewrite space_scale_measure, simp) using assms by (smt Collect_cong not_gr_zero) 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)" proof - { fix x assume "x ∈ space M" have "(x ∈ A ⟶ f x = g x) ⟶ f x * indicator A x = g x * indicator A x" by force } hence "AE x in M. (x ∈ A ⟶ f x = g x) ⟶ f x * indicator A x = g x * indicator A x" by (rule AE_I2) hence "AE x in M. f x * indicator A x = g x * indicator A x" using assms AE_mp by auto thus ?thesis by (rule nn_integral_cong_AE) 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)" proof - let ?fA = "λx. indicator A x *⇩_{R}f x" and ?gA = "λx. indicator A x *⇩_{R}g x" have "?fA ∈ borel_measurable M" "?gA ∈ borel_measurable M" using assms unfolding set_borel_measurable_def by simp_all moreover have "AE x ∈ A in M. ?fA x = ?gA x" using assms by simp ultimately have "(LINT x:A|M. ?fA x) = (LINT x:A|M. ?gA x)" by (intro set_lebesgue_integral_cong_AE; simp) moreover have "(LINT x:A|M. f x) = (LINT x:A|M. ?fA x)" "(LINT x:A|M. g x) = (LINT x:A|M. ?gA x)" unfolding set_lebesgue_integral_def by (metis indicator_scaleR_eq_if)+ ultimately show ?thesis by simp qed 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 {}) = {}" apply simp using assms unfolding disjoint_family_on_def by blast } 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 nn_integral_distr_set: assumes "T ∈ measurable M M'" and "f ∈ borel_measurable (distr M M' T)" and "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 "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))" proof - have [simp]: "sym_diff (space M') A = space M' - A" using assms by (metis Diff_mono sets.sets_into_space sup.orderE) show ?thesis apply (rule nn_integral_null_delta; simp add: assms) unfolding null_sets_def using assms apply (simp, rewrite emeasure_distr; simp) unfolding vimage_def using emeasure_empty by (smt (z3) Collect_empty_eq Diff_iff Int_def mem_Collect_eq) qed finally show ?thesis . qed (* Analogue for "measure_eqI_lessThan" in the "Lebesgue_Measure" Theory *) lemma measure_eqI_Ioc: fixes M N :: "real measure" assumes sets: "sets M = sets borel" "sets N = 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 "⋀x. x ∈ space N ⟹ f x ≥ 0" and "A ∈ sets N" shows "measure M (X -` A ∩ space M) = (∫x. indicator A x * f x ∂N)" proof - have [simp]: "(λx. indicat_real A x * f x) ∈ borel_measurable N" using assms apply (measurable; simp?) using distributed_real_measurable assms by force 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" apply (rewrite enn2real_nn_integral_eq_integral [where f="λx. ennreal (indicator A x * f x)", THEN sym]; (simp add: assms)?) using distributed_emeasure assms by (smt (verit) emeasure_finite indicator_mult_ennreal mult.commute nn_integral_cong top.not_eq_extremum) 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(1)) (* Set Integral Version of the Lebesgue's Dominated Convergence Theorem *) 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 (smt (verit) AE_I' DiffI N_null mem_Collect_eq subsetI) 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