# Theory Preliminaries

```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"
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"

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"

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)"

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
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])
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))"
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)"
ultimately show "continuous (at x within s) (λx. f (x+a))"
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];
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
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"
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"
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) ```