# Theory Preliminaries

```theory Preliminaries
imports "HOL-Library.Rewrite" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Extended_Real"
"HOL-Probability.Probability"
begin
declare [[show_types]]
notation powr (infixr ".^" 80)

section ‹Preliminary Lemmas›

lemma Collect_conj_eq2: "{x ∈ A. P x ∧ Q x} = {x ∈ A. P x} ∩ {x ∈ A. Q x}"
by blast

lemma vimage_compl_atMost:
fixes f :: "'a ⇒ 'b::linorder"
shows "-(f -` {..y}) = f -` {y<..}"
by fastforce

context linorder
begin

lemma Icc_minus_Ico:
fixes a b
assumes "a ≤ b"
shows  "{a..b} - {a..<b} = {b}"
proof
{ fix x assume "x ∈ {a..b} - {a..<b}"
hence "x ∈ {b}" by force }
thus "{a..b} - {a..<b} ⊆ {b}" by blast
next
show "{b} ⊆ {a..b} - {a..<b}" using assms by simp
qed

lemma Icc_minus_Ioc:
fixes a b
assumes "a ≤ b"
shows "{a..b} - {a<..b} = {a}"
proof
{ fix x assume "x ∈ {a..b} - {a<..b}"
hence "x ∈ {a}" by force }
thus "{a..b} - {a<..b} ⊆ {a}" by blast
next
show "{a} ⊆ {a..b} - {a<..b}" using assms by simp
qed

(* subsubsection ‹Intersection› in Set_Interval.thy *)
lemma Int_atLeastAtMost_Unbounded[simp]: "{a..} Int {..b} = {a..b}"
by auto

lemma Int_greaterThanAtMost_Unbounded[simp]: "{a<..} Int {..b} = {a<..b}"
by auto

lemma Int_atLeastLessThan_Unbounded[simp]: "{a..} Int {..<b} = {a..<b}"
by auto

lemma Int_greaterThanLessThan_Unbounded[simp]: "{a<..} Int {..<b} = {a<..<b}"
by auto

end

lemma Ico_real_nat_disjoint:
"disjoint_family (λn::nat. {a + real n ..< a + real n + 1})" for a::real
proof -
{ fix m n :: nat
assume "{a + real m ..< a + real m + 1} ∩ {a + real n ..< a + real n + 1} ≠ {}"
then obtain x::real
where "x ∈ {a + real m ..< a + real m + 1} ∩ {a + real n ..< a + real n + 1}" by force
hence "m = n" by simp }
thus ?thesis unfolding disjoint_family_on_def by blast
qed

corollary Ico_nat_disjoint: "disjoint_family (λn::nat. {real n ..< real n + 1})"
using Ico_real_nat_disjoint[of 0] by simp

lemma Ico_real_nat_union: "(⋃n::nat. {a + real n ..< a + real n + 1}) = {a..}" for a::real
proof
show "(⋃n::nat. {a + real n ..< a + real n + 1}) ⊆ {a..}" by auto
next
show "{a..} ⊆ (⋃n::nat. {a + real n ..< a + real n + 1})"
proof
fix x assume "x ∈ {a..}"
hence "a ≤ x" by simp
hence "nat ⌊x-a⌋ ≤ x-a ∧ x-a < nat ⌊x-a⌋ + 1" by linarith
hence "a + nat ⌊x-a⌋ ≤ x ∧ x < a + nat ⌊x-a⌋ + 1" by auto
thus "x ∈ (⋃n::nat. {a + real n ..< a + real n + 1})" by auto
qed
qed

corollary Ico_nat_union: "(⋃n::nat. {real n ..< real n + 1}) = {0..}"
using Ico_real_nat_union[of 0] by simp

lemma Ico_nat_union_finite: "(⋃(n::nat)<m. {real n ..< real n + 1}) = {0..<m}"
proof
show "(⋃(n::nat)<m. {real n ..< real n + 1}) ⊆ {0..<m}" by auto
next
show "{0..<m} ⊆ (⋃(n::nat)<m. {real n ..< real n + 1})"
proof
fix x::real
assume ⋆: "x ∈ {0..<m}"
hence "nat ⌊x⌋ < m" using of_nat_floor by fastforce
moreover with ⋆ have "nat ⌊x⌋ ≤ x ∧ x < nat ⌊x⌋ + 1"
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 LIM_zero_iff': "((λx. l - f x) ⤏ 0) F = (f ⤏ l) F"
for f :: "'a ⇒ 'b::real_normed_vector"
unfolding tendsto_iff dist_norm
by (rewrite minus_diff_eq[THEN sym], rewrite norm_minus_cancel) simp

lemma antimono_onI:
"(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r ≤ s ⟹ f r ≥ f s) ⟹ antimono_on A f"
by (rule monotone_onI)

lemma antimono_onD:
"⟦antimono_on A f; r ∈ A; s ∈ A; r ≤ s⟧ ⟹ f r ≥ f s"
by (rule monotone_onD)

lemma antimono_imp_mono_on: "antimono f ⟹ antimono_on A f"

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 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 has_real_derivative_at_split:
"(f has_real_derivative D) (at x) ⟷
(f has_real_derivative D) (at_left x) ∧ (f has_real_derivative D) (at_right x)"
proof -
have "at x = at x within ({..<x} ∪ {x<..})" by (simp add: at_eq_sup_left_right at_within_union)
thus "(f has_real_derivative D) (at x) ⟷
(f has_real_derivative D) (at_left x) ∧ (f has_real_derivative D) (at_right x)"
using Lim_within_Un has_field_derivative_iff by fastforce
qed

lemma DERIV_cmult_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. c * f x) has_field_derivative c * D) (at x within s)"
proof
assume "(f has_field_derivative D) (at x within s)"
thus  "((λx. c * f x) has_field_derivative c * D) (at x within s)" using DERIV_cmult by force
next
assume "((λx. c * f x) has_field_derivative c * D) (at x within s)"
hence "((λx. c * f x / c) has_field_derivative c * D / c) (at x within s)"
using DERIV_cdivide assms by blast
thus "(f has_field_derivative D) (at x within s)" by (simp add: assms field_simps)
qed

lemma DERIV_cmult_right_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. f x * c) has_field_derivative D * c) (at x within s)"
by (rewrite DERIV_cmult_iff[of c], simp_all add: assms mult_ac)

lemma DERIV_cdivide_iff:
assumes "c ≠ 0"
shows "(f has_field_derivative D) (at x within s) ⟷
((λx. f x / c) has_field_derivative D / c) (at x within s)"
apply (rewrite field_class.field_divide_inverse)+
using DERIV_cmult_right_iff assms inverse_nonzero_iff_nonzero by blast

lemma DERIV_ln_divide_chain:
fixes f :: "real ⇒ real"
assumes "f x > 0" and "(f has_real_derivative D) (at x within s)"
shows "((λx. ln (f x)) has_real_derivative (D / f x)) (at x within s)"
proof -
have "DERIV ln (f x) :> 1 / f x" using assms by (intro DERIV_ln_divide) blast
thus ?thesis using DERIV_chain2 assms by fastforce
qed

lemma inverse_fun_has_integral_ln:
fixes f :: "real ⇒ real" and f' :: "real ⇒ real"
assumes "a ≤ b" and
"⋀x. x∈{a..b} ⟹ f x > 0" and
"continuous_on {a..b} f" and
"⋀x. x∈{a<..<b} ⟹ (f has_real_derivative f' x) (at x)"
shows "((λx. f' x / f x) has_integral (ln (f b) - ln (f a))) {a..b}"
proof -
have "continuous_on {a..b} (λx. ln (f x))" using assms by (intro continuous_intros; force)
moreover have "⋀x. x∈{a<..<b} ⟹ ((λx. ln (f x)) has_vector_derivative f' x / f x) (at x)"
apply (rewrite has_real_derivative_iff_has_vector_derivative[THEN sym])
using assms by (intro DERIV_ln_divide_chain; simp)
ultimately show ?thesis using assms by (intro fundamental_theorem_of_calculus_interior; simp)
qed

lemma DERIV_fun_powr2:
fixes a::real
assumes a_pos: "a > 0"
and f: "DERIV f x :> r"
shows "DERIV (λx. a.^(f x)) x :> a.^(f x) * r * ln a"
proof -
let ?g = "(λx. a)"
have g: "DERIV ?g x :> 0" by simp
have pos: "?g x > 0" by (simp add: a_pos)
show ?thesis
using DERIV_powr[OF g pos f] a_pos by (auto simp add: field_simps)
qed

lemma has_real_derivative_powr2:
assumes a_pos: "a > 0"
shows "((λx. a.^x) has_real_derivative a.^x * ln a) (at x)"
proof -
let ?f = "(λx. x::real)"
have f: "DERIV ?f x :> 1" by simp
thus ?thesis using DERIV_fun_powr2[OF a_pos f] by simp
qed

(* corollary to DERIV_shift *)
lemma field_differentiable_shift:
"(f field_differentiable (at (x + z))) = ((λx. f (x + z)) field_differentiable (at x))"
unfolding field_differentiable_def using DERIV_shift by force

subsection ‹Lemmas on ‹indicator› for a Linearly Ordered Type›

lemma indicator_Icc_shift:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a..b} x = indicator {t+a..t+b} (t+x)"

lemma indicator_Icc_shift_inverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a-t..b-t} x = indicator {a..b} (t+x)"

lemma indicator_Ici_shift:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a..} x = indicator {t+a..} (t+x)"

lemma indicator_Ici_shift_inverse:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a-t..} x = indicator {a..} (t+x)"

lemma indicator_Iic_shift:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b} x = indicator {..t+b} (t+x)"

lemma indicator_Iic_shift_inverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b-t} x = indicator {..b} (t+x)"

lemma indicator_Icc_reverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {a..b} x = indicator {t-b..t-a} (t-x)"

lemma indicator_Icc_reverse_inverse:
fixes a b t x :: "'a::linordered_ab_group_add"
shows "indicator {t-b..t-a} x = indicator {a..b} (t-x)"

lemma indicator_Ici_reverse:
fixes a t x :: "'a::linordered_ab_group_add"
shows "indicator {a..} x = indicator {..t-a} (t-x)"

lemma indicator_Ici_reverse_inverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {t-b..} x = indicator {..b} (t-x)"

lemma indicator_Iic_reverse:
fixes b t x :: "'a::linordered_ab_group_add"
shows "indicator {..b} x = indicator {t-b..} (t-x)"

lemma indicator_Iic_reverse_inverse:
fixes a t x :: "'a::linordered_field"
shows "indicator {..t-a} x = indicator {a..} (t-x)"

lemma indicator_Icc_affine_pos:
fixes a b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {a..b} x = indicator {t+c*a..t+c*b} (t + c*x)"
unfolding indicator_def using assms by simp

lemma indicator_Icc_affine_pos_inverse:
fixes a b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {(a-t)/c..(b-t)/c} x = indicator {a..b} (t + c*x)"
using indicator_Icc_affine_pos[where a="(a-t)/c" and b="(b-t)/c" and c=c and t=t ] assms by simp

lemma indicator_Ici_affine_pos:
fixes a c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {a..} x = indicator {t+c*a..} (t + c*x)"
unfolding indicator_def using assms by simp

lemma indicator_Ici_affine_pos_inverse:
fixes a c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {(a-t)/c..} x = indicator {a..} (t + c*x)"
using indicator_Ici_affine_pos[where a="(a-t)/c" and c=c and t=t] assms by simp

lemma indicator_Iic_affine_pos:
fixes b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {..b} x = indicator {..t+c*b} (t + c*x)"
unfolding indicator_def using assms by simp

lemma indicator_Iic_affine_pos_inverse:
fixes b c t x :: "'a::linordered_field"
assumes "c > 0"
shows "indicator {..(b-t)/c} x = indicator {..b} (t + c*x)"
using indicator_Iic_affine_pos[where b="(b-t)/c" and c=c and t=t] assms by simp

lemma indicator_Icc_affine_neg:
fixes a b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {a..b} x = indicator {t+c*b..t+c*a} (t + c*x)"
unfolding indicator_def using assms by auto

lemma indicator_Icc_affine_neg_inverse:
fixes a b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {(b-t)/c..(a-t)/c} x = indicator {a..b} (t + c*x)"
using indicator_Icc_affine_neg[where a="(b-t)/c" and b="(a-t)/c" and c=c and t=t] assms by simp

lemma indicator_Ici_affine_neg:
fixes a c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {a..} x = indicator {..t+c*a} (t + c*x)"
unfolding indicator_def using assms by simp

lemma indicator_Ici_affine_neg_inverse:
fixes b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {(b-t)/c..} x = indicator {..b} (t + c*x)"
using indicator_Ici_affine_neg[where a="(b-t)/c" and c=c and t=t] assms by simp

lemma indicator_Iic_affine_neg:
fixes b c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {..b} x = indicator {t+c*b..} (t + c*x)"
unfolding indicator_def using assms by simp

lemma indicator_Iic_affine_neg_inverse:
fixes a c t x :: "'a::linordered_field"
assumes "c < 0"
shows "indicator {..(a-t)/c} x = indicator {a..} (t + c*x)"
using indicator_Iic_affine_neg[where b="(a-t)/c" and c=c and t=t] assms by simp

section ‹Additional Lemmas for the ‹HOL-Analysis› Library›

lemma differentiable_eq_field_differentiable_real:
fixes f :: "real ⇒ real"
shows "f differentiable F ⟷ f field_differentiable F"
unfolding field_differentiable_def differentiable_def has_real_derivative
using has_real_derivative_iff by presburger

lemma differentiable_on_eq_field_differentiable_real:
fixes f :: "real ⇒ real"
shows "f differentiable_on s ⟷ (∀x∈s. f field_differentiable (at x within s))"
unfolding differentiable_on_def using differentiable_eq_field_differentiable_real by simp

lemma differentiable_on_cong :
assumes "⋀x. x∈s ⟹ f x = g x" and "f differentiable_on s"
shows "g differentiable_on s"
proof -
{ fix x assume "x∈s"
hence "f differentiable at x within s" using assms unfolding differentiable_on_def by simp
from this obtain D where "(f has_derivative D) (at x within s)"
unfolding differentiable_def by blast
hence "(g has_derivative D) (at x within s)"
using has_derivative_transform assms ‹x∈s› by metis
hence "g differentiable at x within s" unfolding differentiable_def by blast }
hence "∀x∈s. g differentiable at x within s" by simp
thus ?thesis unfolding differentiable_on_def by simp
qed

lemma C1_differentiable_imp_deriv_continuous_on:
"f C1_differentiable_on S ⟹ continuous_on S (deriv f)"
using C1_differentiable_on_eq field_derivative_eq_vector_derivative by auto

lemma deriv_shift:
assumes "f field_differentiable at (x+a)"
shows "deriv f (x+a) = deriv (λs. f (x+s)) a"
proof -
have "(f has_field_derivative deriv f (x+a)) (at (x+a))"
using DERIV_deriv_iff_field_differentiable assms
by force
hence "((λs. f (x+s)) has_field_derivative deriv f (x+a)) (at a)"
using DERIV_at_within_shift has_field_derivative_at_within by blast
moreover have "((λs. f (x+s)) has_field_derivative deriv (λs. f (x+s)) a) (at a)"
using DERIV_imp_deriv calculation by fastforce
ultimately show ?thesis using DERIV_unique by force
qed

lemma piecewise_differentiable_on_cong:
assumes "f piecewise_differentiable_on i"
and "⋀x. x ∈ i ⟹ f x = g x"
shows "g piecewise_differentiable_on i"
proof -
have "continuous_on i g"
using continuous_on_cong_simp assms piecewise_differentiable_on_imp_continuous_on by force
moreover have "∃S. finite S ∧ (∀x ∈ i - S. g differentiable (at x within i))"
proof -
from assms piecewise_differentiable_on_def
obtain S where fin: "finite S" and "∀x ∈ i - S. f differentiable (at x within i)" by metis
hence "⋀x. x ∈ i - S ⟹ f differentiable (at x within i)" by simp
hence "⋀x. x ∈ i - S ⟹ g differentiable (at x within i)"
using has_derivative_transform assms by (metis DiffD1 differentiable_def)
with fin show ?thesis by blast
qed
ultimately show ?thesis unfolding piecewise_differentiable_on_def by simp
qed

lemma differentiable_piecewise:
assumes "continuous_on i f"
and "f differentiable_on i"
shows "f piecewise_differentiable_on i"
unfolding piecewise_differentiable_on_def using assms differentiable_onD by auto

lemma piecewise_differentiable_scaleR:
assumes "f piecewise_differentiable_on S"
shows "(λx. a *⇩R f x) piecewise_differentiable_on S"
proof -
from assms obtain T where fin: "finite T" "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
hence "⋀x. x ∈ S - T ⟹ (λx. a *⇩R f x) differentiable at x within S"
using differentiable_scaleR by simp
moreover have "continuous_on S (λx. a *⇩R f x)"
using assms continuous_on_scaleR continuous_on_const piecewise_differentiable_on_def by blast
ultimately show "(λx. a *⇩R f x) piecewise_differentiable_on S"
using fin piecewise_differentiable_on_def by blast
qed

lemma differentiable_on_piecewise_compose:
assumes "f piecewise_differentiable_on S"
and "g differentiable_on f ` S"
shows "g ∘ f piecewise_differentiable_on S"
proof -
from assms obtain T where fin: "finite T" "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
hence "⋀x. x ∈ S - T ⟹ g ∘ f differentiable at x within S"
by (meson DiffD1 assms differentiable_chain_within differentiable_onD image_eqI)
hence "∃T. finite T ∧ (∀x∈S-T. g ∘ f differentiable at x within S)" using fin by blast
moreover have "continuous_on S (g ∘ f)"
using assms continuous_on_compose differentiable_imp_continuous_on
unfolding piecewise_differentiable_on_def by blast
ultimately show ?thesis
unfolding piecewise_differentiable_on_def by force
qed

lemma MVT_order_free:
fixes r h :: real
defines "I ≡ {r..r+h} ∪ {r+h..r}"
assumes "continuous_on I f" and "f differentiable_on interior I"
obtains t where "t ∈ {0<..<1}" and "f (r+h) - f r = h * deriv f (r + t*h)"
proof -
consider (h_pos) "h > 0" | (h_0) "h = 0" | (h_neg) "h < 0" by force
thus ?thesis
proof cases
case h_pos
hence "r < r+h" "I = {r..r+h}" unfolding I_def by simp_all
moreover hence "interior I = {r<..<r+h}" by simp
moreover hence "⋀x. ⟦r < x; x < r+h⟧ ⟹ f differentiable (at x)"
using assms by (simp add: differentiable_on_eq_differentiable_at)
ultimately obtain z where "r < z ∧ z < r+h ∧ f (r+h) - f r = h * deriv f z"
using MVT assms by (smt (verit) DERIV_imp_deriv)
moreover hence "(z-r) / h ∈ {0<..<1}" by simp
moreover have "z = r + (z-r)/h * h" using h_pos by simp
ultimately show ?thesis using that by presburger
next
case h_0
have "1/2 ∈ {0::real<..<1}" by simp
moreover have "f (r+h) - f r = 0" using h_0 by simp
moreover have "h * deriv f (r + (1/2)*h) = 0" using h_0 by simp
ultimately show ?thesis using that by presburger
next case h_neg
hence "r+h < r" "I = {r+h..r}" unfolding I_def by simp_all
moreover hence "interior I = {r+h<..<r}" by simp
moreover hence "⋀x. ⟦r+h < x; x < r⟧ ⟹ f differentiable (at x)"
using assms by (simp add: differentiable_on_eq_differentiable_at)
ultimately obtain z where "r+h < z ∧ z < r ∧ f r - f (r+h) = -h * deriv f z"
using MVT assms by (smt (verit) DERIV_imp_deriv)
moreover hence "(z-r) / h ∈ {0<..<1}" by (simp add: neg_less_divide_eq)
moreover have "z = r + (z-r)/h * h" using h_neg by simp
ultimately show ?thesis using that mult_minus_left by fastforce
qed
qed

lemma integral_combine2:
fixes f :: "real ⇒ 'a::banach"
assumes "a ≤ c" "c ≤ b"
and "f integrable_on {a..c}" "f integrable_on {c..b}"
shows "integral {a..c} f + integral {c..b} f = integral {a..b} f"
apply (rule integral_unique[THEN sym])
apply (rule has_integral_combine[of a c b], simp_all add: assms)
using has_integral_integral assms by auto

lemma has_integral_null_interval: fixes a b :: real and f::"real ⇒ real" assumes "a ≥ b"
shows "(f has_integral 0) {a..b}"
using assms content_real_eq_0 by blast

lemma has_integral_interval_reverse: fixes f :: "real ⇒ real" and a b :: real
assumes "a ≤ b"
and "continuous_on {a..b} f"
shows "((λx. f (a+b-x)) has_integral (integral {a..b} f)) {a..b}"
proof -
let ?g = "λx. a + b - x"
let ?g' = "λx. -1"
have g_C0: "continuous_on {a..b} ?g" using continuous_on_op_minus by simp
have Dg_g': "⋀x. x∈{a..b} ⟹ (?g has_field_derivative ?g' x) (at x within {a..b})"
by (auto intro!: derivative_eq_intros)
show ?thesis
using has_integral_substitution_general
[of "{}" a b ?g a b f, simplified, OF assms g_C0 Dg_g', simplified]
apply (simp add: has_integral_null_interval[OF assms(1), THEN integral_unique])
qed

lemma FTC_real_deriv_has_integral:
fixes F :: "real ⇒ real"
assumes "a ≤ b"
and "F piecewise_differentiable_on {a<..<b}"
and "continuous_on {a..b} F"
shows "(deriv F has_integral F b - F a) {a..b}"
proof -
obtain S where fin: "finite S" and
diff: "⋀x. x ∈ {a<..<b} - S ⟹ F differentiable at x within {a<..<b} - S"
using assms unfolding piecewise_differentiable_on_def
by (meson Diff_subset differentiable_within_subset)
hence "⋀x. x ∈ {a<..<b} - S ⟹ (F has_real_derivative deriv F x) (at x)"
proof -
fix x assume x_in: "x ∈ {a<..<b} - S"
have "open ({a<..<b} - S)"
using fin finite_imp_closed by (metis open_Diff open_greaterThanLessThan)
hence "at x within {a<..<b} - S = at x" by (meson x_in at_within_open)
hence "F differentiable at x" using diff x_in by smt
thus "(F has_real_derivative deriv F x) (at x)"
using DERIV_deriv_iff_real_differentiable by simp
qed
thus ?thesis
by (intro fundamental_theorem_of_calculus_interior_strong[where S=S];
qed

lemma integrable_spike_cong:
assumes "negligible S" "⋀x. x ∈ T - S ⟹ g x = f x"
shows "f integrable_on T ⟷ g integrable_on T"
using integrable_spike assms by force

lemma has_integral_powr2_from_0:
fixes a c :: real
assumes a_pos: "a > 0" and a_neq_1: "a ≠ 1" and c_nneg: "c ≥ 0"
shows "((λx. a.^x) has_integral ((a.^c - 1) / (ln a))) {0..c}"
proof -
have "((λx. a.^x) has_integral ((a.^c)/(ln a) - (a.^0)/(ln a))) {0..c}"
proof (rule fundamental_theorem_of_calculus[OF c_nneg])
fix x::real
assume "x ∈ {0..c}"
show "((λy. a.^y / ln a) has_vector_derivative a.^x) (at x within {0..c})"
apply (insert has_real_derivative_powr2[OF a_pos, of x])
apply (drule DERIV_cdivide[where c = "ln a"], simp add: assms)
apply (rule has_vector_derivative_within_subset[where S=UNIV and T="{0..c}"], auto)
by (rule iffD1[OF has_real_derivative_iff_has_vector_derivative])
qed
thus ?thesis
using assms powr_zero_eq_one by (simp add: field_simps)
qed

lemma integrable_on_powr2_from_0:
fixes a c :: real
assumes a_pos: "a > 0" and a_neq_1: "a ≠ 1" and c_nneg: "c ≥ 0"
shows "(λx. a.^x) integrable_on {0..c}"
using has_integral_powr2_from_0[OF assms] unfolding integrable_on_def by blast

lemma integrable_on_powr2_from_0_general:
fixes a c :: real
assumes a_pos: "a > 0" and c_nneg: "c ≥ 0"
shows "(λx. a.^x) integrable_on {0..c}"
proof (cases "a = 1")
case True
thus ?thesis
using has_integral_const_real by auto
next
case False
thus ?thesis
using has_integral_powr2_from_0 False assms by auto
qed

(* Stronger Version of lemma integral_power *)
lemma has_bochner_integral_power:
fixes a b :: real and k :: nat
assumes "a ≤ b"
shows "has_bochner_integral lborel (λx. x^k * indicator {a..b} x) ((b^(k+1) - a^(k+1)) / (k+1))"
proof -
have "⋀x. ((λx. x^(k+1) / (k+1)) has_real_derivative x^k) (at x)"
using DERIV_pow by (intro derivative_eq_intros) auto
hence "has_bochner_integral lborel (λx. x^k * indicator {a..b} x) (b^(k+1)/(k+1) - a^(k+1)/(k+1))"
by (intro has_bochner_integral_FTC_Icc_real; simp add: assms)
thus ?thesis by (simp add: diff_divide_distrib)
qed

corollary integrable_power: "(a::real) ≤ b ⟹ integrable lborel (λx. x^k * indicator {a..b} x)"
using has_bochner_integral_power integrable.intros by blast

(* Analogue for lemma has_integral_integral_real *)
lemma has_integral_set_integral_real:
fixes f::"'a::euclidean_space ⇒ real" and A :: "'a set"
assumes f: "set_integrable lborel A f"
shows "(f has_integral (set_lebesgue_integral lborel A f)) A"
using assms has_integral_integral_real[where f="λx. indicat_real A x * f x"]
unfolding set_integrable_def set_lebesgue_integral_def
by simp (smt (verit, ccfv_SIG) has_integral_cong has_integral_restrict_UNIV indicator_times_eq_if)

lemma set_borel_measurable_lborel:
"set_borel_measurable lborel A f ⟷ set_borel_measurable borel A f"
unfolding set_borel_measurable_def by simp

lemma restrict_space_whole[simp]: "restrict_space M (space M) = M"
unfolding restrict_space_def by (simp add: measure_of_of_measure)

lemma deriv_measurable_real:
fixes f :: "real ⇒ real"
assumes "f differentiable_on S" "open S" "f ∈ borel_measurable borel"
shows "set_borel_measurable borel S (deriv f)"
proof -
have "⋀x. x ∈ S ⟹ deriv f x = lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i))"
proof -
fix x assume x_S: "x ∈ S"
hence "f field_differentiable (at x within S)"
using differentiable_on_eq_field_differentiable_real assms by simp
hence "(f has_field_derivative deriv f x) (at x)"
using assms DERIV_deriv_iff_field_differentiable x_S at_within_open by force
hence "(λh. (f (x+h) - f x) / h) ─0→ deriv f x" using DERIV_def by auto
hence "∀d. (∀i. d i ∈ UNIV-{0::real}) ⟶ d ⇢ 0 ⟶
((λh. (f (x+h) - f x) / h) ∘ d) ⇢ deriv f x"
using tendsto_at_iff_sequentially by blast
moreover have "∀i. 1 / Suc i ∈ UNIV - {0::real}" by simp
moreover have "(λi. 1 / Suc i) ⇢ 0" using LIMSEQ_Suc lim_const_over_n by blast
ultimately have "((λh. (f (x + h) - f x) / h) ∘ (λi. 1 / Suc i)) ⇢ deriv f x" by auto
thus "deriv f x = lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i))"
unfolding comp_def by (simp add: limI)
qed
moreover have "(λx. indicator S x * lim (λi. (f (x + 1 / Suc i) - f x) / (1 / Suc i)))
∈ borel_measurable borel"
using assms by (measurable, simp, measurable)
ultimately show ?thesis
unfolding set_borel_measurable_def measurable_cong
by simp (smt (verit) indicator_simps(2) measurable_cong mult_eq_0_iff)
qed

lemma piecewise_differentiable_on_deriv_measurable_real:
fixes f :: "real ⇒ real"
assumes "f piecewise_differentiable_on S" "open S" "f ∈ borel_measurable borel"
shows "set_borel_measurable borel S (deriv f)"
proof -
from assms obtain T where fin: "finite T" and
diff: "⋀x. x ∈ S - T ⟹ f differentiable at x within S"
unfolding piecewise_differentiable_on_def by blast
with assms have "open (S - T)" using finite_imp_closed by blast
moreover hence "f differentiable_on (S - T)"
unfolding differentiable_on_def using assms by (metis Diff_iff at_within_open diff)
ultimately have "set_borel_measurable borel (S - T) (deriv f)"
by (intro deriv_measurable_real; simp add: assms)
thus ?thesis
unfolding set_borel_measurable_def apply simp
apply (rule measurable_discrete_difference
[where X=T and f="λx. indicat_real (S - T) x * deriv f x"], simp_all)
using fin uncountable_infinite apply blast
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 set_nn_integral_eq_set_integral:
assumes "AE x∈A in M. 0 ≤ f x" "set_integrable M A f"
shows "(∫⇧+x∈A. f x ∂M) = (∫x∈A. f x ∂M)"
proof -
have "(∫⇧+x∈A. f x ∂M) = ∫⇧+x. ennreal (f x * indicator A x) ∂M"
using nn_integral_set_ennreal by blast
also have "… = ∫x. f x * indicator A x ∂M"
using assms unfolding set_integrable_def
by (rewrite nn_integral_eq_integral; force simp add: mult.commute)
also have "… = (∫x∈A. f x ∂M)" unfolding set_lebesgue_integral_def by (simp add: mult.commute)
finally show ?thesis .
qed

proposition nn_integral_disjoint_family_on_finite:
assumes [measurable]: "f ∈ borel_measurable M" "⋀(n::nat). n ∈ S ⟹ B n ∈ sets M"
and "disjoint_family_on B S" "finite S"
shows "(∫⇧+x ∈ (⋃n∈S. B n). f x ∂M) = (∑n∈S. (∫⇧+x ∈ B n. f x ∂M))"
proof -
let ?A = "λn::nat. if n ∈ S then B n else {}"
have "⋀n::nat. ?A n ∈ sets M" by simp
moreover have "disjoint_family ?A"
unfolding disjoint_family_on_def
proof -
{ fix m n :: nat
assume "m ≠ n"
hence "(if m ∈ S then B m else {}) ∩ (if n ∈ S then B n else {}) = {}"
apply simp
using assms unfolding disjoint_family_on_def by blast }
thus "∀m::nat∈UNIV. ∀n::nat∈UNIV. m ≠ n ⟶
(if m ∈ S then B m else {}) ∩ (if n ∈ S then B n else {}) = {}"
by blast
qed
ultimately have "set_nn_integral M (⋃ (range ?A)) f = (∑n. set_nn_integral M (?A n) f)"
by (rewrite nn_integral_disjoint_family; simp)
moreover have "set_nn_integral M (⋃ (range ?A)) f = (∫⇧+x ∈ (⋃n∈S. B n). f x ∂M)"
proof -
have "⋃ (range ?A) = (⋃n∈S. B n)" by simp
thus ?thesis by simp
qed
moreover have "(∑n. set_nn_integral M (?A n) f) = (∑n∈S. set_nn_integral M (B n) f)"
by (rewrite suminf_finite[of S]; simp add: assms)
ultimately show ?thesis by simp
qed

lemma nn_integral_distr_set:
assumes "T ∈ measurable M M'" and "f ∈ borel_measurable (distr M M' T)"
and "A ∈ sets M'" and "⋀x. x ∈ space M ⟹ T x ∈ A"
shows "integral⇧N (distr M M' T) f = set_nn_integral (distr M M' T) A f"
proof -
have "integral⇧N (distr M M' T) f = (∫⇧+x∈(space M'). f x ∂(distr M M' T))"
by (rewrite nn_set_integral_space[THEN sym], simp)
also have "… = (∫⇧+x∈A. f x ∂(distr M M' T))"
proof -
have [simp]: "sym_diff (space M') A = space M' - A"
using assms by (metis Diff_mono sets.sets_into_space sup.orderE)
show ?thesis
apply (rule nn_integral_null_delta; simp add: assms)
unfolding null_sets_def using assms
apply (simp, rewrite emeasure_distr; simp)
unfolding vimage_def using emeasure_empty
by (smt (z3) Collect_empty_eq Diff_iff Int_def mem_Collect_eq)
qed
finally show ?thesis .
qed

(* Analogue for "measure_eqI_lessThan" in the "Lebesgue_Measure" Theory *)
lemma measure_eqI_Ioc:
fixes M N :: "real measure"
assumes sets: "sets M = sets borel" "sets N = borel"
assumes fin: "⋀a b. a ≤ b ⟹ emeasure M {a<..b} < ∞"
assumes eq: "⋀a b. a ≤ b ⟹ emeasure M {a<..b} = emeasure N {a<..b}"
shows "M = N"
proof (rule measure_eqI_generator_eq_countable)
let ?Ioc = "λ(a::real,b::real). {a<..b}" let ?E = "range ?Ioc"
show "Int_stable ?E" using Int_stable_def Int_greaterThanAtMost by force
show "?E ⊆ Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E"
unfolding sets by (auto simp add: borel_sigma_sets_Ioc)
show "⋀I. I ∈ ?E ⟹ emeasure M I = emeasure N I"
proof -
fix I assume "I ∈ ?E"
then obtain a b where "I = {a<..b}" by auto
thus "emeasure M I = emeasure N I" by (smt (verit, best) eq greaterThanAtMost_empty)
qed
show "?Ioc ` (Rats × Rats) ⊆ ?E" "(⋃i∈(Rats×Rats). ?Ioc i) = UNIV"
using Rats_no_bot_less Rats_no_top_le by auto
show "countable (?Ioc ` (Rats × Rats))" using countable_rat by blast
show "⋀I. I ∈ ?Ioc ` (Rats × Rats) ⟹ emeasure M I ≠ ∞"
proof -
fix I assume "I ∈ ?Ioc ` (Rats × Rats)"
then obtain a b where "(a,b) ∈ (Rats × Rats)" "I = {a<..b}" by blast
thus "emeasure M I ≠ ∞" by (smt (verit, best) Ioc_inj fin order.strict_implies_not_eq)
qed
qed

lemma (in finite_measure) distributed_measure:
assumes "distributed M N X f"
and "⋀x. x ∈ space N ⟹  f x ≥ 0"
and "A ∈ sets N"
shows "measure M (X -` A ∩ space M) = (∫x. indicator A x * f x ∂N)"
proof -
have [simp]: "(λx. indicat_real A x * f x) ∈ borel_measurable N"
using assms apply (measurable; simp?)
using distributed_real_measurable assms by force
have "emeasure M (X -` A ∩ space M) = (∫⇧+x∈A. ennreal (f x) ∂N)"
by (rule distributed_emeasure; simp add: assms)
moreover have "enn2real (∫⇧+x∈A. ennreal (f x) ∂N) = ∫x. indicator A x * f x ∂N"
apply (rewrite enn2real_nn_integral_eq_integral
[where f="λx. ennreal (indicator A x * f x)", THEN sym]; (simp add: assms)?)
using distributed_emeasure assms
by (smt (verit) emeasure_finite indicator_mult_ennreal mult.commute
nn_integral_cong top.not_eq_extremum)
ultimately show ?thesis using measure_def by metis
qed

lemma set_integrable_const[simp]:
"A ∈ sets M ⟹ emeasure M A < ∞ ⟹ set_integrable M A (λ_. c)"
using has_bochner_integral_indicator unfolding set_integrable_def by simp

lemma set_integral_const[simp]:
"A ∈ sets M ⟹ emeasure M A < ∞ ⟹ set_lebesgue_integral M A (λ_. c) = measure M A *⇩R c"
unfolding set_lebesgue_integral_def using has_bochner_integral_indicator by force

lemma set_integral_empty_0[simp]: "set_lebesgue_integral M {} f = 0"
unfolding set_lebesgue_integral_def by simp

lemma set_integral_nonneg[simp]:
fixes f :: "'a ⇒ real" and A :: "'a set"
shows "(⋀x. x ∈ A ⟹ 0 ≤ f x) ⟹ 0 ≤ set_lebesgue_integral M A f"
unfolding set_lebesgue_integral_def by (simp add: indicator_times_eq_if(1))

(* Set Integral Version of the Lebesgue's Dominated Convergence Theorem *)
lemma
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
assumes "A ∈ sets M" "set_borel_measurable M A f"
"⋀i. set_borel_measurable M A (s i)" "set_integrable M A w"
assumes lim: "AE x∈A in M. (λi. s i x) ⇢ f x"
assumes bound: "⋀i::nat. AE x∈A in M. norm (s i x) ≤ w x"
shows set_integrable_dominated_convergence: "set_integrable M A f"
and set_integrable_dominated_convergence2: "⋀i. set_integrable M A (s i)"
and set_integral_dominated_convergence:
"(λi. set_lebesgue_integral M A (s i)) ⇢  set_lebesgue_integral M A f"
proof -
have "(λx. indicator A x *⇩R f x) ∈ borel_measurable M" and
"⋀i. (λx. indicator A x *⇩R s i x) ∈ borel_measurable M" and
"integrable M (λx. indicator A x *⇩R w x)"
using assms unfolding set_borel_measurable_def set_integrable_def by simp_all
moreover have "AE x in M. (λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof -
obtain N where N_null: "N ∈ null_sets M" and
si_f: "⋀x. x ∈ space M - N ⟹ x ∈ A ⟶ (λi. s i x) ⇢ f x"
using lim AE_E3 by (smt (verit))
hence "⋀x. x ∈ space M - N ⟹ (λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof -
fix x assume asm: "x ∈ space M - N"
thus "(λi. indicator A x *⇩R s i x) ⇢ indicator A x *⇩R f x"
proof (cases ‹x ∈ A›)
case True
with si_f asm show ?thesis by simp
next
case False
thus ?thesis by simp
qed
qed
thus ?thesis by (smt (verit) AE_I' DiffI N_null mem_Collect_eq subsetI)
qed
moreover have "⋀i. AE x in M. norm (indicator A x *⇩R s i x) ≤ indicator A x *⇩R w x"
proof -
fix i
from bound obtain N where N_null: "N ∈ null_sets M" and
"⋀x. x ∈ space M - N ⟹ x ∈ A ⟶ norm (s i x) ≤ w x"
using AE_E3 by (smt (verit))
hence "⋀x. x ∈ space M - N ⟹ norm (indicator A x *⇩R s i x) ≤ indicator A x *⇩R w x"