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 (verit) that powr_divide powr_minus_divide powr_one_eq_one)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma set_AE_translation:
  assumes "AE x∈S in lborel. P x" shows "AE x ∈ plus (-a) ` S in lborel. P (a+x)"
proof -
  have "AE x in lborel. a+x ∈ S ⟶ P (a+x)" using assms by (rule AE_translation)
  moreover have "⋀x. a+x ∈ S ⟷ x ∈ plus (-a) ` S" by force
  ultimately show ?thesis by simp
qed

lemma AE_scale_measure_iff:
  assumes "r > 0"
  shows "(AE x in (scale_measure r M). P x) ⟷ (AE x in M. P x)"
  unfolding ae_filter_def null_sets_def
  apply (rewrite space_scale_measure, simp)
  using assms by (smt (verit) 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 (metis (no_types, lifting) Diff_disjoint disjoint_iff_not_equal mem_Collect_eq)
  qed
  finally show ?thesis .
qed

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

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

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

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

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

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

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

lemma absolutely_integrable_on_iff_set_integrable:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "f ∈ borel_measurable lborel"
    and  "S ∈ sets lborel"
  shows "set_integrable lborel S f ⟷ f absolutely_integrable_on S"
  unfolding set_integrable_def apply (simp, rewrite integrable_completion[THEN sym])
   apply measurable using assms by simp_all

corollary integrable_on_iff_set_integrable_nonneg:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "⋀x. x ∈ S ⟹ f x ≥ 0" "f ∈ borel_measurable lborel"
    and  "S ∈ sets lborel"
  shows "set_integrable lborel S f ⟷ f integrable_on S"
  using absolutely_integrable_on_iff_set_integrable assms
  by (metis absolutely_integrable_on_iff_nonneg)

lemma integrable_on_iff_set_integrable_nonneg_AE:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "AE x∈S in lborel. f x ≥ 0" "f ∈ borel_measurable lborel"
    and  "S ∈ sets lborel"
  shows "set_integrable lborel S f ⟷ f integrable_on S"
proof -
  from assms obtain N where nonneg: "⋀x. x ∈ S - N ⟹ f x ≥ 0" and null: "N ∈ null_sets lborel"
    by (smt (verit, ccfv_threshold) AE_E3 Diff_iff UNIV_I space_borel space_lborel)
  let ?g = "λx. if x ∈ N then 0 else f x"
  have [simp]: "negligible N" using null negligible_iff_null_sets null_sets_completionI by blast
  have "N ∈ sets lborel" using null by auto
  hence [simp]: "?g ∈ borel_measurable borel" using assms by force
  have "set_integrable lborel S f ⟷ set_integrable lborel S ?g"
  proof -
    have "AE x∈S in lborel. f x = ?g x" by (rule AE_I'[of N], simp_all add: null, blast)
    thus ?thesis using assms by (intro set_integrable_cong_AE[of f _ ?g S]; simp)
  qed
  also have "… ⟷ ?g integrable_on S"
    using assms by (intro integrable_on_iff_set_integrable_nonneg; simp add: nonneg)
  also have "… ⟷ f integrable_on S" by (rule integrable_spike_cong[of N]; simp)
  finally show ?thesis .
qed

lemma set_borel_integral_eq_integral_nonneg:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "⋀x. x ∈ S ⟹ f x ≥ 0" "f ∈ borel_measurable borel" "S ∈ sets borel"
  shows "(LINT x : S | lborel. f x) = integral S f"
    ― ‹Note that ‹0 = 0› holds when the integral diverges.›
proof (cases ‹set_integrable lborel S f›)
  case True
  thus ?thesis using set_borel_integral_eq_integral by force
next
  case False
  hence "(LINT x : S | lborel. f x) = 0"
    unfolding set_lebesgue_integral_def set_integrable_def
    by (rewrite not_integrable_integral_eq; simp)
  moreover have "integral S f = 0"
    apply (rule not_integrable_integral)
    using False assms by (rewrite in asm integrable_on_iff_set_integrable_nonneg; simp)
  ultimately show ?thesis ..
qed

lemma set_borel_integral_eq_integral_nonneg_AE:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes "AE x∈S in lborel. f x ≥ 0" "f ∈ borel_measurable borel" "S ∈ sets borel"
  shows "(LINT x : S | lborel. f x) = integral S f"
    ― ‹Note that ‹0 = 0› holds when the integral diverges.›
proof (cases ‹set_integrable lborel S f›)
  case True
  thus ?thesis using set_borel_integral_eq_integral by force
next
  case False
  hence "(LINT x : S | lborel. f x) = 0"
    unfolding set_lebesgue_integral_def set_integrable_def
    by (rewrite not_integrable_integral_eq; simp)
  moreover have "integral S f = 0"
    apply (rule not_integrable_integral)
    using False assms by (rewrite in asm integrable_on_iff_set_integrable_nonneg_AE; simp)
  ultimately show ?thesis ..
qed

subsection ‹Set Lebesgue Integrability on Affine Transformation›

lemma set_integrable_Icc_affine_pos_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b c t :: real
  assumes "c > 0"
  shows "set_integrable lborel {(a-t)/c..(b-t)/c} (λx. f (t + c*x))
    ⟷ set_integrable lborel {a..b} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Icc_affine_pos_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Icc_shift:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b t :: real
  shows "set_integrable lborel {a-t..b-t} (λx. f (t+x)) ⟷ set_integrable lborel {a..b} f"
  using set_integrable_Icc_affine_pos_iff[where c=1] by simp

lemma set_integrable_Ici_affine_pos_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a c t :: real
  assumes "c > 0"
  shows "set_integrable lborel {(a-t)/c..} (λx. f (t + c*x))
    ⟷ set_integrable lborel {a..} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Ici_affine_pos_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Ici_shift:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a t :: real
  shows "set_integrable lborel {a-t..} (λx. f (t+x)) ⟷ set_integrable lborel {a..} f"
  using set_integrable_Ici_affine_pos_iff[where c=1] by simp

lemma set_integrable_Iic_affine_pos_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b c t :: real
  assumes "c > 0"
  shows "set_integrable lborel {..(b-t)/c} (λx. f (t + c*x))
    ⟷ set_integrable lborel {..b} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Iic_affine_pos_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Iic_shift:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b t :: real
  shows "set_integrable lborel {..b-t} (λx. f (t+x)) ⟷ set_integrable lborel {..b} f"
  using set_integrable_Iic_affine_pos_iff[where c=1] by simp

lemma set_integrable_Icc_affine_neg_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b c t :: real
  assumes "c < 0"
  shows "set_integrable lborel {(b-t)/c..(a-t)/c} (λx. f (t + c*x))
    ⟷ set_integrable lborel {a..b} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Icc_affine_neg_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Icc_reverse:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b t :: real
  shows "set_integrable lborel {t-b..t-a} (λx. f (t-x)) ⟷ set_integrable lborel {a..b} f"
  using set_integrable_Icc_affine_neg_iff[where c="-1"] by simp

lemma set_integrable_Ici_affine_neg_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b c t :: real
  assumes "c < 0"
  shows "set_integrable lborel {(b-t)/c..} (λx. f (t + c*x))
    ⟷ set_integrable lborel {..b} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Ici_affine_neg_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Ici_reverse:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and b t :: real
  shows "set_integrable lborel {t-b..} (λx. f (t-x)) ⟷ set_integrable lborel {..b} f"
  using set_integrable_Ici_affine_neg_iff[where c="-1"] by simp

lemma set_integrable_Iic_affine_neg_iff:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a c t :: real
  assumes "c < 0"
  shows "set_integrable lborel {..(a-t)/c} (λx. f (t + c*x))
    ⟷ set_integrable lborel {a..} f"
  unfolding set_integrable_def using assms
  apply (rewrite indicator_Iic_affine_neg_inverse, simp)
  by (rule lborel_integrable_real_affine_iff) simp

corollary set_integrable_Iic_reverse:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a t :: real
  shows "set_integrable lborel {..t-a} (λx. f (t-x)) ⟷ set_integrable lborel {a..} f"
  using set_integrable_Iic_affine_neg_iff[where c="-1"] by simp

subsection ‹Set Lebesgue Integral on Affine Transformation›

lemma lborel_set_integral_Icc_affine_pos:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b c :: real
  assumes "c > 0"
  shows "(∫x∈{a..b}. f x ∂lborel) = c *⇩R (∫x∈{(a-t)/c..(b-t)/c}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Icc_affine_pos_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Icc_shift:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b :: real
  shows "(∫x∈{a..b}. f x ∂lborel) = (∫x∈{a-t..b-t}. f (t+x) ∂lborel)"
  using lborel_set_integral_Icc_affine_pos[where c=1] by simp

lemma lborel_set_integral_Ici_affine_pos:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a c :: real
  assumes "c > 0"
  shows "(∫x∈{a..}. f x ∂lborel) = c *⇩R (∫x∈{(a-t)/c..}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Ici_affine_pos_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Ici_shift:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a::real
  shows "(∫x∈{a..}. f x ∂lborel) = (∫x∈{a-t..}. f (t+x) ∂lborel)"
  using lborel_set_integral_Ici_affine_pos[where c=1] by simp

lemma lborel_set_integral_Iic_affine_pos:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b c :: real
  assumes "c > 0"
  shows "(∫x∈{..b}. f x ∂lborel) = c *⇩R (∫x∈{..(b-t)/c}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Iic_affine_pos_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Iic_shift:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b::real
  shows "(∫x∈{..b}. f x ∂lborel) = (∫x∈{..b-t}. f (t+x) ∂lborel)"
  using lborel_set_integral_Iic_affine_pos[where c=1] by simp

lemma lborel_set_integral_Icc_affine_neg:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b c :: real
  assumes "c < 0"
  shows "(∫x∈{a..b}. f x ∂lborel) = -c *⇩R (∫x∈{(b-t)/c..(a-t)/c}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Icc_affine_neg_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Icc_reverse:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a b :: real
  shows "(∫x∈{a..b}. f x ∂lborel) = (∫x∈{t-b..t-a}. f (t-x) ∂lborel)"
  using lborel_set_integral_Icc_affine_neg[where c="-1"] by simp

lemma lborel_set_integral_Ici_affine_neg:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b c :: real
  assumes "c < 0"
  shows "(∫x∈{..b}. f x ∂lborel) = -c *⇩R (∫x∈{(b-t)/c..}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Ici_affine_neg_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Ici_reverse:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and b::real
  shows "(∫x∈{..b}. f x ∂lborel) = (∫x∈{t-b..}. f (t-x) ∂lborel)"
  using lborel_set_integral_Ici_affine_neg[where c="-1"] by simp

lemma lborel_set_integral_Iic_affine_neg:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a c :: real
  assumes "c < 0"
  shows "(∫x∈{a..}. f x ∂lborel) = -c *⇩R (∫x∈{..(a-t)/c}. f (t + c*x) ∂lborel)"
  unfolding set_lebesgue_integral_def using assms
  apply (rewrite indicator_Iic_affine_neg_inverse, simp)
  using lborel_integral_real_affine[where c=c] by force

corollary lborel_set_integral_Iic_reverse:
  fixes f :: "real ⇒ 'a :: {banach, second_countable_topology}" and a::real
  shows "(∫x∈{a..}. f x ∂lborel) = (∫x∈{..t-a}. f (t-x) ∂lborel)"
  using lborel_set_integral_Iic_affine_neg[where c="-1"] by simp

lemma set_integrable_Ici_equiv_aux:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b :: real
  assumes "⋀c d. set_integrable lborel {c..d} f" "a ≤ b"
  shows "set_integrable lborel {a..} f ⟷ set_integrable lborel {b..} f"
proof
  assume "set_integrable lborel {a..} f"
  thus "set_integrable lborel {b..} f" by (rule set_integrable_subset; simp add: assms)
next
  assume "set_integrable lborel {b..} f"
  moreover have "set_integrable lborel {a..b} f" using assms by blast
  moreover have "{a..} = {a..b} ∪ {b..}" using assms by auto
  ultimately show "set_integrable lborel {a..} f" using set_integrable_Un by force
qed

corollary set_integrable_Ici_equiv:
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}" and a b :: real
  assumes "⋀c d. set_integrable lborel {c..d} f"
  shows "set_integrable lborel {a..} f ⟷ set_integrable lborel {b..} f"
  using set_integrable_Ici_equiv_aux assms by (smt (verit))

lemma set_integrable_Iic_equiv:
  fixes f :: "real ⇒ real" and a b :: real
  assumes "⋀c d. set_integrable lborel {c..d} f"
  shows "set_integrable lborel {..a} f ⟷ set_integrable lborel {..b} f" (is "?LHS ⟷ ?RHS")
proof -
  have "?LHS ⟷ set_integrable lborel {-a..} (λx. f (-x))"
    using set_integrable_Ici_reverse[where t=0] by force
  also have "… ⟷ set_integrable lborel {-b..} (λx. f (-x))"
  proof -
    have "⋀c d. set_integrable lborel {c..d} (λx. f (-x))"
      apply (rewrite at "{⌑.._}" minus_minus[THEN sym])
      apply (rewrite at "{_..⌑}" minus_minus[THEN sym])
      using assms set_integrable_Icc_reverse[where t=0] by force
    thus ?thesis by (rule set_integrable_Ici_equiv)
  qed
  also have "… ⟷ ?RHS" using set_integrable_Ici_reverse[where t=0] by force
  finally show ?thesis .
qed

subsection ‹Alternative Integral Test›

lemma nn_integral_suminf_Ico_real_nat:
  fixes a::real and f :: "real ⇒ ennreal"
  assumes "f ∈ borel_measurable lborel"
  shows "(∫⇧+x∈{a..}. f x ∂lborel) = (∑k. ∫⇧+x∈{a+k..<a+k+1}. f x ∂lborel)"
  apply (rewrite Ico_real_nat_union[THEN sym])
  using Ico_real_nat_disjoint assms by (intro nn_integral_disjoint_family; simp)

lemma set_integrable_iff_bounded:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes "A ∈ sets M"
  shows "set_integrable M A f ⟷ set_borel_measurable M A f ∧ (∫⇧+x∈A. norm (f x) ∂M) < ∞"
  unfolding set_integrable_def set_borel_measurable_def using integrable_iff_bounded
  by (smt (verit, ccfv_threshold) indicator_mult_ennreal indicator_pos_le
      mult.commute nn_integral_cong norm_scaleR)

(* Another Version of theorem integral_test *)
theorem set_integrable_iff_summable:
  fixes a::real and f :: "real ⇒ real"
  assumes "antimono_on {a..} f" "⋀x. a ≤ x ⟹ f x ≥ 0" "f ∈ borel_measurable lborel"
  shows "set_integrable lborel {a..} f ⟷ summable (λk. f (a+k))"
proof
  assume asm: "set_integrable lborel {a..} f"
  have [measurable]: "(λx. ennreal (f x)) ∈ borel_measurable lborel" using assms by simp
  have "∀k≥0. norm (f (a+(k+1::nat))) ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)"
  proof -
    { fix k::nat
      have "norm (f (a+(k+1::nat))) = f (a+k+1)"
        using assms by (smt (verit) of_nat_0_le_iff of_nat_1 of_nat_add real_norm_def)
      also have "… = (∫x∈{a+k..<a+k+1}. f (a+k+1) ∂lborel)"
        unfolding set_lebesgue_integral_def by simp
      also have "… ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)"
        apply (rule set_integral_mono, simp)
         apply (rule set_integrable_restrict_space[of lborel "{a..}"], simp add: asm)
         apply (rewrite sets_restrict_space, force)
        using assms unfolding mono_on_def monotone_on_def by simp
      finally have "norm (f (a+(k+1::nat))) ≤ (∫x∈{a+k..<a+k+1}. f x ∂lborel)" . }
    thus ?thesis by simp
  qed
  moreover have "summable (λk. ∫x∈{a+k..<a+k+1}. f x ∂lborel)"
  proof -
    have "(∫⇧+x∈{a..}. ennreal (f x) ∂lborel) ≠ ∞"
      using asm unfolding set_integrable_def apply simp
      by (smt (verit) indicator_mult_ennreal infinity_ennreal_def mult.commute
          nn_integral_cong real_integrable_def)
    thus ?thesis
      apply (rewrite in asm nn_integral_suminf_Ico_real_nat, simp)
      apply (rule summable_suminf_not_top)
      using assms apply (intro set_integral_nonneg, force)
      apply (rewrite set_nn_integral_eq_set_integral[THEN sym], simp add: assms)
      by (rule set_integrable_subset[of lborel "{a..}"], simp_all add: asm) force
  qed
  ultimately have "summable (λk. f (a+(k+1::nat)))"
    using summable_comparison_test by (smt (verit, del_insts))
  thus "summable (λk. f (a+k))" using summable_iff_shift by blast
next
  assume asm: "summable (λk. f (a+k))"
  hence "(∫⇧+x∈{a..}. ennreal ¦f x¦ ∂lborel) < ∞"
  proof -
    have "(∫⇧+x∈{a..}. ennreal ¦f x¦ ∂lborel) = (∫⇧+x∈{a..}. ennreal (f x) ∂lborel)"
      using assms by (metis abs_of_nonneg atLeast_iff indicator_simps(2) mult_eq_0_iff)
    also have "…  = (∑k. ∫⇧+x∈{a+k..<a+k+1}. ennreal (f x) ∂lborel)"
      using assms by (rewrite nn_integral_suminf_Ico_real_nat; simp)
    also have "… ≤ (∑k. ∫⇧+x∈{a+k..<a+k+1}. ennreal (f (a+k)) ∂lborel)"
    proof -
      have "⋀(k::nat) x. x∈{a+k..<a+k+1} ⟹ f x ≤ f (a+k)"
        using assms unfolding monotone_on_def by auto
      thus ?thesis
        apply (intro suminf_le, simp_all)
        by (rule nn_integral_mono)
          (metis (no_types, opaque_lifting) atLeastLessThan_iff dual_order.refl ennreal_leI
            indicator_simps(2) mult_eq_0_iff mult_mono zero_le)
    qed
    also have "… = (∑k. ennreal (f (a+k)))"
      apply (rule suminf_cong)
      by (rewrite nn_integral_cmult_indicator; simp)
    also have "… < ∞"
      unfolding infinity_ennreal_def apply (rewrite less_top[THEN sym])
      using asm assms by (smt (verit) of_nat_0_le_iff suminf_cong suminf_ennreal2 top_neq_ennreal)
    finally show ?thesis .
  qed
  moreover have "set_borel_measurable lborel {a..} f"
    using assms unfolding set_borel_measurable_def by simp
  ultimately show "set_integrable lborel {a..} f" by (rewrite set_integrable_iff_bounded) auto
qed

subsection ‹Interchange of Differentiation and Lebesgue Integration›

definition measurable_extension :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  "measurable_extension M N f = 
    (SOME g. g ∈ M →⇩M N ∧ (∃S∈(null_sets M). {x ∈ space M. f x ≠ g x} ⊆ S))"
  ― ‹The term ‹measurable_extension› is proposed by Reynald Affeldt.›
  ― ‹This function is used to make an almost-everywhere-defined function measurable.›

lemma
  fixes f g
  assumes "g ∈ M →⇩M N" "S ∈ null_sets M" "{x ∈ space M. f x ≠ g x} ⊆ S"
  shows measurable_extensionI: "AE x in M. f x = measurable_extension M N f x" and
    measurable_extensionI2: "AE x in M. g x = measurable_extension M N f x" and
    measurable_extension_measurable: "measurable_extension M N f ∈ measurable M N"
proof -
  let ?G = "λg. g ∈ M →⇩M N" and ?S = "λg. ∃S∈null_sets M. {x ∈ space M. f x ≠ g x} ⊆ S"
  show "AE x in M. f x = measurable_extension M N f x"
    unfolding measurable_extension_def
    apply (rule someI2[of "λg. ?G g ∧ ?S g" g])
    using assms apply blast
    using AE_I' by auto
  moreover have "AE x in M. g x = f x"
    using assms by (smt (verit, best) AE_I' Collect_cong)
  ultimately show "AE x in M. g x = measurable_extension M N f x" by force
  show "measurable_extension M N f ∈ measurable M N"
    unfolding measurable_extension_def
    apply (rule conjE[of "?G g" "?S g"])
    using assms apply auto[1]
    using someI_ex[of "λg. ?G g ∧ ?S g"] by auto
qed

corollary measurable_measurable_extension_AE:
  fixes f
  assumes "f ∈ M →⇩M N"
  shows "AE x in M. f x = measurable_extension M N f x"
  by (rule measurable_extensionI[where g=f and S="{}"]; simp add: assms)

definition borel_measurable_extension ::
  "'a measure ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b" where
  "borel_measurable_extension M f = measurable_extension M borel f"

lemma
  fixes f g
  assumes "g ∈ borel_measurable M" "S ∈ null_sets M" "{x ∈ space M. f x ≠ g x} ⊆ S"
  shows borel_measurable_extensionI: "AE x in M. f x = borel_measurable_extension M f x" and
    borel_measurable_extensionI2: "AE x in M. g x = borel_measurable_extension M f x" and
    borel_measurable_extension_measurable: "borel_measurable_extension M f ∈ borel_measurable M"
  unfolding borel_measurable_extension_def using assms
  apply -
  using measurable_extensionI apply blast
  using measurable_extensionI2 apply blast
  using measurable_extension_measurable by blast

corollary borel_measurable_measurable_extension_AE:
  fixes f
  assumes "f ∈ borel_measurable M"
  shows "AE x in M. f x = borel_measurable_extension M f x"
  using assms measurable_measurable_extension_AE unfolding borel_measurable_extension_def by auto

definition set_borel_measurable_extension ::
  "'a measure ⇒ 'a set ⇒ ('a ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b"
  where "set_borel_measurable_extension M A f = borel_measurable_extension (restrict_space M A) f"

lemma
  fixes f g :: "'a ⇒ 'b::real_normed_vector" and A
  assumes "A ∈ sets M" "set_borel_measurable M A g" "S ∈ null_sets M" "{x ∈ A. f x ≠ g x} ⊆ S"
  shows set_borel_measurable_extensionI:
    "AE x∈A in M. f x = set_borel_measurable_extension M A f x" and
    set_borel_measurable_extensionI2:
    "AE x∈A in M. g x = set_borel_measurable_extension M A f x" and
    set_borel_measurable_extension_measurable:
    "set_borel_measurable M A (set_borel_measurable_extension M A f)"
proof -
  have "g ∈ borel_measurable (restrict_space M A)"
    using assms by (rewrite set_borel_measurable_restrict_space_iff; simp)
  moreover have "S ∩ A ∈ null_sets (restrict_space M A)"
    using assms null_sets_restrict_space by (metis Int_lower2 null_set_Int2)
  moreover have "{x ∈ space (restrict_space M A). f x ≠ g x} ⊆ S ∩ A"
    using assms by (rewrite space_restrict_space2; simp)
  ultimately show "AE x∈A in M. f x = set_borel_measurable_extension M A f x" and
    "AE x∈A in M. g x = set_borel_measurable_extension M A f x" and
    "set_borel_measurable M A (set_borel_measurable_extension M A f)"
    unfolding set_borel_measurable_extension_def using assms
      apply -
      apply (rewrite AE_restrict_space_iff[THEN sym], simp)
      apply (rule borel_measurable_extensionI[of g _ "S ∩ A"]; simp)
     apply (rewrite AE_restrict_space_iff[THEN sym], simp)
     apply (rule borel_measurable_extensionI2[of g _ "S ∩ A"]; simp)
    apply (rewrite set_borel_measurable_restrict_space_iff[THEN sym], simp)
    by (rule borel_measurable_extension_measurable[of g _ "S ∩ A"]; simp)
qed

corollary set_borel_measurable_measurable_extension_AE:
  fixes f::"'a ⇒ 'b::real_normed_vector" and A
  assumes "set_borel_measurable M A f" "A ∈ sets M"
  shows "AE x∈A in M. f x = set_borel_measurable_extension M A f x"
  using set_borel_measurable_restrict_space_iff
    borel_measurable_measurable_extension_AE AE_restrict_space_iff
  unfolding set_borel_measurable_extension_def
  by (smt (verit) AE_cong sets.Int_space_eq2 assms)

proposition interchange_deriv_LINT_general:
  fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real"
  assumes f_integ: "⋀r. r∈{a<..<b} ⟹ integrable M (f r)" and
    f_diff: "AE x in M. (λr. f r x) differentiable_on {a<..<b}" and
    Df_bound: "AE x in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "integrable M g"
  shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x. f r x ∂M) has_real_derivative
    ∫x. borel_measurable_extension M (λx. deriv (λr. f r x) r) x ∂M) (at r)"
proof -
  text ‹Preparation›
  have f_msr: "⋀r. r∈{a<..<b} ⟹ f r ∈ borel_measurable M" using f_integ by auto
  from f_diff obtain N1 where N1_null: "N1 ∈ null_sets M" and
    "⋀x. x ∈ space M - N1 ⟹ (λs. f s x) differentiable_on {a<..<b}"
    by (smt (verit) AE_E3)
  hence f_diffN1: "⋀x. x ∈ space M - N1 ⟹ (λs. f s x) differentiable_on {a<..<b}"
    by (meson Diff_iff sets.sets_into_space subset_eq)
  from Df_bound obtain N2 where N2_null: "N2 ∈ null_sets M" and
    "⋀x. x ∈ space M - N2 ⟹ ∀r∈{a<..<b}. ¦deriv (λs. f s x) r¦ ≤ g x"
    by (smt (verit) AE_E3)
  hence Df_boundN2:"⋀x. x ∈ space M - N2 ⟹ ∀r∈{a<..<b}. ¦deriv (λs. f s x) r¦ ≤ g x"
    by (meson Diff_iff sets.sets_into_space subset_eq)
  define N where "N ≡ N1 ∪ N2"
  let ?CN = "space M - N"
  have N_null: "N ∈ null_sets M" and N_msr: "N ∈ sets M"
    unfolding N_def using N1_null N2_null by auto
  have f_diffCN: "⋀x. x∈?CN ⟹ (λs. f s x) differentiable_on {a<..<b}"
    unfolding N_def using f_diffN1 by simp
  define Df :: "real ⇒ 'a ⇒ real" where
    "Df r x ≡ indicator ({a<..<b}×?CN) (r,x) * deriv (λs. f s x) r" for r x
  have Df_boundCN: "⋀x. x∈?CN ⟹ ∀r∈{a<..<b}. ¦Df r x¦ ≤ g x"
    unfolding Df_def N_def using Df_boundN2 by simp
  text ‹Main Part of the Proof›
  fix r assume r_ab: "r∈{a<..<b}"
  then obtain e where e_pos: "e > 0" and ball_ab: "ball r e ⊆ {a<..<b}"
    by (meson openE open_greaterThanLessThan)
  have "⋀d::nat⇒real. ⟦∀i. d i ∈ UNIV-{0}; d ⇢ 0⟧ ⟹
    ((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
    ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
  proof -
    fix d::"nat⇒real" assume d_neq0: "∀i. d i ∈ UNIV-{0}" and d_to0: "d ⇢ 0"
    then obtain m where "∀i≥m. ¦d i - 0¦ < e" using LIMSEQ_def e_pos dist_real_def by metis
    hence rd_ab: "⋀n. r + d (n+m) ∈ {a<..<b}" using dist_real_def ball_ab by (simp add: subset_eq)
    hence fd_msr: "⋀n. (λx. (f (r + d (n+m)) x - f r x) / d (n+m)) ∈ borel_measurable M"
      using r_ab by (measurable; (intro f_msr)?; simp)
    hence limf_msr: "(λx. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))) ∈ borel_measurable M"
      by measurable
    moreover have limf_Df: "⋀x. x∈?CN ⟹ (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢ Df r x"
    proof -
      fix x assume x_CN: "x∈?CN"
      hence "(λs. f s x) field_differentiable (at r)"
        using f_diffCN r_ab
        by (metis at_within_open differentiable_on_eq_field_differentiable_real
            open_greaterThanLessThan)
      hence "((λh. (f (r+h) x - f r x) / h) ⤏ Df r x) (at 0)"
        apply (rewrite in asm DERIV_deriv_iff_field_differentiable[THEN sym])
        unfolding Df_def using r_ab x_CN by (simp add: DERIV_def)
      hence "(λi. (f (r + d i) x - f r x) / d i) ⇢ Df r x"
        apply (rewrite in asm tendsto_at_iff_sequentially)
        apply (rule allE'[where x=d], simp)
        unfolding comp_def using d_neq0 d_to0 by simp
      thus "(λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢ Df r x"
        by (rule LIMSEQ_ignore_initial_segment[where k=m])
    qed
    ultimately have Df_eq:
      "⋀x. Df r x = indicator ?CN x * lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))"
    proof -
      fix x
      show "Df r x = indicator ?CN x * lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))"
      proof (cases ‹x∈?CN›)
        case True
        hence "lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x"
          by (intro limI, rule limf_Df)
        thus ?thesis using True by simp
      next
        case False
        thus ?thesis unfolding Df_def by simp
      qed
    qed
    hence Df_msr: "Df r ∈ borel_measurable M"
      apply (rewrite in "λx. ⌑" Df_eq)
      apply (measurable; (rule limf_msr)?)
      using N_null unfolding null_sets_def by force
    have "((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
      ∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M"
    proof -
      have "(λn. ∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M) ⇢
        ∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M"
      proof - ― ‹by Lebesgue's Dominated Convergence Theorem›
        have "AE x in M. (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ⇢
          lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m))"
          using limf_Df Df_eq N_null by (smt (verit) DiffI AE_I' limI mem_Collect_eq subset_eq)
        moreover have "⋀n. AE x in M. norm ((f (r + d (n+m)) x - f r x) / d (n+m)) ≤ g x"
        proof -
          fix n
          { fix x assume x_CN: "x∈?CN"
            let ?I = "{r..(r + d (n+m))} ∪ {(r + d (n+m))..r}"
            have f_diffI: "(λs. f s x) differentiable_on ?I"
              apply (rule differentiable_on_subset[where t="{a<..<b}"], rule f_diffCN, rule x_CN)
              using r_ab rd_ab[of n] by (rewrite Un_subset_iff, auto)
            hence "continuous_on ?I (λs. f s x)" "(λs. f s x) differentiable_on interior ?I"
               apply -
              using differentiable_imp_continuous_on apply blast
              by (metis differentiable_on_subset interior_subset)
            then obtain t where t_01: "t∈{0<..<1}" and
              f_MVT: "f (r + d (n+m)) x - f r x = d (n+m) * deriv (λs. f s x) (r + t * (d (n+m)))"
              by (rule MVT_order_free)
            hence "0 < t" "t < 1" by simp_all
            hence rtd_ab: "r + t * (d (n+m)) ∈ {a<..<b}"
              using r_ab rd_ab[of n]
              by simp (smt (verit, ccfv_threshold) mult_less_cancel_left mult_less_cancel_right2)
            have "d (n+m) * deriv (λs. f s x) (r + t * (d (n+m))) =
              d (n+m) * Df (r + t * (d (n+m))) x"
            proof -
              have "r + t * (d (n+m)) ∈ {a<..<b}"
                using r_ab rd_ab[of n] t_01
                by (smt (verit) ball_eq_greaterThanLessThan dist_real_def
                    greaterThanLessThan_eq_iff greaterThanLessThan_eq_ball mem_ball
                    mult_le_cancel_right1 mult_minus_right mult_pos_neg)
              thus ?thesis unfolding Df_def using x_CN by simp
            qed
            with f_MVT have "(f (r + d (n+m)) x - f r x) / d (n+m) = Df (r + t * (d (n+m))) x"
              using d_neq0 by simp
            moreover have "¦Df (r + t * (d (n+m))) x¦ ≤ g x" using Df_boundCN x_CN rtd_ab by simp
            ultimately have "¦(f (r + d (n+m)) x - f r x) / d (n+m)¦ ≤ g x" by simp }
          thus "AE x in M. norm ((f (r + d (n+m)) x - f r x) / d (n+m)) ≤ g x"
            unfolding real_norm_def using AE_I' N_null
            by (smt (verit, ccfv_threshold) Diff_iff mem_Collect_eq subsetI)
        qed
        ultimately show "((λn. ∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M) ⇢
          ∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M)" 
          using limf_msr fd_msr Df_bound
          by (intro integral_dominated_convergence[where w=g], simp_all)
      qed
      moreover have "⋀n. ((∫x. f (r + d (n+m)) x ∂M) - ∫x. f r x ∂M) / d (n+m) =
        ∫x. (f (r + d (n+m)) x - f r x) / d (n+m) ∂M"
        using d_neq0 apply simp
        by (rewrite Bochner_Integration.integral_diff;
            (rule f_integ | simp); (rule rd_ab | rule r_ab))
      ultimately show ?thesis
        unfolding comp_def using d_neq0
        apply -
        by (rule LIMSEQ_offset[where k=m]) simp
    qed
    moreover have "(∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M) =
      ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
    proof -
      have "(∫x. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) ∂M) = ∫x. Df r x ∂M"
      proof -
        have "AE x in M. lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x"
        proof -
          { fix x assume x_CN: "x∈?CN"
            hence "lim (λn. (f (r + d (n+m)) x - f r x) / d (n+m)) = Df r x" by (simp add: Df_eq) }
          thus ?thesis using AE_I' N_null by (smt (verit, del_insts) DiffI mem_Collect_eq subsetI)
        qed
        thus ?thesis using limf_msr Df_msr by (intro integral_cong_AE; simp)
      qed
      also have "… = ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
      proof -
        have "AE x in M. Df r x = borel_measurable_extension M (λy. deriv (λs. f s y) r) x" and
          "borel_measurable_extension M (λy. deriv (λs. f s y) r) ∈ borel_measurable M"
        proof -
          have "{x ∈ space M. deriv (λs. f s x) r ≠ Df r x} ⊆ N"
          proof -
            { fix x assume "x∈?CN"
              hence "deriv (λs. f s x) r = Df r x" unfolding Df_def using r_ab by simp }
            thus ?thesis by blast
          qed
          thus "AE x in M. Df r x = borel_measurable_extension M (λy. deriv (λs. f s y) r) x" and
            "borel_measurable_extension M (λy. deriv (λs. f s y) r) ∈ borel_measurable M"
            using Df_msr N_null
             apply -
             apply (rule borel_measurable_extensionI2[where S=N]; simp)
            by (rule borel_measurable_extension_measurable[where g="Df r"]; simp)
        qed
        thus ?thesis using Df_msr by (intro integral_cong_AE; simp)
      qed
      finally show ?thesis .
    qed
    ultimately show "((λh. ((∫x. f (r+h) x ∂M) - ∫x. f r x ∂M) / h) ∘ d) ⇢
      ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M"
      using tendsto_cong_limit by simp
  qed
  thus "((λs. ∫x. f s x ∂M) has_real_derivative
    ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M) (at r)"
    by (rewrite DERIV_def, rewrite tendsto_at_iff_sequentially) simp
qed

proposition interchange_deriv_LINT:
  fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real"
  assumes "⋀r. r∈{a<..<b} ⟹ integrable M (f r)" and
    "AE x in M. (λr. f r x) differentiable_on {a<..<b}" and
    "⋀r. r∈{a<..<b} ⟹ (λx. (deriv (λr. f r x) r)) ∈ borel_measurable M" and
    "AE x in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "integrable M g"
  shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x. f r x ∂M) has_real_derivative
    ∫x. deriv (λr. f r x) r ∂M) (at r)"
proof -
  fix r assume r_ab: "r∈{a<..<b}"
  hence Df_msr: "(λx. deriv (λs. f s x) r) ∈ borel_measurable M" using assms by simp
  have "((λs. ∫x. f s x ∂M) has_real_derivative
    ∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M) (at r)"
    using assms r_ab by (intro interchange_deriv_LINT_general; simp)
  moreover have "(∫x. borel_measurable_extension M (λy. deriv (λs. f s y) r) x ∂M) =
    ∫x. deriv (λs. f s x) r ∂M"
    apply (rule integral_cong_AE)
      apply (rule borel_measurable_extension_measurable
        [where g="λy. deriv (λs. f s y) r" and S="{}"], simp_all add: Df_msr)
    using borel_measurable_measurable_extension_AE Df_msr by (smt (verit) AE_cong)
  ultimately show "((λr. ∫x. f r x ∂M) has_real_derivative ∫x. deriv (λr. f r x) r ∂M) (at r)"
    by simp
qed

proposition interchange_deriv_LINT_set_general:
  fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real" and A :: "'a set"
  assumes A_msr: "A ∈ sets M" and
    f_integ: "⋀r. r∈{a<..<b} ⟹ set_integrable M A (f r)" and
    f_diff: "AE x∈A in M. (λr. f r x) differentiable_on {a<..<b}" and
    Df_bound: "AE x∈A in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "set_integrable M A g"
  shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
    (∫x∈A. set_borel_measurable_extension M A (λx. deriv (λr. f r x) r) x ∂M)) (at r)"
proof -
  let ?M_A = "restrict_space M A"
  have "⋀r. r∈{a<..<b} ⟹ integrable ?M_A (f r)"
    using A_msr f_integ set_integrable_restrict_space_iff by auto
  moreover have "AE x in ?M_A. (λr. f r x) differentiable_on {a<..<b}"
    using AE_restrict_space_iff A_msr f_diff by (metis sets.Int_space_eq2)
  moreover have "AE x in ?M_A. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" and
    "integrable ?M_A g"
    using A_msr Df_bound set_integrable_restrict_space_iff
     apply -
    by (simp add: AE_restrict_space_iff, auto)
  ultimately have "⋀r. r∈{a<..<b} ⟹ ((λr. integral⇧L ?M_A (f r)) has_real_derivative
    integral⇧L ?M_A (borel_measurable_extension ?M_A (λx. deriv (λr. f r x) r))) (at r)"
    by (rule interchange_deriv_LINT_general[where M="restrict_space M A"]) auto
  thus "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
    (∫x∈A. set_borel_measurable_extension M A (λx. deriv (λr. f r x) r) x ∂M)) (at r)"
    unfolding set_borel_measurable_extension_def using assms 
    by (rewrite set_lebesgue_integral_restrict_space, simp)+
qed

proposition interchange_deriv_LINT_set:
  fixes a b :: real and f :: "real ⇒ 'a ⇒ real" and g :: "'a ⇒ real" and A :: "'a set"
  assumes "A ∈ sets M" and
    "⋀r. r∈{a<..<b} ⟹ set_integrable M A (f r)" and
    "AE x∈A in M. (λr. f r x) differentiable_on {a<..<b}" and
    "⋀r. r∈{a<..<b} ⟹ set_borel_measurable M A (λx. (deriv (λr. f r x) r))" and
    "AE x∈A in M. ∀r∈{a<..<b}. ¦deriv (λr. f r x) r¦ ≤ g x" "set_integrable M A g"
  shows "⋀r. r∈{a<..<b} ⟹ ((λr. ∫x∈A. f r x ∂M) has_real_derivative
    (∫x∈A. deriv (λr. f r x) r ∂M)) (at r)"
proof -
  fix r assume r_ab: "r∈{a<..<b}"
  hence Df_msr: "set_borel_measurable M A (λx. deriv (λs. f s x) r)" using assms by simp
  have "((λs. ∫x∈A. f s x ∂M) has_real_derivative
    (∫x∈A. set_borel_measurable_extension M A (λy. deriv (λs. f s y) r) x ∂M)) (at r)"
    using assms r_ab by (intro interchange_deriv_LINT_set_general; simp)
  moreover have "(∫x∈A. set_borel_measurable_extension M A (λy. deriv (λs. f s y) r) x ∂M) =
    (∫x∈A. deriv (λs. f s x) r ∂M)"
    apply (rule set_lebesgue_integral_cong_AE2, simp add: assms)
      apply (rule set_borel_measurable_extension_measurable
        [where g="λy. deriv (λs. f s y) r" and S="{}"], simp_all add: Df_msr assms)
    using set_borel_measurable_measurable_extension_AE Df_msr assms by (smt (verit) AE_cong)
  ultimately show
    "((λr. ∫x∈A. f r x ∂M) has_real_derivative (∫x∈A. deriv (λr. f r x) r ∂M)) (at r)"
    by simp
qed

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

lemma (in finite_borel_measure)
  fixes F :: "real ⇒ real"
  assumes nondecF : "⋀ x y. x ≤ y ⟹ F x ≤ F y" and
    right_cont_F : "⋀a. continuous (at_right a) F" and
    lim_F_at_bot : "(F ⤏ 0) at_bot" and
    lim_F_at_top : "(F ⤏ m) at_top" and
    m : "0 ≤ m"
  shows emeasure_interval_measure_Ioi: "emeasure (interval_measure F) {x<..} = m - F x"
    and measure_interval_measure_Ioi: "measure (interval_measure F) {x<..} = m - F x"
proof -
  interpret F_FM: finite_measure "interval_measure F"
    using finite_borel_measure.axioms(1) finite_borel_measure_interval_measure lim_F_at_bot
      lim_F_at_top m nondecF right_cont_F by blast
  have "UNIV = {..x} ∪ {x<..}" by auto
  moreover have "{..x} ∩ {x<..} = {}" by auto
  ultimately have "emeasure (interval_measure F) UNIV =
    emeasure (interval_measure F) {..x} + emeasure (interval_measure F) {x<..}"
    by (simp add: plus_emeasure)
  moreover have "emeasure (interval_measure F) UNIV = m"
    using assms interval_measure_UNIV by presburger
  ultimately show ⋆: "emeasure (interval_measure F) {x<..} = m - F x"
    using assms emeasure_interval_measure_Iic
    by (metis ennreal_add_diff_cancel_left ennreal_minus measure_interval_measure_Iic
        measure_nonneg top_neq_ennreal)
  hence "ennreal (measure (interval_measure F) {x<..}) = m - F x"
    using emeasure_eq_measure by (metis emeasure_eq_ennreal_measure top_neq_ennreal)
  moreover have "⋀x. F x ≤ m"
    using lim_F_at_top nondecF by (intro mono_at_top_le[where f=F]; simp add: mono_def)
  ultimately show "measure (interval_measure F) {x<..} = m - F x"
    using ennreal_inj F_FM.emeasure_eq_measure by force
qed

lemma (in prob_space) cond_prob_nonneg[simp]: "cond_prob M P Q ≥ 0"
  by (auto simp: cond_prob_def)

lemma (in prob_space) cond_prob_whole_1: "cond_prob M P P = 1" if "prob {ω ∈ space M. P ω} ≠ 0"
  unfolding cond_prob_def using that by simp

lemma (in prob_space) cond_prob_0_null: "cond_prob M P Q = 0" if "prob {ω ∈ space M. Q ω} = 0"
  unfolding cond_prob_def using that by simp

lemma (in prob_space) cond_prob_AE_prob:
  assumes "{ω ∈ space M. P ω} ∈ events" "{ω ∈ space M. Q ω} ∈ events"
    and "AE ω in M. Q ω"
  shows "cond_prob M P Q = prob {ω ∈ space M. P ω}"
proof -
  let ?setP = "{ω ∈ space M. P ω}"
  let ?setQ = "{ω ∈ space M. Q ω}"
  have [simp]: "prob ?setQ = 1" using assms prob_Collect_eq_1 by simp
  hence "cond_prob M P Q = prob (?setP ∩ ?setQ)"
    unfolding cond_prob_def by (simp add: Collect_conj_eq2)
  also have "… = prob ?setP"
  proof (rule antisym)
    show "prob (?setP ∩ ?setQ) ≤ prob ?setP"
      using assms finite_measure_mono inf_sup_ord(1) by blast
  next
    show "prob ?setP ≤ prob (?setP ∩ ?setQ)"
    proof -
      have "prob (?setP ∩ ?setQ) = prob ?setP + prob ?setQ - prob (?setP ∪ ?setQ)"
        using assms by (smt (verit) finite_measure_Diff' finite_measure_Union' sup_commute)
      also have "… = prob ?setP + (1 - prob (?setP ∪ ?setQ))" by simp
      also have "… ≥ prob ?setP" by simp
      finally show ?thesis .
    qed
  qed
  finally show ?thesis .
qed

subsection ‹More Properties of ‹cdf›'s›

context finite_borel_measure
begin

lemma cdf_diff_eq2:
  assumes "x ≤ y"
  shows "cdf M y - cdf M x = measure M {x<..y}"
proof (cases ‹x = y›)
  case True
  thus ?thesis by force
next 
  case False
  hence "x < y" using assms by simp
  thus ?thesis by (rule cdf_diff_eq)
qed

end

context prob_space
begin

lemma cdf_distr_measurable [measurable]:
  assumes [measurable]: "random_variable borel X"
  shows "cdf (distr M borel X) ∈ borel_measurable borel"
proof (rule borel_measurable_mono)
  show "mono (cdf (distr M borel X))"
    unfolding mono_def
    using finite_borel_measure.cdf_nondecreasing
    by (simp add: real_distribution.finite_borel_measure_M)
qed

lemma cdf_distr_P:
  assumes "random_variable borel X"
  shows "cdf (distr M borel X) x = 𝒫(ω in M. X ω ≤ x)"
  unfolding cdf_def apply (rewrite measure_distr; (simp add: assms)?)
  unfolding vimage_def by (rule arg_cong[where f=prob], force)

lemma cdf_continuous_distr_P_lt:
  assumes "random_variable borel X" "isCont (cdf (distr M borel X)) x"
  shows "cdf (distr M borel X) x = 𝒫(ω in M. X ω < x)"
proof -
  have "𝒫(ω in M. X ω < x) = measure (distr M borel X) {..<x}"
    apply (rewrite measure_distr, simp_all add: assms)
    unfolding vimage_def by simp (smt (verit) Collect_cong Int_def mem_Collect_eq)
  also have "… = measure (distr M borel X) ({..<x} ∪ {x})"
    apply (rewrite finite_measure.measure_zero_union, simp_all add: assms finite_measure_distr)
    using finite_borel_measure.isCont_cdf real_distribution.finite_borel_measure_M assms by blast
  also have "… = measure (distr M borel X) {..x}" by (metis ivl_disj_un_singleton(2))
  also have "… = cdf (distr M borel X) x" unfolding cdf_def by simp
  finally show ?thesis by simp
qed

lemma cdf_distr_diff_P:
  assumes "x ≤ y"
    and "random_variable borel X"
  shows "cdf (distr M borel X) y - cdf (distr M borel X) x = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  have "cdf (distr M borel X) y - cdf (distr M borel X) x = measure (distr M borel X) {x<..y}"
    by (rewrite distrX_FBM.cdf_diff_eq2; simp add: assms)
  also have "… = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
    apply (rewrite measure_distr; (simp add: assms)?)
    unfolding vimage_def by (rule arg_cong[where f=prob], force)
  finally show ?thesis .
qed

lemma cdf_distr_max:
  fixes c::real
  assumes [measurable]: "random_variable borel X"
  shows "cdf (distr M borel (λx. max (X x) c)) u = cdf (distr M borel X) u * indicator {c..} u"
proof (cases ‹c ≤ u›)
  case True
  thus ?thesis
    unfolding cdf_def
    apply (rewrite measure_distr; simp?)+
    by (smt (verit) Collect_cong atMost_iff vimage_def)
next
  case False
  thus ?thesis
    unfolding cdf_def
    apply (rewrite measure_distr; simp?)+
    by (smt (verit, best) Int_emptyI atMost_iff measure_empty vimage_eq)
qed

lemma cdf_distr_min:
  fixes c::real
  assumes [measurable]: "random_variable borel X"
  shows "cdf (distr M borel (λx. min (X x) c)) u =
    1 - (1 - cdf (distr M borel X) u) * indicator {..<c} u"
proof (cases ‹c ≤ u›)
  case True
  thus ?thesis
    unfolding cdf_def
    using real_distribution.finite_borel_measure_M real_distribution_distr
    apply (rewrite measure_distr; simp?)
    by (smt (verit, del_insts) Int_absorb1 atMost_iff prob_space subset_vimage_iff)
next
  case False
  thus ?thesis
    unfolding cdf_def
    using real_distribution.finite_borel_measure_M real_distribution_distr
    apply (rewrite measure_distr; simp?)+
    using prob_space_axioms assms
    by (smt (verit) Collect_cong Int_def atMost_iff prob_space prob_space.cdf_distr_P vimage_eq)
qed

lemma cdf_distr_floor_P:
  fixes X :: "'a ⇒ real"
  assumes [measurable]: "random_variable borel X"
  shows "cdf (distr M borel (λx. ⌊X x⌋)) u = 𝒫(x in M. X x < ⌊u⌋ + 1)"
  unfolding cdf_def
  apply (rewrite measure_distr; simp?)
  apply (rule arg_cong[where f=prob])
  unfolding vimage_def using floor_le_iff le_floor_iff by blast

lemma expectation_nonneg_tail:
  assumes [measurable]: "random_variable borel X"
    and X_nonneg: "⋀x. x ∈ space M ⟹ X x ≥ 0"
  defines "F u ≡ cdf (distr M borel X) u"
  shows "(∫⇧+x. ennreal (X x) ∂M) = (∫⇧+u∈{0..}. ennreal (1 - F u) ∂lborel)"
proof -
  let ?distrX = "distr M borel X"
  have "(∫⇧+x. ennreal (X x) ∂M) = (∫⇧+u. ennreal u ∂?distrX)"
    by (rewrite nn_integral_distr; simp)
  also have "… = (∫⇧+u∈{0..}. ennreal u ∂?distrX)"
    by (rule nn_integral_distr_set; simp add: X_nonneg)
  also have "… = (∫⇧+u∈{0..}. (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel) ∂?distrX)"
  proof -
    have "⋀u::real. u∈{0..} ⟹ ennreal u = (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel)"
      apply (rewrite indicator_inter_arith[THEN sym])
      apply (rewrite nn_integral_indicator, measurable, simp)
      by (metis atLeastLessThan_def diff_zero emeasure_lborel_Ico inf.commute)
    thus ?thesis by (metis (no_types, lifting) indicator_eq_0_iff mult_eq_0_iff)
  qed
  also have "… = (∫⇧+v∈{0..}. (∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) ∂lborel)"
  proof -
    have "(∫⇧+u∈{0..}. (∫⇧+v∈{0..}. indicator {..<u} v ∂lborel) ∂?distrX) =
      ∫⇧+u. (∫⇧+v. indicator {..<u} v * indicator {0..} v * indicator {0..} u ∂lborel) ∂?distrX"
      by (rewrite nn_integral_multc; simp)
    also have "… =
      ∫⇧+v. (∫⇧+u. indicator {..<u} v * indicator {0..} v * indicator {0..} u ∂?distrX) ∂lborel"
      apply (rewrite pair_sigma_finite.Fubini'; simp?)
      using pair_sigma_finite.intro assms
        prob_space_distr prob_space_imp_sigma_finite sigma_finite_lborel
       apply blast
      by measurable auto
    also have "… = (∫⇧+v∈{0..}. (∫⇧+u∈{0..}. indicator {..<u} v ∂?distrX) ∂lborel)"
      apply (rewrite nn_integral_multc[THEN sym]; measurable; simp?)
      apply (rule nn_integral_cong)+ 
      using mult.assoc mult.commute by metis
    finally show ?thesis by simp
  qed
  also have "… = (∫⇧+v∈{0..}. (∫⇧+u. indicator {v<..} u ∂?distrX) ∂lborel)"
    apply (rule nn_integral_cong)
    apply (rewrite nn_integral_multc[THEN sym], measurable; (simp del: nn_integral_indicator)?)+
    apply (rule nn_integral_cong)
    using lessThan_iff greaterThan_iff atLeast_iff indicator_simps
    by (smt (verit, del_insts) mult_1 mult_eq_0_iff)
  also have "… = (∫⇧+v∈{0..}. ennreal (1 - F v) ∂lborel)"
    apply (rule nn_integral_cong, simp)
    apply (rewrite emeasure_distr; simp?)
    apply (rewrite vimage_compl_atMost[THEN sym])
    unfolding F_def cdf_def
    apply (rewrite measure_distr; simp?)
    apply (rewrite prob_compl[THEN sym], simp)
    by (metis (no_types, lifting) Diff_Compl Diff_Diff_Int Int_commute emeasure_eq_measure)
  finally show ?thesis .
qed

lemma expectation_nonpos_tail:
  assumes [measurable]: "random_variable borel X"
    and X_nonpos: "⋀x. x ∈ space M ⟹ X x ≤ 0"
  defines "F u ≡ cdf (distr M borel X) u"
  shows "(∫⇧+x. ennreal (- X x) ∂M) = (∫⇧+u∈{..0}. ennreal (F u) ∂lborel)"
proof -
  let ?distrX = "distr M borel X"
  have "(∫⇧+x. ennreal (- X x) ∂M) = (∫⇧+u. ennreal (-u) ∂?distrX)"
    by (rewrite nn_integral_distr; simp)
  also have "… = (∫⇧+u∈{..0}. ennreal (-u) ∂?distrX)"
  proof -
    have [simp]: "{..0::real} ∪ {0<..} = UNIV" by force
    have "(∫⇧+u. ennreal (-u) ∂?distrX) =
      (∫⇧+u∈{..0}. ennreal (-u) ∂?distrX) + (∫⇧+u∈{0<..}. ennreal (-u) ∂?distrX)"
      by (rewrite nn_integral_disjoint_pair[THEN sym], simp_all, force)
    also have "… = (∫⇧+u∈{..0}. ennreal (-u) ∂?distrX)"
      apply (rewrite nn_integral_zero'[of "λu. ennreal (-u) * indicator {0<..} u"]; simp?)
      unfolding indicator_def using always_eventually ennreal_lt_0 by force
    finally show ?thesis .
  qed
  also have "… = (∫⇧+u∈{..0}. (∫⇧+v∈{..0}. indicator {u..} v ∂lborel) ∂?distrX)"
  proof -
    have "⋀u::real. u∈{..0} ⟹ ennreal (-u) = (∫⇧+v∈{..0}. indicator {u..} v ∂lborel)"
      by (rewrite indicator_inter_arith[THEN sym]) simp
    thus ?thesis by (metis (no_types, lifting) indicator_eq_0_iff mult_eq_0_iff)
  qed
  also have "… = (∫⇧+v∈{..0}. (∫⇧+u∈{..0}. indicator {u..} v ∂?distrX) ∂lborel)"
  proof -
    have "(∫⇧+u∈{..0}. (∫⇧+v∈{..0}. indicator {u..} v ∂lborel) ∂?distrX) =
      ∫⇧+u. (∫⇧+v. indicator {u..} v * indicator {..0} v * indicator {..0} u ∂lborel) ∂?distrX"
      by (rewrite nn_integral_multc; simp)
    also have "… =
      ∫⇧+v. (∫⇧+u. indicator {u..} v * indicator {..0} v * indicator {..0} u ∂?distrX) ∂lborel"
      apply (rewrite pair_sigma_finite.Fubini'; simp?)
      using pair_sigma_finite.intro assms
        prob_space_distr prob_space_imp_sigma_finite sigma_finite_lborel
       apply blast
      by measurable auto
    also have "… = (∫⇧+v∈{..0}. (∫⇧+u∈{..0}. indicator {u..} v ∂?distrX) ∂lborel)"
      apply (rewrite nn_integral_multc[THEN sym]; measurable; simp?)
      apply (rule nn_integral_cong)+ 
      using mult.assoc mult.commute by metis
    finally show ?thesis by simp
  qed
  also have "… = (∫⇧+v∈{..0}. (∫⇧+u. indicator {..v} u ∂?distrX) ∂lborel)"
    apply (rule nn_integral_cong)
    apply (rewrite nn_integral_multc[THEN sym], measurable; (simp del: nn_integral_indicator)?)+
    apply (rule nn_integral_cong)
    using atMost_iff atLeast_iff indicator_simps by (smt (verit, del_insts) mult_1 mult_eq_0_iff)
  also have "… = (∫⇧+v∈{..0}. ennreal (F v) ∂lborel)"
    apply (rule nn_integral_cong, simp)
    apply (rewrite emeasure_distr; simp?)
    unfolding F_def cdf_def
    by (rewrite measure_distr; simp add: emeasure_eq_measure)
  finally show ?thesis .
qed

proposition expectation_tail:
  assumes [measurable]: "integrable M X"
  defines "F u ≡ cdf (distr M borel X) u"
  shows "expectation X = (LBINT u:{0..}. 1 - F u) - (LBINT u:{..0}. F u)"
proof -
  have "expectation X = expectation (λx. max (X x) 0) + expectation (λx. min (X x) 0)"
    using integrable_max integrable_min
    apply (rewrite Bochner_Integration.integral_add[THEN sym], measurable)
    by (rule Bochner_Integration.integral_cong; simp)
  also have "… = expectation (λx. max (X x) 0) - expectation (λx. - min (X x) 0)" by force
  also have "… = (LBINT u:{0..}. 1 - F u) - (LBINT u:{..0}. F u)"
  proof -
    have "expectation (λx. max (X x) 0) = (LBINT u:{0..}. 1 - F u)"
    proof -
      have "expectation (λx. max (X x) 0) = enn2real (∫⇧+x. ennreal (max (X x) 0) ∂M)"
        by (rule integral_eq_nn_integral; simp)
      also have "… = enn2real (∫⇧+u∈{0..}. ennreal (1 - F u) ∂lborel)"
        apply (rewrite expectation_nonneg_tail; simp?)
        apply (rewrite cdf_distr_max, simp)
        unfolding F_def
        by (metis (opaque_lifting) indicator_simps mult.commute mult_1 mult_eq_0_iff)
      also have "… = enn2real (∫⇧+u. ennreal ((1 - F u) * indicator {0..} u) ∂lborel)"
        by (simp add: indicator_mult_ennreal mult.commute)
      also have "… = (LBINT u:{0..}. 1 - F u)"
        apply (rewrite integral_eq_nn_integral[THEN sym], simp add: F_def)
        unfolding F_def using real_distribution.cdf_bounded_prob apply force
        unfolding set_lebesgue_integral_def by (rule Bochner_Integration.integral_cong; simp)
      finally show ?thesis .
    qed
    moreover have "expectation (λx. - min (X x) 0) = (LBINT u:{..0}. F u)"
    proof -
      have "expectation (λx. - min (X x) 0) = enn2real (∫⇧+x. ennreal (- min (X x) 0) ∂M)"
        by (rule integral_eq_nn_integral; simp)
      also have "… = enn2real (∫⇧+u∈{..0}. ennreal (F u) ∂lborel)"
      proof -
        let ?distrminX = "distr M borel (λx. min (X x) 0)"
        have [simp]: "sym_diff {..0} {..<0} = {0::real}" by force
        have "enn2real (∫⇧+x. ennreal (- min (X x) 0) ∂M) =
      enn2real (∫⇧+u∈{..0}. ennreal (cdf ?distrminX u) ∂lborel)"
          by (rewrite expectation_nonpos_tail; simp)
        also have "… = enn2real (∫⇧+u∈{..<0}. ennreal (cdf ?distrminX u) ∂lborel)"
          by (rewrite nn_integral_null_delta, auto)
        also have "… = enn2real (∫⇧+u∈{..<0}. ennreal (F u) ∂lborel)"
          apply (rewrite cdf_distr_min, simp)
          apply (rule arg_cong[where f=enn2real], rule nn_integral_cong)
          unfolding F_def by (smt (verit) indicator_simps mult_cancel_left1 mult_eq_0_iff)
        also have "… = enn2real (∫⇧+u∈{..0}. ennreal (F u) ∂lborel)"
          by (rewrite nn_integral_null_delta, auto simp add: sup_commute)
        finally show ?thesis .
      qed
      also have "… = enn2real (∫⇧+u. ennreal (F u * indicator {..0} u) ∂lborel)"
        using mult.commute indicator_mult_ennreal by metis
      also have "… = (LBINT u:{..0}. F u)"
        apply (rewrite integral_eq_nn_integral[THEN sym], simp add: F_def)
        unfolding F_def
        using finite_borel_measure.cdf_nonneg real_distribution.finite_borel_measure_M apply simp
        unfolding set_lebesgue_integral_def by (rule Bochner_Integration.integral_cong; simp)
      finally show ?thesis .
    qed
    ultimately show ?thesis by simp
  qed
  finally show ?thesis .
qed

proposition distributed_deriv_cdf:
  assumes [measurable]: "random_variable borel X"
  defines "F u ≡ cdf (distr M borel X) u"
  assumes "finite S" "⋀x. x ∉ S ⟹ (F has_real_derivative f x) (at x)"
    and "continuous_on UNIV F" "f ∈ borel_measurable lborel"
  shows "distributed M lborel X f"
proof -
  have FBM: "finite_borel_measure (distr M borel X)"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  then interpret distrX_FBM: finite_borel_measure "distr M borel X" .
  have FBMl: "finite_borel_measure (distr M lborel X)" using FBM distr_borel_lborel by (smt (verit))
  then interpret distrlX_FBM: finite_borel_measure "distr M lborel X" .
  have [simp]: "(λx. ennreal (f x)) ∈ borel_measurable borel" using assms by simp
  moreover have "distr M lborel X = density lborel f"
  proof -
    have "⋀a b. a ≤ b ⟹ emeasure (distr M lborel X) {a<..b} < ⊤"
      using distrlX_FBM.emeasure_real less_top_ennreal by blast
    moreover have "⋀a b. a ≤ b ⟹
      emeasure (distr M lborel X) {a<..b} = emeasure (density lborel f) {a<..b}"
    proof -
      fix a b :: real assume "a ≤ b"
      hence [simp]: "sym_diff {a<..b} {a..b} = {a}" by force
      have "emeasure (density lborel f) {a<..b} = (∫⇧+x∈{a<..b}. ennreal (f x) ∂lborel)"
        by (rewrite emeasure_density; simp)
      also have "… = (∫⇧+x∈{a..b}. ennreal (f x) ∂lborel)" by (rewrite nn_integral_null_delta, auto)
      also have "… = ∫⇧+x. ennreal (indicat_real {a..b} x * f x) ∂lborel"
        by (metis indicator_mult_ennreal mult.commute)
      also have "… = ennreal (F b - F a)"
      proof -
        define g where "g x = (if x ∈ S then 0 else f x)" for x :: real
        have [simp]: "⋀x. g x ≥ 0"
          unfolding g_def
          apply (split if_split, auto)
          apply (rule mono_on_imp_deriv_nonneg[of UNIV F], auto)
          unfolding F_def mono_on_def using distrX_FBM.cdf_nondecreasing apply blast
          using assms unfolding F_def by force
        have "(∫⇧+x. ennreal (indicat_real {a..b} x * f x) ∂lborel)
          = ∫⇧+x. ennreal (indicat_real {a..b} x * g x) ∂lborel"
          apply (rule nn_integral_cong_AE)
          apply (rule AE_mp[where P= "λx. x ∉ S"])
          using assms finite_imp_null_set_lborel AE_not_in apply blast
          unfolding g_def by simp
        also have "… = ennreal (F b - F a)"
          apply (rewrite nn_integral_has_integral_lebesgue, simp)
           apply (rule fundamental_theorem_of_calculus_strong[of S], auto simp: ‹a ≤ b› g_def assms)
          using has_real_derivative_iff_has_vector_derivative assms apply presburger
          using assms continuous_on_subset subsetI by fastforce
        finally show ?thesis .
      qed
      also have "… = emeasure (distr M lborel X) {a <.. b}"
        apply (rewrite distrlX_FBM.emeasure_Ioc, simp add: ‹a ≤ b›)
        unfolding F_def cdf_def
        apply (rewrite ennreal_minus[THEN sym], simp)+
        by (metis distr_borel_lborel)
      finally show "emeasure (distr M lborel X) {a<..b} = emeasure (density lborel f) {a<..b}"
        by simp
    qed
    ultimately show ?thesis by (intro measure_eqI_Ioc; simp)
  qed
  ultimately show ?thesis unfolding distributed_def by auto
qed

end

text ‹
  Define the conditional probability space.
  This is obtained by rescaling the restricted space of a probability space.
›

subsection ‹Conditional Probability Space›

lemma restrict_prob_space:
  assumes "measure_space Ω A μ" "a ∈ A"
    and "0 < μ a" "μ a < ∞"
  shows "prob_space (scale_measure (1 / μ a) (restrict_space (measure_of Ω A μ) a))"
proof
  let ?M = "measure_of Ω A μ"
  let ?Ma = "restrict_space ?M a"
  let ?rMa = "scale_measure (1 / μ a) ?Ma"
  have "emeasure ?rMa (space ?rMa) = 1 / μ a * emeasure ?Ma (space ?rMa)" by simp
  also have "… = 1 / μ a * emeasure ?M (space ?rMa)"
    using assms
    apply (rewrite emeasure_restrict_space)
    apply (simp add: measure_space_def sigma_algebra.sets_measure_of_eq)
    by (simp add: space_restrict_space space_scale_measure) simp
  also have "… = 1 / μ a * emeasure ?M (space ?Ma)" by (rewrite space_scale_measure) simp
  also have "… = 1 / μ a * emeasure ?M a"
    using assms
    apply (rewrite space_restrict_space2)
    by (simp add: measure_space_closed)+
  also have "… = 1"
    using assms measure_space_def
    apply (rewrite emeasure_measure_of_sigma, blast+)
    by (simp add: ennreal_divide_times)
  finally show "emeasure ?rMa (space ?rMa) = 1" .
qed

definition cond_prob_space :: "'a measure ⇒ 'a set ⇒ 'a measure" (infix ‹⇂› 200)
  where "M⇂A ≡ scale_measure (1 / emeasure M A) (restrict_space M A)"

context prob_space
begin

lemma cond_prob_space_whole[simp]: "M ⇂ space M = M"
  unfolding cond_prob_space_def using emeasure_space_1 by simp

lemma cond_prob_space_correct:
  assumes "A ∈ events" "prob A > 0"
  shows "prob_space (M⇂A)"
  unfolding cond_prob_space_def
  apply (subst(2) measure_of_of_measure[of M, THEN sym])
  using assms
  by (intro restrict_prob_space; (simp add: measure_space)?; simp_all add: emeasure_eq_measure)

lemma space_cond_prob_space:
  assumes "A ∈ events"
  shows "space (M⇂A) = A"
  unfolding cond_prob_space_def using assms by (simp add: space_scale_measure)

lemma sets_cond_prob_space: "sets (M⇂A) = (∩) A ` events"
  unfolding cond_prob_space_def by (metis sets_restrict_space sets_scale_measure)

lemma measure_cond_prob_space:
  assumes "A ∈ events" "B ∈ events"
    and "prob A > 0"
  shows "measure (M⇂A) (B ∩ A) = prob (B ∩ A) / prob A"
proof -
  have "1 / emeasure M A = ennreal (1 / prob A)"
    using assms by (smt (verit) divide_ennreal emeasure_eq_measure ennreal_1)
  hence "measure (M⇂A) (B ∩ A) = (1 / prob A) * measure (restrict_space M A) (B ∩ A)"
    unfolding cond_prob_space_def using measure_scale_measure by force
  also have "… = (1 / prob A) * prob (B ∩ A)"
    using measure_restrict_space assms by (metis inf.cobounded2 sets.Int_space_eq2)
  also have "… = prob (B ∩ A) / prob A" by simp
  finally show ?thesis .
qed

corollary measure_cond_prob_space_subset:
  assumes "A ∈ events" "B ∈ events" "B ⊆ A"
    and "prob A > 0"
  shows "measure (M⇂A) B = prob B / prob A"
proof -
  have "B = B ∩ A" using assms by auto
  moreover have "measure (M⇂A) (B ∩ A) = prob (B ∩ A) / prob A"
    using assms measure_cond_prob_space by simp
  ultimately show ?thesis by auto
qed

lemma cond_cond_prob_space:
  assumes "A ∈ events" "B ∈ events" "B ⊆ A" "prob B > 0"
  shows "(M⇂A)⇂B = M⇂B"
proof (rule measure_eqI)
  have pA_pos[simp]: "prob A > 0" using assms by (smt (verit, ccfv_SIG) finite_measure_mono)
  interpret MA_PS: prob_space "M⇂A" using cond_prob_space_correct assms by simp
  interpret MB_PS: prob_space "M⇂B" using cond_prob_space_correct assms by simp
  have "1 / emeasure M A = ennreal (1 / prob A)"
    using pA_pos by (smt (verit, ccfv_SIG) divide_ennreal emeasure_eq_measure ennreal_1)
  hence [simp]: "0 < MA_PS.prob B"
    using assms pA_pos
    by (metis divide_eq_0_iff measure_cond_prob_space_subset zero_less_measure_iff)
  have [simp]: "B ∈ MA_PS.events"
    using assms by (rewrite sets_cond_prob_space, unfold image_def) blast
  have [simp]: "finite_measure ((M⇂A)⇂B)"
    by (rule prob_space.finite_measure, rule prob_space.cond_prob_space_correct,
        simp_all add: MA_PS.prob_space_axioms)
  show sets_MAB: "sets ((M⇂A)⇂B) = sets (M⇂B)"
    apply (rewrite prob_space.sets_cond_prob_space)
    using MA_PS.prob_space_axioms apply presburger
    apply (rewrite sets_cond_prob_space, unfold image_def)+
    using assms by blast
  show "⋀C. C ∈ sets ((M⇂A)⇂B) ⟹ emeasure ((M⇂A)⇂B) C = emeasure (M⇂B) C"
  proof -
    fix C assume "C ∈ sets ((M⇂A)⇂B)"
    hence "C ∈ sets (M⇂B)" using sets_MAB by simp
    from this obtain D where "D ∈ events" "C = B ∩ D"
      by (rewrite in asm sets_cond_prob_space, auto)
    hence [simp]: "C ∈ events" and [simp]: "C ⊆ B" and [simp]: "C ⊆ A" using assms by auto
    hence [simp]: "C ∈ MA_PS.events"
      using assms by (rewrite sets_cond_prob_space, unfold image_def) blast
    show "emeasure ((M⇂A)⇂B) C = emeasure (M⇂B) C"
      apply (rewrite finite_measure.emeasure_eq_measure, simp)+
      apply (rewrite ennreal_inj, simp_all)
      apply (rewrite prob_space.measure_cond_prob_space_subset,
          simp_all add: assms prob_space_axioms MA_PS.prob_space_axioms)+
      using pA_pos by fastforce
  qed
qed

lemma cond_prob_space_prob:
  assumes[measurable]: "Measurable.pred M P" "Measurable.pred M Q"
    and "𝒫(x in M. Q x) > 0"
  shows "measure (M ⇂ {x ∈ space M. Q x}) {x ∈ space M. P x ∧ Q x} = 𝒫(x in M. P x ¦ Q x)"
proof -
  let ?SetP = "{x ∈ space M. P x}"
  let ?SetQ = "{x ∈ space M. Q x}"
  have "measure (M⇂?SetQ) {x ∈ space M. P x ∧ Q x} = measure (M⇂?SetQ) (?SetP ∩ ?SetQ)"
    by (smt (verit, ccfv_SIG) Collect_cong Int_def mem_Collect_eq)
  also have "… = prob (?SetP ∩ ?SetQ) / prob ?SetQ"
    using assms by (rewrite measure_cond_prob_space; simp?)
  also have "… = 𝒫(x in M. P x ¦ Q x)"
    unfolding cond_prob_def assms by (smt (verit) Collect_cong Int_def mem_Collect_eq)
  finally show ?thesis .
qed

lemma cond_prob_space_cond_prob:
  assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
    and "𝒫(x in M. Q x) > 0"
  shows "𝒫(x in M. P x ¦ Q x) = 𝒫(x in (M ⇂ {x ∈ space M. Q x}). P x)"
proof -
  let ?setQ = "{x ∈ space M. Q x}"
  have "𝒫(x in M. P x ¦ Q x) = measure (M⇂?setQ) {x ∈ space M. P x ∧ Q x}"
    using cond_prob_space_prob assms by simp
  also have "… = 𝒫(x in (M⇂?setQ). P x)"
  proof -
    have "{x ∈ space M. P x ∧ Q x} = {x ∈ space (M⇂?setQ). P x}"
      using space_cond_prob_space assms by force
    thus ?thesis by simp
  qed
  finally show ?thesis .
qed

lemma cond_prob_neg:
  assumes[measurable]: "Measurable.pred M P" "Measurable.pred M Q"
    and "𝒫(x in M. Q x) > 0"
  shows "𝒫(x in M. ¬ P x ¦ Q x) = 1 - 𝒫(x in M. P x ¦ Q x)"
proof -
  let ?setP = "{x ∈ space M. P x}"
  let ?setQ = "{x ∈ space M. Q x}"
  interpret setQ_PS: prob_space "M⇂?setQ" using cond_prob_space_correct assms by simp
  have [simp]: "{x ∈ space (M⇂?setQ). P x} ∈ setQ_PS.events"
  proof -
    have "{x ∈ space (M⇂?setQ). P x} = ?setQ ∩ ?setP" using space_cond_prob_space by force
    thus ?thesis using sets_cond_prob_space by simp
  qed
  have "𝒫(x in M. ¬ P x ¦ Q x) = 𝒫(x in M⇂?setQ. ¬ P x)"
    by (rewrite cond_prob_space_cond_prob; simp add: assms)
  also have "… = 1 - 𝒫(x in M⇂?setQ. P x)" by (rewrite setQ_PS.prob_neg, simp_all add: assms)
  also have "… = 1 - 𝒫(x in M. P x ¦ Q x)"
    by (rewrite cond_prob_space_cond_prob; simp add: assms)
  finally show ?thesis .
qed

lemma random_variable_cond_prob_space:
  assumes "A ∈ events" "prob A > 0"
    and [measurable]: "random_variable borel X"
  shows "X ∈ borel_measurable (M⇂A)"
proof (rule borel_measurableI)
  fix S :: "'b set"
  assume [measurable]: "open S"
  show "X -` S ∩ space (M ⇂ A) ∈ sets (M ⇂ A)"
    apply (rewrite space_cond_prob_space, simp add: assms)
    apply (rewrite sets_cond_prob_space, simp add: image_def)
    apply (rule bexI[of _ "X -` S ∩ space M"]; measurable)
    using sets.Int_space_eq2 Int_commute assms by auto
qed

lemma AE_cond_prob_space_iff:
  assumes "A ∈ events" "prob A > 0"
  shows "(AE x in M⇂A. P x) ⟷ (AE x in M. x ∈ A ⟶ P x)"
proof -
  have [simp]: "1 / emeasure M A > 0"
    using assms divide_ennreal emeasure_eq_measure ennreal_1
    by (smt (verit) divide_pos_pos ennreal_eq_0_iff not_gr_zero)
  show ?thesis
    unfolding cond_prob_space_def
    apply (rewrite AE_scale_measure_iff, simp)
    by (rewrite AE_restrict_space_iff; simp add: assms)
qed

lemma integral_cond_prob_space_nn:
  assumes "A ∈ events" "prob A > 0"
    and [measurable]: "random_variable borel X"
    and nonneg: "AE x in M. x ∈ A ⟶ 0 ≤ X x"
  shows "integral⇧L (M⇂A) X = expectation (λx. indicator A x * X x) / prob A"
proof -
  have [simp]: "X ∈ borel_measurable (M⇂A)"
    by (rule random_variable_cond_prob_space; (simp add: assms))
  have [simp]: "AE x in (M⇂A). 0 ≤ X x"
    by (rewrite AE_cond_prob_space_iff; simp add: assms)
  have [simp]: "random_variable borel (λx. indicat_real A x * X x)" 
    using borel_measurable_indicator assms by force
  have [simp]: "AE x in M. 0 ≤ indicat_real A x * X x" using nonneg by fastforce
  have "integral⇧L (M⇂A) X = enn2real (∫⇧+ x. ennreal (X x) ∂(M⇂A))"
    by (rewrite integral_eq_nn_integral; simp)
  also have "… = enn2real (1 / prob A * ∫⇧+ x. ennreal (X x) ∂(restrict_space M A))"
    unfolding cond_prob_space_def
    apply (rewrite nn_integral_scale_measure, simp add: measurable_restrict_space1)
    using divide_ennreal emeasure_eq_measure ennreal_1 assms by (smt (verit))
  also have "… = enn2real (1 / prob A * (∫⇧+ x. ennreal (indicator A x * X x) ∂M))"
    apply (rewrite nn_integral_restrict_space, simp add: assms)
    by (metis indicator_mult_ennreal mult.commute)
  also have "… = integral⇧L M (λx. indicator A x * X x) / prob A"
    apply (rewrite integral_eq_nn_integral; simp?)
    by (simp add: divide_nonneg_pos enn2real_mult)
  finally show ?thesis by simp
qed

end

text ‹
  Define the complementary cumulative distribution function, also known as tail distribution.
  The theory presented below is a slight modification of the subsection "Properties of cdf's"
  in the theory ‹Distribution_Functions›.
›

subsection ‹Complementary Cumulative Distribution Function›

definition ccdf :: "real measure ⇒ real ⇒ real"
  where "ccdf M ≡ λx. measure M {x<..}"
    ― ‹complementary cumulative distribution function (tail distribution)›

lemma ccdf_def2: "ccdf M x = measure M {x<..}"
  by (simp add: ccdf_def)

context finite_borel_measure
begin

lemma add_cdf_ccdf: "cdf M x + ccdf M x = measure M (space M)"
proof -
  have "{..x} ∪ {x<..} = UNIV" by auto
  moreover have "{..x} ∩ {x<..} = {}" by auto
  ultimately have "emeasure M {..x} + emeasure M {x<..} = emeasure M UNIV"
    using plus_emeasure M_is_borel atMost_borel greaterThan_borel by metis
  hence "measure M {..x} + measure M {x<..} = measure M UNIV"
    using finite_emeasure_space emeasure_eq_measure ennreal_inj
    by (smt (verit, ccfv_SIG) ennreal_plus measure_nonneg)
  thus ?thesis unfolding cdf_def ccdf_def using borel_UNIV by simp
qed

lemma ccdf_cdf: "ccdf M = (λx. measure M (space M) - cdf M x)"
  by (rule ext) (smt (verit) add_cdf_ccdf)

lemma cdf_ccdf: "cdf M = (λx. measure M (space M) - ccdf M x)"
  by (rule ext) (smt (verit) add_cdf_ccdf)

lemma isCont_cdf_ccdf: "isCont (cdf M) x ⟷ isCont (ccdf M) x"
proof
  show "isCont (cdf M) x ⟹ isCont (ccdf M) x" by (rewrite ccdf_cdf) auto
next
  show "isCont (ccdf M) x ⟹ isCont (cdf M) x" by (rewrite cdf_ccdf) auto
qed

lemma isCont_ccdf: "isCont (ccdf M) x ⟷ measure M {x} = 0"
  using isCont_cdf_ccdf isCont_cdf by simp

lemma continuous_cdf_ccdf:
  shows "continuous F (cdf M) ⟷ continuous F (ccdf M)"
    (is "?LHS ⟷ ?RHS")
proof
  assume ?LHS
  thus ?RHS using continuous_diff continuous_const by (rewrite ccdf_cdf) blast
next
  assume ?RHS
  thus ?LHS using continuous_diff continuous_const by (rewrite cdf_ccdf) blast
qed

lemma has_real_derivative_cdf_ccdf:
  "(cdf M has_real_derivative D) F ⟷ (ccdf M has_real_derivative -D) F"
proof
  assume "(cdf M has_real_derivative D) F"
  thus "(ccdf M has_real_derivative -D) F"
    using ccdf_cdf DERIV_const Deriv.field_differentiable_diff by fastforce
next
  assume "(ccdf M has_real_derivative -D) F"
  thus "(cdf M has_real_derivative D) F"
    using cdf_ccdf DERIV_const Deriv.field_differentiable_diff by fastforce
qed

lemma differentiable_cdf_ccdf: "(cdf M differentiable F) ⟷ (ccdf M differentiable F)"
  unfolding differentiable_def
  apply (rewrite has_real_derivative_iff[THEN sym])+
  apply (rewrite has_real_derivative_cdf_ccdf)
  by (metis verit_minus_simplify(4))

lemma deriv_cdf_ccdf:
  assumes "cdf M differentiable at x"
  shows "deriv (cdf M) x = - deriv (ccdf M) x"
  using has_real_derivative_cdf_ccdf differentiable_cdf_ccdf assms
  by (simp add: DERIV_deriv_iff_real_differentiable DERIV_imp_deriv)

lemma ccdf_diff_eq2:
  assumes "x ≤ y"
  shows "ccdf M x - ccdf M y = measure M {x<..y}"
proof -
  have "ccdf M x - ccdf M y = cdf M y - cdf M x" using add_cdf_ccdf by (smt (verit))
  also have "… = measure M {x<..y}" using cdf_diff_eq2 assms by simp
  finally show ?thesis .
qed

lemma ccdf_nonincreasing: "x ≤ y ⟹ ccdf M x ≥ ccdf M y"
  using add_cdf_ccdf cdf_nondecreasing by (smt (verit))

lemma ccdf_nonneg: "ccdf M x ≥ 0"
  using add_cdf_ccdf cdf_bounded by (smt (verit))

lemma ccdf_bounded: "ccdf M x ≤ measure M (space M)"
  using add_cdf_ccdf cdf_nonneg by (smt (verit))

lemma ccdf_lim_at_top: "(ccdf M ⤏ 0) at_top"
proof -
  have "((λx. measure M (space M) - cdf M x) ⤏ measure M (space M) - measure M (space M)) at_top"
    apply (intro tendsto_intros)
    by (rule cdf_lim_at_top)
  thus ?thesis
    by (rewrite ccdf_cdf) simp
qed

lemma ccdf_lim_at_bot: "(ccdf M ⤏ measure M (space M)) at_bot"
proof -
  have "((λx. measure M (space M) - cdf M x) ⤏ measure M (space M) - 0) at_bot"
    apply (intro tendsto_intros)
    by (rule cdf_lim_at_bot)
  thus ?thesis
    by (rewrite ccdf_cdf) simp
qed

lemma ccdf_is_right_cont: "continuous (at_right a) (ccdf M)"
proof -
  have "continuous (at_right a) (λx. measure M (space M) - cdf M x)"
    apply (intro continuous_intros)
    by (rule cdf_is_right_cont)
  thus ?thesis by (rewrite ccdf_cdf) simp
qed

end

context prob_space
begin

lemma ccdf_distr_measurable [measurable]:
  assumes [measurable]: "random_variable borel X"
  shows "ccdf (distr M borel X) ∈ borel_measurable borel"
  using real_distribution.finite_borel_measure_M by (rewrite finite_borel_measure.ccdf_cdf; simp)

lemma ccdf_distr_P:
  assumes "random_variable borel X"
  shows "ccdf (distr M borel X) x = 𝒫(ω in M. X ω > x)"
  unfolding ccdf_def apply (rewrite measure_distr; (simp add: assms)?)
  unfolding vimage_def by (rule arg_cong[where f=prob]) force

lemma ccdf_continuous_distr_P_ge:
  assumes "random_variable borel X" "isCont (ccdf (distr M borel X)) x"
  shows "ccdf (distr M borel X) x = 𝒫(ω in M. X ω ≥ x)"
proof -
  have "ccdf (distr M borel X) x = measure (distr M borel X) {x<..}" unfolding ccdf_def by simp
  also have "… = measure (distr M borel X) ({x<..} ∪ {x})"
    apply (rewrite finite_measure.measure_zero_union, simp_all add: assms finite_measure_distr)
    using finite_borel_measure.isCont_ccdf real_distribution.finite_borel_measure_M assms by blast
  also have "… = measure (distr M borel X) {x..}" by (metis Un_commute ivl_disj_un_singleton(1))
  also have "… = 𝒫(ω in M. X ω ≥ x)" 
    apply (rewrite measure_distr, simp_all add: assms)
    unfolding vimage_def by simp (smt (verit) Collect_cong Int_def mem_Collect_eq)
  finally show ?thesis .
qed

lemma ccdf_distr_diff_P:
  assumes "x ≤ y"
    and "random_variable borel X"
  shows "ccdf (distr M borel X) x - ccdf (distr M borel X) y = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  have "ccdf (distr M borel X) x - ccdf (distr M borel X) y = measure (distr M borel X) {x<..y}"
    by (rewrite distrX_FBM.ccdf_diff_eq2; simp add: assms)
  also have "… = 𝒫(ω in M. x < X ω ∧ X ω ≤ y)"
    apply (rewrite measure_distr; (simp add: assms)?)
    unfolding vimage_def by (rule arg_cong[where f=prob], force)
  finally show ?thesis .
qed

end

context real_distribution
begin

lemma ccdf_bounded_prob: "⋀x. ccdf M x ≤ 1"
  by (subst prob_space[THEN sym], rule ccdf_bounded)

lemma ccdf_lim_at_bot_prob: "(ccdf M ⤏ 1) at_bot"
  by (subst prob_space[THEN sym], rule ccdf_lim_at_bot)

end

text ‹Introduce the hazard rate. This notion will be used to define the force of mortality.›

subsection ‹Hazard Rate›

context prob_space
begin

definition hazard_rate :: "('a ⇒ real) ⇒ real ⇒ real"
  where "hazard_rate X t ≡
    Lim (at_right 0) (λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt)"
    ― ‹Here, ‹X› is supposed to be a random variable.›

lemma hazard_rate_0_ccdf_0:
  assumes [measurable]: "random_variable borel X"
    and "ccdf (distr M borel X) t = 0"
  shows "hazard_rate X t = 0"
  ― ‹Note that division by ‹0› is calculated as ‹0› in Isabelle/HOL.›
proof -
  have "⋀dt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) = 0"
    unfolding cond_prob_def using ccdf_distr_P assms by simp
  hence "hazard_rate X t = Lim (at_right 0) (λdt::real. 0)"
    unfolding hazard_rate_def by (rewrite Lim_cong; simp)
  also have "… = 0" by (rule tendsto_Lim; simp)
  finally show ?thesis .
qed

lemma hazard_rate_deriv_cdf:
  assumes [measurable]: "random_variable borel X"
    and "(cdf (distr M borel X)) differentiable at t"
  shows "hazard_rate X t = deriv (cdf (distr M borel X)) t / ccdf (distr M borel X) t"
proof (cases ‹ccdf (distr M borel X) t = 0›)
  case True
  with hazard_rate_0_ccdf_0 show ?thesis by simp
next
  case False
  let ?F = "cdf (distr M borel X)"
  have "∀⇩F dt in at_right 0. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt =
    (?F (t + dt) - ?F t) / dt / ccdf (distr M borel X) t"
    apply (rule eventually_at_rightI[where b=1]; simp)
    unfolding cond_prob_def
    apply (rewrite cdf_distr_diff_P; simp)
    apply (rewrite ccdf_distr_P[THEN sym], simp)
    by (smt (verit) Collect_cong mult.commute)
  moreover have "((λdt. (?F (t + dt) - ?F t) / dt / ccdf (distr M borel X) t) ⤏
    deriv ?F t / ccdf (distr M borel X) t) (at_right 0)"
    apply (rule tendsto_intros, simp_all add: False)
    apply (rule Lim_at_imp_Lim_at_within)
    using DERIV_deriv_iff_real_differentiable assms DERIV_def by blast
  ultimately show ?thesis
    unfolding hazard_rate_def using tendsto_cong by (intro tendsto_Lim; force)
qed

lemma deriv_cdf_hazard_rate:
  assumes [measurable]: "random_variable borel X"
    and "(cdf (distr M borel X)) differentiable at t"
  shows "deriv (cdf (distr M borel X)) t = ccdf (distr M borel X) t * hazard_rate X t"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  show ?thesis
  proof (cases ‹ccdf (distr M borel X) t = 0›)
    case True
    hence "cdf (distr M borel X) t = 1"
      using distrX_FBM.cdf_ccdf
      by simp (metis assms(1) distrX_FBM.borel_UNIV prob_space.prob_space prob_space_distr)
    moreover obtain D where "(cdf (distr M borel X) has_real_derivative D) (at t)"
      using assms real_differentiable_def by atomize_elim blast
    ultimately have "(cdf (distr M borel X) has_real_derivative 0) (at t)"
      using assms
      by (smt (verit) DERIV_local_max real_distribution.cdf_bounded_prob real_distribution_distr)
    thus ?thesis using True by (simp add: DERIV_imp_deriv)
  next
    case False
    thus ?thesis using hazard_rate_deriv_cdf assms by simp
  qed
qed

lemma hazard_rate_deriv_ccdf:
  assumes [measurable]: "random_variable borel X"
    and "(ccdf (distr M borel X)) differentiable at t"
  shows "hazard_rate X t = - deriv (ccdf (distr M borel X)) t / ccdf (distr M borel X) t"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  show ?thesis
    using hazard_rate_deriv_cdf distrX_FBM.deriv_cdf_ccdf assms distrX_FBM.differentiable_cdf_ccdf
    by presburger
qed

lemma deriv_ccdf_hazard_rate: 
  assumes [measurable]: "random_variable borel X"
    and "(ccdf (distr M borel X)) differentiable at t"
  shows "deriv (ccdf (distr M borel X)) t = - ccdf (distr M borel X) t * hazard_rate X t"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  show ?thesis
    using deriv_cdf_hazard_rate distrX_FBM.deriv_cdf_ccdf assms distrX_FBM.differentiable_cdf_ccdf
    by simp
qed

lemma hazard_rate_deriv_ln_ccdf:
  assumes [measurable]: "random_variable borel X"
    and "(ccdf (distr M borel X)) differentiable at t"
    and "ccdf (distr M borel X) t ≠ 0"
  shows "hazard_rate X t = - deriv (λt. ln (ccdf (distr M borel X) t)) t"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  let ?srvl = "ccdf (distr M borel X)"
  have "?srvl t > 0" using distrX_FBM.ccdf_nonneg assms by (smt (verit))
  moreover have "(?srvl has_real_derivative (deriv ?srvl t)) (at t)"
    using DERIV_deriv_iff_real_differentiable assms by blast
  ultimately have "((λt. ln (?srvl t)) has_real_derivative  1 / ?srvl t * deriv ?srvl t) (at t)"
    by (rule derivative_intros)
  hence "deriv (λt. ln (?srvl t)) t = deriv ?srvl t / ?srvl t" by (simp add: DERIV_imp_deriv)
  also have "… = - hazard_rate X t" using hazard_rate_deriv_ccdf assms by simp
  finally show ?thesis by simp
qed

lemma hazard_rate_has_integral:
  assumes [measurable]: "random_variable borel X"
    and "t ≤ u"
    and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
    and "continuous_on {t..u} (ccdf (distr M borel X))"
    and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
  shows
    "(hazard_rate X has_integral ln (ccdf (distr M borel X) t / ccdf (distr M borel X) u)) {t..u}"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  let ?srvl = "ccdf (distr M borel X)"
  have [simp]: "⋀s. t ≤ s ∧ s ≤ u ⟹ ?srvl s > 0"
    using distrX_FBM.ccdf_nonneg assms by (smt (verit) atLeastAtMost_iff)
  have "(deriv (λs. - ln (?srvl s)) has_integral - ln (?srvl u) - - ln (?srvl t)) {t..u}"
  proof -
    have "continuous_on {t..u} (λs. - ln (?srvl s))"
      by (rule continuous_intros, rule continuous_on_ln, auto simp add: assms)
    moreover hence "(λs. - ln (?srvl s)) piecewise_differentiable_on {t<..<u}"
    proof -
      have "?srvl ` {t<..<u} ⊆ {0<..}"
      proof -
        { fix s assume "s ∈ {t<..<u}"
          hence "?srvl s ≠ 0" using assms by simp
          moreover have "?srvl s ≥ 0" using distrX_FBM.ccdf_nonneg by simp
          ultimately have "?srvl s > 0" by simp }
        thus ?thesis by auto
      qed
      hence "(λr. - ln r) ∘ ?srvl piecewise_differentiable_on {t<..<u}"
        apply (intro differentiable_on_piecewise_compose, simp add: assms)
        apply (rule derivative_intros)
        apply (rule differentiable_on_subset[of ln "{0<..}"], simp_all)
        apply (rewrite differentiable_on_eq_field_differentiable_real, auto)
        unfolding field_differentiable_def using DERIV_ln by (metis has_field_derivative_at_within)
      thus ?thesis unfolding comp_def by simp
    qed
    ultimately show ?thesis by (intro FTC_real_deriv_has_integral; simp add: assms)
  qed
  hence ln: "(deriv (λs. - ln (?srvl s)) has_integral ln (?srvl t / ?srvl u)) {t..u}"
    by simp (rewrite ln_div; force simp: assms)
  thus "((hazard_rate X) has_integral ln (?srvl t / ?srvl u)) {t..u}"
  proof -
    from assms obtain S0 where finS0: "finite S0" and
      diffS0: "⋀s. s ∈ {t<..<u} - S0 ⟹ ?srvl differentiable at s within {t<..<u}"
      unfolding piecewise_differentiable_on_def by blast
    from this obtain S where "finite S" and "⋀s. s ∈ {t..u} - S ⟹ ?srvl differentiable at s"
    proof (atomize_elim)
      let ?S = "S0 ∪ {t, u}"
      have "finite ?S" using finS0 by simp
      moreover have "∀s. s ∈ {t..u} - ?S ⟶ ccdf (distr M borel X) differentiable at s"
      proof -
        { fix s assume s_in: "s ∈ {t..u} - ?S"
          hence "?srvl differentiable at s within {t<..<u}" using diffS0 by simp
          hence "?srvl differentiable at s"
            using s_in by (rewrite at_within_open[THEN sym], simp_all) }
        thus ?thesis by blast
      qed
      ultimately show
        "∃S. finite S ∧ (∀s. s ∈ {t..u} - S ⟶ ccdf (distr M borel X) differentiable at s)"
        by blast
    qed
    thus ?thesis
      apply (rewrite has_integral_spike_finite_eq [of S _ "deriv (λs. - ln (?srvl s))"], simp)
       apply (rewrite hazard_rate_deriv_ln_ccdf, simp_all add: assms)
       apply (rewrite deriv_minus, simp_all)
       apply (rewrite in asm differentiable_eq_field_differentiable_real)
       apply (rewrite comp_def[THEN sym], rule field_differentiable_compose[of "?srvl"], simp_all)
      unfolding field_differentiable_def apply (rule exI, rule DERIV_ln, simp)
      using ln by simp
  qed
qed

corollary hazard_rate_integrable:
  assumes [measurable]: "random_variable borel X"
    and "t ≤ u"
    and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
    and "continuous_on {t..u} (ccdf (distr M borel X))"
    and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
  shows "hazard_rate X integrable_on {t..u}"
  using has_integral_integrable hazard_rate_has_integral assms by blast

lemma ccdf_exp_cumulative_hazard:
  assumes [measurable]: "random_variable borel X"
    and "t ≤ u"
    and "(ccdf (distr M borel X)) piecewise_differentiable_on {t<..<u}"
    and "continuous_on {t..u} (ccdf (distr M borel X))"
    and "⋀s. s ∈ {t..u} ⟹ ccdf (distr M borel X) s ≠ 0"
  shows "ccdf (distr M borel X) u / ccdf (distr M borel X) t =
    exp (- integral {t..u} (hazard_rate X))"
proof -
  interpret distrX_FBM: finite_borel_measure "distr M borel X"
    using real_distribution.finite_borel_measure_M real_distribution_distr assms by simp
  let ?srvl = "ccdf (distr M borel X)"
  have [simp]: "⋀s. t ≤ s ∧ s ≤ u ⟹ ?srvl s > 0"
    using distrX_FBM.ccdf_nonneg assms by (smt (verit) atLeastAtMost_iff)
  have "integral {t..u} (hazard_rate X) = ln (?srvl t / ?srvl u)"
    using hazard_rate_has_integral has_integral_integrable_integral assms by auto
  also have "… = - ln (?srvl u / ?srvl t)" using ln_div assms by simp
  finally have "- integral {t..u} (hazard_rate X) = ln (?srvl u / ?srvl t)" by simp
  thus ?thesis using assms by simp
qed

lemma hazard_rate_density_ccdf:
  assumes "distributed M lborel X f"
    and "⋀s. f s ≥ 0" "t < u" "continuous_on {t..u} f"
  shows "hazard_rate X t = f t / ccdf (distr M borel X) t"
proof (cases ‹ccdf (distr M borel X) t = 0›)
  case True
  thus ?thesis
    apply (rewrite hazard_rate_0_ccdf_0, simp_all)
    using assms(1) distributed_measurable by force
next
  case False
  have [simp]: "t ≤ u" using assms by simp
  have [measurable]: "random_variable borel X"
    using assms distributed_measurable measurable_lborel1 by blast
  have [measurable]: "f ∈ borel_measurable lborel"
    using assms distributed_real_measurable by metis
  have [simp]: "integrable lborel f"
  proof -
    have "prob (X -` UNIV ∩ space M) = LINT x|lborel. indicat_real UNIV x * f x"
      by (rule distributed_measure; simp add: assms)
    thus ?thesis
      using prob_space not_integrable_integral_eq by fastforce
  qed
  have "((λdt. (LBINT s:{t..t+dt}. f s) / dt) ⤏ f t) (at_right 0)"
  proof -
    have "⋀dt. (∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) < ∞"
    proof -
      fix dt :: real
      have "(∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) =
        set_nn_integral lborel {t..t+dt} f"
        by (metis indicator_mult_ennreal mult.commute)
      moreover have "emeasure M (X -` {t..t+dt} ∩ space M) = set_nn_integral lborel {t..t+dt} f"
        by (rule distributed_emeasure; simp add: assms)
      moreover have "emeasure M (X -` {t..t+dt} ∩ space M) < ∞"
        using emeasure_eq_measure ennreal_less_top infinity_ennreal_def by presburger
      ultimately show "(∫⇧+ x. ennreal (indicat_real {t..t+dt} x * f x) ∂lborel) < ∞" by simp
    qed
    hence "⋀dt. (LBINT s:{t..t+dt}. f s) = integral {t..t+dt} f"
      apply (intro set_borel_integral_eq_integral)
      unfolding set_integrable_def
      apply (rule integrableI_nonneg; simp)
      by (rule AE_I2, simp add: assms)
    moreover have "((λdt. (integral {t..t+dt} f) / dt) ⤏ f t) (at_right 0)"
    proof -
      have "((λx. integral {t..x} f) has_real_derivative f t) (at t within {t..u})"
        by (rule integral_has_real_derivative; simp add: assms)
      moreover have "(at t within {t..u}) = (at (t+0) within (+)t ` {0..u-t})" by simp
      ultimately have
        "((λx. integral {t..x} f) ∘ (+)t has_real_derivative f t) (at 0 within {0..u-t})"
        by (metis DERIV_at_within_shift_lemma)
      hence "((λdt. (integral {t..t+dt} f) / dt) ⤏ f t) (at 0 within {0..u-t})"
        using has_field_derivative_iff by force
      thus ?thesis using at_within_Icc_at_right assms by (smt (verit))
    qed
    ultimately show ?thesis by simp
  qed
  moreover have "⋀dt. dt > 0 ⟹ 𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t..t+dt}. f s)"
  proof -
    fix dt :: real assume "dt > 0"
    hence [simp]: "sym_diff {t<..t + dt} {t..t + dt} = {t}" by force
    have "prob (X -` {t<..t+dt} ∩ space M) = ∫s. indicator {t<..t+dt} s * f s ∂lborel"
      by (rule distributed_measure; simp add: assms)
    hence "𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t<..t+dt}. f s)"
      unfolding set_lebesgue_integral_def vimage_def Int_def by simp (smt (verit) Collect_cong)
    moreover have "(LBINT s:{t<..t+dt}. f s) = (LBINT s:{t..t+dt}. f s)"
      by (rule set_integral_null_delta; force)
    ultimately show "𝒫(x in M. X x ∈ {t <.. t+dt}) = (LBINT s:{t..t+dt}. f s)" by simp
  qed
  ultimately have "((λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt) / dt) ⤏ f t) (at_right 0)"
    by simp (smt (verit) Lim_cong_within greaterThan_iff)
  hence "((λdt. 𝒫(x in M. t < X x ∧ X x ≤ t + dt ¦ X x > t) / dt) ⤏
    f t / ccdf (distr M borel X) t) (at_right 0)"
    unfolding cond_prob_def
    apply (rewrite ccdf_distr_P[THEN sym]; simp)
    apply (rewrite mult.commute, rewrite divide_divide_eq_left[THEN sym])
    by (rule tendsto_intros; (simp add: False)?) (smt (verit) Collect_cong Lim_cong_within)
  thus ?thesis unfolding hazard_rate_def by (intro tendsto_Lim; simp)
qed

end

end