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"
      by (metis Nat.add_0_right atLeastLessThan_iff le_nat_floor
          less_one linorder_not_le nat_add_left_cancel_le of_nat_floor)
    ultimately show "x  ((n::nat)<m. {real n ..< real n + 1})"
      unfolding atLeastLessThan_def by force
  qed
qed

lemma seq_part_multiple: fixes m n :: nat assumes "m  0" defines "A  λi::nat. {i*m ..< (i+1)*m}"
  shows "i j. i  j  A i  A j = {}" and "(i<n. A i) = {..< n*m}"
proof -
  { fix i j :: nat
    have "i  j  A i  A j = {}"
    proof (erule contrapos_np)
      assume "A i  A j  {}"
      then obtain k where "k  A i  A j" by blast
      hence "i*m < (j+1)*m  j*m < (i+1)*m" unfolding A_def by force
      hence "i < j+1  j < i+1" using mult_less_cancel2 by blast
      thus "i = j" by force
    qed }
  thus "i j. i  j  A i  A j = {}" by blast
next
  show "(i<n. A i) = {..< n*m}"
  proof
    show "(i<n. A i)  {..< n*m}"
    proof
      fix x::nat
      assume "x  (i<n. A i)"
      then obtain i where i_n: "i < n" and i_x: "x < (i+1)*m" unfolding A_def by force
      hence "i+1  n" by linarith
      hence "x < n*m" by (meson less_le_trans mult_le_cancel2 i_x)
      thus "x  {..< n*m}"
        using diff_mult_distrib mult_1 i_n by auto
    qed
  next
    show "{..< n*m}  (i<n. A i)"
    proof
      fix x::nat
      let ?i = "x div m"
      assume "x  {..< n*m}"
      hence "?i < n" by (simp add: less_mult_imp_div_less)
      moreover have "?i*m  x  x < (?i+1)*m"
        using assms div_times_less_eq_dividend dividend_less_div_times by auto
      ultimately show "x  (i<n. A i)" unfolding A_def by force
    qed
  qed
qed

lemma frontier_Icc_real: "frontier {a..b} = {a, b}" if "a  b" for a b :: real
  unfolding frontier_def using that by force

lemma(in field) divide_mult_cancel[simp]: fixes a b assumes "b  0"
  shows "a / b * b = a"
  by (simp add: assms)

lemma inverse_powr: "(1/a).^b = a.^-b" if "a > 0" for a b :: real
  by (smt that powr_divide powr_minus_divide powr_one_eq_one)

lemma powr_eq_one_iff_gen[simp]: "a.^x = 1  x = 0" if "a > 0" "a  1" for a x :: real
  by (metis powr_eq_0_iff powr_inj powr_zero_eq_one that)

lemma powr_less_cancel2: "0 < a  0 < x  0 < y  x.^a < y.^a  x < y"
  for a x y ::real
proof -
  assume a_pos: "0 < a" and x_pos: "0 < x" and y_pos: "0 < y"
  show "x.^a < y.^a  x < y"
  proof (erule contrapos_pp)
    assume "¬ x < y"
    hence "x  y" by fastforce
    hence "x.^a  y.^a"
    proof (cases "x = y")
      case True
      thus ?thesis by simp
    next
      case False
      hence "x.^a > y.^a"
        using x  y powr_less_mono2 a_pos y_pos by auto
      thus ?thesis by auto
    qed
    thus "¬ x.^a < y.^a" by fastforce
  qed
qed

lemma geometric_increasing_sum_aux: "(1-r)^2 * (k<n. (k+1)*r^k) = 1 - (n+1)*r^n + n*r^(n+1)"
  for n::nat and r::real
proof (induct n)
  case 0
  thus ?case by simp
next
  case (Suc n)
  thus ?case
    apply (simp only: sum.lessThan_Suc)
    apply (subst distrib_left)
    apply (subst Suc.hyps)
    by (subst power2_diff, simp add: field_simps power2_eq_square)
qed

lemma geometric_increasing_sum: "(k<n. (k+1)*r^k) = (1 - (n+1)*r^n + n*r^(n+1)) / (1-r)^2"
  if "r  1" for n::nat and r::real
  by (subst geometric_increasing_sum_aux[THEN sym], simp add: that)

lemma Reals_UNIV[simp]: " = {x::real. True}"
  unfolding Reals_def by auto

lemma Lim_cong:
  assumes "F x in F. f x = g x"
  shows "Lim F f = Lim F g"
  unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce

lemma LIM_zero_iff': "((λx. l - f x)  0) F = (f  l) F"
  for f :: "'a  'b::real_normed_vector"
  unfolding tendsto_iff dist_norm
  by (rewrite minus_diff_eq[THEN sym], rewrite norm_minus_cancel) simp

lemma antimono_onI:
  "(r s. r  A  s  A  r  s  f r  f s)  antimono_on A f"
  by (rule monotone_onI)

lemma antimono_onD:
  "antimono_on A f; r  A; s  A; r  s  f r  f s"
  by (rule monotone_onD)

lemma antimono_imp_mono_on: "antimono f  antimono_on A f"
  by (simp add: antimonoD antimono_onI)

lemma antimono_on_subset: "antimono_on A f  B  A  antimono_on B f"
  by (rule monotone_on_subset)

lemma mono_on_antimono_on:
  fixes f :: "'a::order  'b::ordered_ab_group_add"
  shows "mono_on A f  antimono_on A (λr. - f r)"
  by (simp add: monotone_on_def)

corollary mono_antimono:
  fixes f :: "'a::order  'b::ordered_ab_group_add"
  shows "mono f  antimono (λr. - f r)"
  by (rule mono_on_antimono_on)

lemma mono_on_at_top_le:
  fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
    and f :: "'a  'b"
  assumes f_mono: "mono_on {a..} f" and f_to_l: "(f  l) at_top"
  shows "x. x  {a..}  f x  l"
proof (unfold atomize_ball)
  { fix b assume b_a: "b  a" and fb_l: "¬ f b  l"
    let ?eps = "f b - l"
    have lim_top: "S. open S  l  S  eventually (λx. f x  S) at_top"
      using assms tendsto_def by auto
    have "eventually (λx. f x  {l - ?eps <..< l + ?eps}) at_top"
      using fb_l by (intro lim_top; force)
    then obtain N where fn_in: "n. n  N  f n  {l - ?eps <..< l + ?eps}"
      using eventually_at_top_linorder by metis
    let ?n = "max b N"
    have "f ?n < f b" using fn_in by force
    moreover have "f ?n  f b" using f_mono b_a by (simp add: le_max_iff_disj mono_on_def)
    ultimately have False by simp }
  thus "x{a..}. f x  l"
    apply -
    by (rule notnotD, rewrite Set.ball_simps) auto
qed

corollary mono_at_top_le:
  fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder  'b"
  assumes "mono f" and "(f  b) at_top"
  shows "x. f x  b"
  using mono_on_at_top_le assms by (metis atLeast_iff mono_imp_mono_on nle_le)

lemma mono_on_at_bot_ge:
  fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
    and f :: "'a  'b"
  assumes f_mono: "mono_on {..a} f" and f_to_l: "(f  l) at_bot"
  shows "x. x  {..a}  f x  l"
proof (unfold atomize_ball)
  { fix b assume b_a: "b  a" and fb_l: "¬ f b  l"
    let ?eps = "l - f b"
    have lim_bot: "S. open S  l  S  eventually (λx. f x  S) at_bot"
      using assms tendsto_def by auto
    have "eventually (λx. f x  {l - ?eps <..< l + ?eps}) at_bot"
      using fb_l by (intro lim_bot; force)
    then obtain N where fn_in: "n. n  N  f n  {l - ?eps <..< l + ?eps}"
      using eventually_at_bot_linorder by metis
    let ?n = "min b N"
    have "f ?n > f b" using fn_in by force
    moreover have "f ?n  f b" using f_mono b_a by (simp add: min.coboundedI1 mono_onD)
    ultimately have False by simp }
  thus "x{..a}. f x  l"
    apply -
    by (rule notnotD, rewrite Set.ball_simps) auto
qed

corollary mono_at_bot_ge:
  fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder  'b"
  assumes "mono f" and "(f  b) at_bot"
  shows "x. f x  b"
  using mono_on_at_bot_ge assms by (metis atMost_iff mono_imp_mono_on nle_le)

lemma antimono_on_at_top_ge:
  fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
    and f :: "'a  'b"
  assumes f_antimono: "antimono_on {a..} f" and f_to_l: "(f  l) at_top"
  shows "x. x  {a..}  f x  l"
proof (unfold atomize_ball)
  { fix b assume b_a: "b  a" and fb_l: "¬ f b  l"
    let ?eps = "l - f b"
    have lim_top: "S. open S  l  S  eventually (λx. f x  S) at_top"
      using assms tendsto_def by auto
    have "eventually (λx. f x  {l - ?eps <..< l + ?eps}) at_top"
      using fb_l by (intro lim_top; force)
    then obtain N where fn_in: "n. n  N  f n  {l - ?eps <..< l + ?eps}"
      using eventually_at_top_linorder by metis
    let ?n = "max b N"
    have "f ?n > f b" using fn_in by force
    moreover have "f ?n  f b" using f_antimono b_a
      by (simp add: antimono_onD le_max_iff_disj)
    ultimately have False by simp }
  thus "x{a..}. f x  l"
    apply -
    by (rule notnotD, rewrite Set.ball_simps) auto
qed

corollary antimono_at_top_le:
  fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder  'b"
  assumes "antimono f" and "(f  b) at_top"
  shows "x. f x  b"
  using antimono_on_at_top_ge assms antimono_imp_mono_on by blast

lemma antimono_on_at_bot_ge:
  fixes a :: "'a::linorder" and b :: "'b::{order_topology, linordered_ab_group_add}"
    and f :: "'a  'b"
  assumes f_antimono: "antimono_on {..a} f" and f_to_l: "(f  l) at_bot"
  shows "x. x  {..a}  f x  l"
proof (unfold atomize_ball)
  { fix b assume b_a: "b  a" and fb_l: "¬ f b  l"
    let ?eps = "f b - l"
    have lim_bot: "S. open S  l  S  eventually (λx. f x  S) at_bot"
      using assms tendsto_def by auto
    have "eventually (λx. f x  {l - ?eps <..< l + ?eps}) at_bot"
      using fb_l by (intro lim_bot; force)
    then obtain N where fn_in: "n. n  N  f n  {l - ?eps <..< l + ?eps}"
      using eventually_at_bot_linorder by metis
    let ?n = "min b N"
    have "f ?n < f b" using fn_in by force 
   moreover have "f ?n  f b" using f_antimono b_a by (simp add: min.coboundedI1 antimono_onD)
    ultimately have False by simp }
  thus  "x{..a}. f x  l"
    apply -
    by (rule notnotD, rewrite Set.ball_simps) auto
qed

corollary antimono_at_bot_ge:
  fixes b :: "'b::{order_topology, linordered_ab_group_add}" and f :: "'a::linorder  'b"
  assumes "antimono f" and "(f  b) at_bot"
  shows "x. f x  b"
  using antimono_on_at_bot_ge assms antimono_imp_mono_on by blast

lemma continuous_cdivide:
  fixes c::"'a::real_normed_field"
  assumes "c  0" "continuous F f"
  shows "continuous F (λx. f x / c)"
  using assms continuous_mult_right by (rewrite field_class.field_divide_inverse) auto

lemma continuous_mult_left_iff:
  fixes c::"'a::real_normed_field"
  assumes "c  0"
  shows "continuous F f  continuous F (λx. c * f x)"
  using continuous_mult_left continuous_cdivide assms by force

lemma continuous_mult_right_iff:
  fixes c::"'a::real_normed_field"
  assumes "c  0"
  shows "continuous F f  continuous F (λx. f x * c)"
  using continuous_mult_right continuous_cdivide assms by force

lemma continuous_cdivide_iff:
  fixes c::"'a::real_normed_field"
  assumes "c  0"
  shows "continuous F f  continuous F (λx. f x / c)"
proof
  assume "continuous F f"
  thus "continuous F (λx. f x / c)"
    by (intro continuous_cdivide) (simp add: assms)
next
  assume "continuous F (λx. f x / c)"
  hence "continuous F (λx. f x / c * c)" using continuous_mult_right by fastforce
  thus "continuous F f" using assms by force
qed

lemma continuous_cong:
  assumes "eventually (λx. f x = g x) F" "f (Lim F (λx. x)) = g (Lim F (λx. x))"
  shows "continuous F f  continuous F g"
  unfolding continuous_def using assms filterlim_cong by force

lemma continuous_at_within_cong:
  assumes "f x = g x" "eventually (λx. f x = g x) (at x within s)"
  shows "continuous (at x within s) f  continuous (at x within s) g"
proof (cases x  closure (s - {x}))
  case True
  thus ?thesis
    using assms apply (intro continuous_cong, simp)
    by (rewrite Lim_ident_at, simp add: at_within_eq_bot_iff)+ simp
next
  case False
  hence "at x within s = bot" using not_trivial_limit_within by blast
  thus ?thesis by simp
qed

lemma continuous_within_shift:
  fixes a x :: "'a :: {topological_ab_group_add, t2_space}"
    and s :: "'a set"
    and f :: "'a  'b::topological_space"
  shows "continuous (at x within s) (λx. f (x+a))  continuous (at (x+a) within plus a ` s) f"
proof
  assume "continuous (at x within s) (λx. f (x+a))"
  moreover have "continuous (at (x+a) within plus a ` s) (plus (-a))"
    by (simp add: continuous_at_imp_continuous_at_within)
  moreover have "plus (-a) ` plus a ` s = s" by force
  ultimately show "continuous (at (x+a) within plus a ` s) f"
    using continuous_within_compose unfolding comp_def by force
next
  assume "continuous (at (x+a) within plus a ` s) f"
  moreover have "continuous (at x within s) (plus a)"
    by (simp add: continuous_at_imp_continuous_at_within)
  ultimately show "continuous (at x within s) (λx. f (x+a))"
    using continuous_within_compose unfolding comp_def by (force simp add: add.commute)
qed

lemma isCont_shift:
  fixes a x :: "'a :: {topological_ab_group_add, t2_space}"
    and f :: "'a  'b::topological_space"
  shows "isCont (λx. f (x+a)) x  isCont f (x+a)"
  using continuous_within_shift by force

lemma has_real_derivative_at_split:
  "(f has_real_derivative D) (at x) 
    (f has_real_derivative D) (at_left x)  (f has_real_derivative D) (at_right x)"
proof -
  have "at x = at x within ({..<x}  {x<..})" by (simp add: at_eq_sup_left_right at_within_union)
  thus "(f has_real_derivative D) (at x) 
    (f has_real_derivative D) (at_left x)  (f has_real_derivative D) (at_right x)"
    using Lim_within_Un has_field_derivative_iff by fastforce
qed

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

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

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

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

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

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

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

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

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

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

lemma indicator_Icc_shift_inverse:
  fixes a b t x :: "'a::linordered_ab_group_add"
  shows "indicator {a-t..b-t} x = indicator {a..b} (t+x)"
  by (metis add.commute diff_add_cancel indicator_Icc_shift)

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

lemma indicator_Ici_shift_inverse:
  fixes a t x :: "'a::linordered_ab_group_add"
  shows "indicator {a-t..} x = indicator {a..} (t+x)"
  by (metis add.commute diff_add_cancel indicator_Ici_shift)

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

lemma indicator_Iic_shift_inverse:
  fixes b t x :: "'a::linordered_ab_group_add"
  shows "indicator {..b-t} x = indicator {..b} (t+x)"
  by (metis add.commute diff_add_cancel indicator_Iic_shift)

lemma indicator_Icc_reverse:
  fixes a b t x :: "'a::linordered_ab_group_add"
  shows "indicator {a..b} x = indicator {t-b..t-a} (t-x)"
  by (metis add_le_cancel_left atLeastAtMost_iff diff_add_cancel indicator_simps le_diff_eq)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma differentiable_on_eq_field_differentiable_real:
  fixes f :: "real  real"
  shows "f differentiable_on s  (xs. 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. xs  f x = g x" and "f differentiable_on s"
  shows "g differentiable_on s"
proof -
  { fix x assume "xs"
    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 xs by metis
    hence "g differentiable at x within s" unfolding differentiable_def by blast }
  hence "xs. 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  (xS-T. g  f differentiable at x within S)" using fin by blast
  moreover have "continuous_on S (g  f)"
    using assms continuous_on_compose differentiable_imp_continuous_on
    unfolding piecewise_differentiable_on_def by blast
  ultimately show ?thesis
    unfolding piecewise_differentiable_on_def by force
qed

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma piecewise_differentiable_on_deriv_measurable_real:
  fixes f :: "real  real"
  assumes "f piecewise_differentiable_on S" "open S" "f  borel_measurable borel"
  shows "set_borel_measurable borel S (deriv f)"
proof -
  from assms obtain T where fin: "finite T" and
    diff: "x. x  S - T  f differentiable at x within S"
    unfolding piecewise_differentiable_on_def by blast
  with assms have "open (S - T)" using finite_imp_closed by blast
  moreover hence "f differentiable_on (S - T)"
    unfolding differentiable_on_def using assms by (metis Diff_iff at_within_open diff)
  ultimately have "set_borel_measurable borel (S - T) (deriv f)"
    by (intro deriv_measurable_real; simp add: assms)
  thus ?thesis
    unfolding set_borel_measurable_def apply simp
    apply (rule measurable_discrete_difference
        [where X=T and f="λx. indicat_real (S - T) x * deriv f x"], simp_all)
    using fin uncountable_infinite apply blast
    by (simp add: indicator_diff)
qed

lemma borel_measurable_antimono:
  fixes f :: "real  real"
  shows "antimono f  f  borel_measurable borel"
  using borel_measurable_mono by (smt (verit, del_insts) borel_measurable_uminus_eq monotone_on_def)

lemma set_borel_measurable_restrict_space_iff: 
  fixes f :: "'a  'b::real_normed_vector"
  assumes Ω[measurable, simp]: "Ω  space M  sets M"
  shows "f  borel_measurable (restrict_space M Ω)  set_borel_measurable M Ω f"
  using assms borel_measurable_restrict_space_iff set_borel_measurable_def by blast

lemma set_integrable_restrict_space_iff:
  fixes f :: "'a  'b::{banach, second_countable_topology}"
  assumes "A  sets M"
  shows "set_integrable M A f  integrable (restrict_space M A) f"
  unfolding set_integrable_def using assms
  by (rewrite integrable_restrict_space; simp)

lemma set_lebesgue_integral_restrict_space:
  fixes f :: "'a  'b::{banach, second_countable_topology}"
  assumes "A  sets M"
  shows "set_lebesgue_integral M A f = integralL (restrict_space M A) f"
  unfolding set_lebesgue_integral_def using assms integral_restrict_space
  by (metis (mono_tags) sets.Int_space_eq2)

lemma distr_borel_lborel: "distr M borel f = distr M lborel f"
  by (metis distr_cong sets_lborel)

lemma AE_translation:
  assumes "AE x in lborel. P x" shows "AE x in lborel. P (a+x)"
proof -
  from assms obtain N where P: "x. x  space lborel - N  P x" and null: "N  null_sets lborel"
    using AE_E3 by blast
  hence "{y. a+y  N}  null_sets lborel"
    using null_sets_translation[of N "-a", simplified] by (simp add: add.commute)
  moreover have "y. y  space lborel - {y. a+y  N}  P (a+y)" using P by force
  ultimately show "AE y in lborel. P (a+y)"
    by (smt (verit, del_insts) Diff_iff eventually_ae_filter mem_Collect_eq subsetI)
qed

lemma set_AE_translation:
  assumes "AE xS 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 xA in M. f x = g x"
  shows "(+xA. f x M) = (+xA. 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 xA in M. 0  f x" "set_integrable M A f"
  shows "(+xA. f x M) = (xA. f x M)"
proof -
  have "(+xA. 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 " = (xA. 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  (nS. B n). f x M) = (nS. (+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::natUNIV. n::natUNIV. 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  (nS. B n). f x M)"
  proof -
    have " (range ?A) = (nS. B n)" by simp
    thus ?thesis by simp
  qed
  moreover have "(n. set_nn_integral M (?A n) f) = (nS. 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 "integralN (distr M M' T) f = set_nn_integral (distr M M' T) A f"
proof -
  have "integralN (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 " = (+xA. 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) = (+xA. ennreal (f x) N)"
    by (rule distributed_emeasure; simp add: assms)
  moreover have "enn2real (+xA. 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 xA in M. (λi. s i x)  f x"
  assumes bound: "i::nat. AE xA in M. norm (s i x)  w x"
  shows set_integrable_dominated_convergence: "set_integrable M A f"
    and set_integrable_dominated_convergence2: "i. set_integrable M A (s i)"
    and set_integral_dominated_convergence:
    "(λi. set_lebesgue_integral M A (s i))   set_lebesgue_integral M A f"
proof -
  have "(λx. indicator A x *R f x)  borel_measurable M" and
    "i. (λx. indicator A x *R s i x)  borel_measurable M" and
    "integrable M (λx. indicator A x *R w x)"
    using assms unfolding set_borel_measurable_def set_integrable_def by simp_all
  moreover have "AE x in M. (λi. indicator A x *R s i x)  indicator A x *R f x"
  proof -
    obtain N where N_null: "N  null_sets M" and
      si_f: "x. x  space M - N  x  A  (λi. s i x)  f x"
      using lim AE_E3 by (smt (verit))
    hence "x. x  space M - N  (λi. indicator A x *R s i x)  indicator A x *R f x"
    proof -
      fix x assume asm: "x  space M - N"
      thus "(λi. indicator A x *R s i x)  indicator A x *R f x"
      proof (cases x  A)
        case True
        with si_f asm show ?thesis by simp
      next 
        case False
        thus ?thesis by simp
      qed
    qed
    thus ?thesis by (smt (verit) AE_I' DiffI N_null mem_Collect_eq subsetI)
  qed
  moreover have "i. AE x in M. norm (indicator A x *R s i x)  indicator A x *R w x"
  proof -
    fix i
    from bound obtain N where N_null: "N  null_sets M" and
      "x. x  space M - N  x  A  norm (s i x)  w x"
      using AE_E3 by (smt (verit))
    hence "x. x  space M - N  norm (indicator A x *R s i x)  indicator A x *R w x"
      by (simp add: indicator_scaleR_eq_if)
    with N_null show "AE x in M. norm (indicator A x *R s i x)  indicator A x