theory Preliminaries imports "HOL-Library.Rewrite" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Extended_Real" "HOL-Probability.Probability" begin 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 lemma Ico_nat_disjoint: "disjoint_family (λn::nat. {real n ..< real n + 1})" proof - { fix m n :: nat assume "{real m ..< real m + 1} ∩ {real n ..< real n + 1} ≠ {}" then obtain x::real where "x ∈ {real m ..< real m + 1} ∩ {real n ..< real n + 1}" by force hence "m = n" by simp } thus ?thesis unfolding disjoint_family_on_def by blast qed lemma Ico_nat_union: "(⋃n::nat. {real n ..< real n + 1}) = {0..}" proof show "(⋃n::nat. {real n ..< real n + 1}) ⊆ {0..}" by auto next show "{0..} ⊆ (⋃n::nat. {real n ..< real n + 1})" proof fix x::real assume "x ∈ {0..}" hence "nat ⌊x⌋ ≤ x ∧ x < nat ⌊x⌋ + 1" by (metis add_le_same_cancel1 atLeast_iff le_nat_floor less_one linorder_not_le of_nat_floor) thus "x ∈ (⋃n::nat. {real n ..< real n + 1})" unfolding atLeastLessThan_def by force qed qed 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 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 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 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 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 section ‹Additional Lemmas for the "Analysis" Library› 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 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 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 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 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 (* 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 *⇩_{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 "f ∈ borel_measurable lborel" and "S ∈ sets lborel" shows "set_integrable lborel S f ⟷ f absolutely_integrable_on S" unfolding set_integrable_def apply (simp, rewrite integrable_completion[THEN sym]) apply measurable using assms by simp_all 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" "f ∈ borel_measurable lborel" and "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" by (smt (verit, ccfv_threshold) AE_E3 Diff_iff UNIV_I space_borel space_lborel) 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 (rule AE_I'[of N], simp_all add: null, blast) 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" ― ‹Note that 0 = 0 holds when the integral diverges.› 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" ― ‹Note that 0 = 0 holds when the integral diverges.› 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 ‹Interchange of Differentiation and Lebesgue Integration› definition measurize :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where "measurize M N f = (SOME g. g ∈ M →⇩_{M}N ∧ (∃S∈(null_sets M). {x ∈ space M. f x ≠ g x} ⊆ S))" ― ‹The term "measurize" is what I coined in this formalization.› lemma fixes f g assumes "g ∈ M →⇩_{M}N" "S ∈ null_sets M" "{x ∈ space M. f x ≠ g x} ⊆ S" shows measurizeI: "AE x in M. f x = measurize M N f x" and measurizeI2: "AE x in M. g x = measurize M N f x" and measurize_measurable: "measurize M N f ∈ measurable M N" proof - let ?G = "λg. g ∈ M →⇩_{M}N" and ?S = "λg. ∃S∈null_sets M. {x ∈ space M. f x ≠ g x} ⊆ S" show "AE x in M. f x = measurize M N f x" unfolding measurize_def apply (rule someI2[of "λg. ?G g ∧ ?S g" g]) using assms apply blast using AE_I' by auto moreover have "AE x in M. g x = f x" using assms by (smt (verit, best) AE_I' Collect_cong) ultimately show "AE x in M. g x = measurize M N f x" by force show "measurize M N f ∈ measurable M N" unfolding measurize_def apply (rule conjE[of "?G g" "?S g"]) using assms apply auto[1] using someI_ex[of "λg. ?G g ∧ ?S g"] by auto qed corollary measurable_measurize_AE: fixes f assumes "f ∈ M →⇩_{M}N" shows "AE x in M. f x = measurize M N f x" by (rule measurizeI[where g=f and S="{}"]; simp add: assms) definition borel_measurize :: "'a measure ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b" where "borel_measurize M f = measurize M borel f" lemma fixes f g assumes "g ∈ borel_measurable M" "S ∈ null_sets M" "{x ∈ space M. f x ≠ g x} ⊆ S" shows borel_measurizeI: "AE x in M. f x = borel_measurize M f x" and borel_measurizeI2: "AE x in M. g x = borel_measurize M f x" and borel_measurize_measurable: "borel_measurize M f ∈ borel_measurable M" unfolding borel_measurize_def using assms apply - using measurizeI apply blast using measurizeI2 apply blast using measurize_measurable by blast corollary borel_measurable_measurize_AE: fixes f assumes "f ∈ borel_measurable M" shows "AE x in M. f x = borel_measurize M f x" using assms measurable_measurize_AE unfolding borel_measurize_def by auto definition set_borel_measurize :: "'a measure ⇒ 'a set ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b" where "set_borel_measurize M A f = borel_measurize (restrict_space M A) f" lemma fixes f g :: "'a ⇒ 'b::real_normed_vector" and A assumes "A ∈ sets M" "set_borel_measurable M A g" "S ∈ null_sets M" "{x ∈ A. f x ≠ g x} ⊆ S" shows set_borel_measurizeI: "AE x∈A in M. f x = set_borel_measurize M A f x" and set_borel_measurizeI2: "AE x∈A in M. g x = set_borel_measurize M A f x" and set_borel_measurize_measurable: "set_borel_measurable M A (set_borel_measurize M A f)" proof - have "g ∈ borel_measurable (restrict_space M A)" using assms by (rewrite set_borel_measurable_restrict_space_iff; simp) moreover have "S ∩ A ∈ null_sets (restrict_space M A)" using assms null_sets_restrict_space by (metis Int_lower2 null_set_Int2) moreover have "{x ∈ space (restrict_space M A). f x ≠ g x} ⊆ S ∩ A" using assms by (rewrite space_restrict_space2; simp) ultimately show "AE x∈A in M. f x = set_borel_measurize M A f x" and "AE x∈A in M. g x = set_borel_measurize M A f x" and "set_borel_measurable M A (set_borel_measurize M A f)" unfolding set_borel_measurize_def using assms apply - apply (rewrite AE_restrict_space_iff[THEN sym], simp) apply (rule borel_measurizeI[of g _ "S ∩ A"]; simp) apply (rewrite AE_restrict_space_iff[THEN sym], simp) apply (rule borel_measurizeI2[of g _ "S ∩ A"]; simp) apply (rewrite set_borel_measurable_restrict_space_iff[THEN sym], simp) by (rule borel_measurize_measurable[of g _ "S ∩ A"]; simp) qed corollary set_borel_measurable_measurize_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_measurize M A f x" using set_borel_measurable_restrict_space_iff borel_measurable_measurize_AE AE_restrict_space_iff unfolding set_borel_measurize_def by (smt (verit) AE_cong sets.Int_space_eq2 assms) 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_measurize M (λx. deriv (λr. f r x) r) x ∂M) (at r)" proof - text ‹Preparation› have f_msr: "⋀r. r∈{a<..<b} ⟹ f r ∈ borel_measurable M" using f_integ by auto from 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 (smt (verit) AE_E3) 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 (smt (verit) AE_E3) 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: "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_measurize 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) hence fd_msr: "⋀n. (λx. (f (r + d (n+m)) x - f r x) / d (n+m)) ∈ borel_measurable M" using r_ab by (measurable; (intro f_msr)?; simp) hence limf_msr: "(λx. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))) ∈ borel_measurable M" by measurable moreover 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)" apply (rewrite in asm DERIV_deriv_iff_field_differentiable[THEN sym]) unfolding Df_def using r_ab x_CN by (simp add: DERIV_def) hence "(λi. (f (r + d i) x - f r x) / d i)