Theory Set_Integral

(*  Title:      HOL/Probability/Set_Integral.thy
    Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin

Notation and useful facts for working with integrals over a set.

TODO: keep all these? Need unicode translations as well.
*)

theory Set_Integral
  imports Bochner_Integration Lebesgue_Measure
begin

(*
    Notation
*)

abbreviation "set_borel_measurable M A f ≡ (λx. indicator A x *⇩R f x) ∈ borel_measurable M"

abbreviation "set_integrable M A f ≡ integrable M (λx. indicator A x *⇩R f x)"

abbreviation "set_lebesgue_integral M A f ≡ lebesgue_integral M (λx. indicator A x *⇩R f x)"

syntax
"_ascii_set_lebesgue_integral" :: "pttrn ⇒ 'a set ⇒ 'a measure ⇒ real ⇒ real"
("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)

translations
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (λx. f)"

abbreviation
  "set_almost_everywhere A M P ≡ AE x in M. x ∈ A ⟶ P x"

syntax
  "_set_almost_everywhere" :: "pttrn ⇒ 'a set ⇒ 'a ⇒ bool ⇒ bool"
("AE _∈_ in _./ _" [0,0,0,10] 10)

translations
  "AE x∈A in M. P" == "CONST set_almost_everywhere A M (λx. P)"

(*
    Notation for integration wrt lebesgue measure on the reals:

      LBINT x. f
      LBINT x : A. f

    TODO: keep all these? Need unicode.
*)

syntax
"_lebesgue_borel_integral" :: "pttrn ⇒ real ⇒ real"
("(2LBINT _./ _)" [0,60] 60)

translations
"LBINT x. f" == "CONST lebesgue_integral CONST lborel (λx. f)"

syntax
"_set_lebesgue_borel_integral" :: "pttrn ⇒ real set ⇒ real ⇒ real"
("(3LBINT _:_./ _)" [0,60,61] 60)

translations
"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (λx. f)"

(*
    Basic properties
*)

(*
lemma indicator_abs_eq: "⋀A x. ¦indicator A x¦ = ((indicator A x) :: real)"
  by (auto simp add: indicator_def)
*)

lemma set_borel_measurable_sets:
  fixes f :: "_ ⇒ _::real_normed_vector"
  assumes "set_borel_measurable M X f" "B ∈ sets borel" "X ∈ sets M"
  shows "f -` B ∩ X ∈ sets M"
proof -
  have "f ∈ borel_measurable (restrict_space M X)"
    using assms by (subst borel_measurable_restrict_space_iff) auto
  then have "f -` B ∩ space (restrict_space M X) ∈ sets (restrict_space M X)"
    by (rule measurable_sets) fact
  with ‹X ∈ sets M› show ?thesis
    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
qed

lemma set_lebesgue_integral_cong:
  assumes "A ∈ sets M" and "∀x. x ∈ A ⟶ f x = g x"
  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)

lemma set_lebesgue_integral_cong_AE:
  assumes [measurable]: "A ∈ sets M" "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  assumes "AE x ∈ A in M. f x = g x"
  shows "LINT x:A|M. f x = LINT x:A|M. g x"
proof-
  have "AE x in M. indicator A x *⇩R f x = indicator A x *⇩R g x"
    using assms by auto
  thus ?thesis by (intro integral_cong_AE) auto
qed

lemma set_integrable_cong_AE:
    "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹
    AE x ∈ A in M. f x = g x ⟹ A ∈ sets M ⟹
    set_integrable M A f = set_integrable M A g"
  by (rule integrable_cong_AE) auto

lemma set_integrable_subset:
  fixes M A B and f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "set_integrable M A f" "B ∈ sets M" "B ⊆ A"
  shows "set_integrable M B f"
proof -
  have "set_integrable M B (λx. indicator A x *⇩R f x)"
    by (rule integrable_mult_indicator) fact+
  with ‹B ⊆ A› show ?thesis
    by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
qed

(* TODO: integral_cmul_indicator should be named set_integral_const *)
(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)

lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *⇩R f t = a *⇩R (LINT t:A|M. f t)"
  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)

lemma set_integral_mult_right [simp]:
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)

lemma set_integral_mult_left [simp]:
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)

lemma set_integral_divide_zero [simp]:
  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
  by (subst integral_divide_zero[symmetric], intro integral_cong)
     (auto split: split_indicator)

lemma set_integrable_scaleR_right [simp, intro]:
  shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. a *⇩R f t)"
  unfolding scaleR_left_commute by (rule integrable_scaleR_right)

lemma set_integrable_scaleR_left [simp, intro]:
  fixes a :: "_ :: {banach, second_countable_topology}"
  shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. f t *⇩R a)"
  using integrable_scaleR_left[of a M "λx. indicator A x *⇩R f x"] by simp

lemma set_integrable_mult_right [simp, intro]:
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
  shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. a * f t)"
  using integrable_mult_right[of a M "λx. indicator A x *⇩R f x"] by simp

lemma set_integrable_mult_left [simp, intro]:
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
  shows "(a ≠ 0 ⟹ set_integrable M A f) ⟹ set_integrable M A (λt. f t * a)"
  using integrable_mult_left[of a M "λx. indicator A x *⇩R f x"] by simp

lemma set_integrable_divide [simp, intro]:
  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
  assumes "a ≠ 0 ⟹ set_integrable M A f"
  shows "set_integrable M A (λt. f t / a)"
proof -
  have "integrable M (λx. indicator A x *⇩R f x / a)"
    using assms by (rule integrable_divide_zero)
  also have "(λx. indicator A x *⇩R f x / a) = (λx. indicator A x *⇩R (f x / a))"
    by (auto split: split_indicator)
  finally show ?thesis .
qed

lemma set_integral_add [simp, intro]:
  fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "set_integrable M A f" "set_integrable M A g"
  shows "set_integrable M A (λx. f x + g x)"
    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
  using assms by (simp_all add: scaleR_add_right)

lemma set_integral_diff [simp, intro]:
  assumes "set_integrable M A f" "set_integrable M A g"
  shows "set_integrable M A (λx. f x - g x)" and "LINT x:A|M. f x - g x =
    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
  using assms by (simp_all add: scaleR_diff_right)

lemma set_integral_reflect:
  fixes S and f :: "real ⇒ 'a :: {banach, second_countable_topology}"
  shows "(LBINT x : S. f x) = (LBINT x : {x. - x ∈ S}. f (- x))"
  using assms
  by (subst lborel_integral_real_affine[where c="-1" and t=0])
     (auto intro!: integral_cong split: split_indicator)

(* question: why do we have this for negation, but multiplication by a constant
   requires an integrability assumption? *)
lemma set_integral_uminus: "set_integrable M A f ⟹ LINT x:A|M. - f x = - (LINT x:A|M. f x)"
  by (subst integral_minus[symmetric]) simp_all

lemma set_integral_complex_of_real:
  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
  by (subst integral_complex_of_real[symmetric])
     (auto intro!: integral_cong split: split_indicator)

lemma set_integral_mono:
  fixes f g :: "_ ⇒ real"
  assumes "set_integrable M A f" "set_integrable M A g"
    "⋀x. x ∈ A ⟹ f x ≤ g x"
  shows "(LINT x:A|M. f x) ≤ (LINT x:A|M. g x)"
using assms by (auto intro: integral_mono split: split_indicator)

lemma set_integral_mono_AE:
  fixes f g :: "_ ⇒ real"
  assumes "set_integrable M A f" "set_integrable M A g"
    "AE x ∈ A in M. f x ≤ g x"
  shows "(LINT x:A|M. f x) ≤ (LINT x:A|M. g x)"
using assms by (auto intro: integral_mono_AE split: split_indicator)

lemma set_integrable_abs: "set_integrable M A f ⟹ set_integrable M A (λx. ¦f x¦ :: real)"
  using integrable_abs[of M "λx. f x * indicator A x"] by (simp add: abs_mult ac_simps)

lemma set_integrable_abs_iff:
  fixes f :: "_ ⇒ real"
  shows "set_borel_measurable M A f ⟹ set_integrable M A (λx. ¦f x¦) = set_integrable M A f"
  by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)

lemma set_integrable_abs_iff':
  fixes f :: "_ ⇒ real"
  shows "f ∈ borel_measurable M ⟹ A ∈ sets M ⟹
    set_integrable M A (λx. ¦f x¦) = set_integrable M A f"
by (intro set_integrable_abs_iff) auto

lemma set_integrable_discrete_difference:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes "countable X"
  assumes diff: "(A - B) ∪ (B - A) ⊆ X"
  assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0" "⋀x. x ∈ X ⟹ {x} ∈ sets M"
  shows "set_integrable M A f ⟷ set_integrable M B f"
proof (rule integrable_discrete_difference[where X=X])
  show "⋀x. x ∈ space M ⟹ x ∉ X ⟹ indicator A x *⇩R f x = indicator B x *⇩R f x"
    using diff by (auto split: split_indicator)
qed fact+

lemma set_integral_discrete_difference:
  fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
  assumes "countable X"
  assumes diff: "(A - B) ∪ (B - A) ⊆ X"
  assumes "⋀x. x ∈ X ⟹ emeasure M {x} = 0" "⋀x. x ∈ X ⟹ {x} ∈ sets M"
  shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
proof (rule integral_discrete_difference[where X=X])
  show "⋀x. x ∈ space M ⟹ x ∉ X ⟹ indicator A x *⇩R f x = indicator B x *⇩R f x"
    using diff by (auto split: split_indicator)
qed fact+

lemma set_integrable_Un:
  fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
    and [measurable]: "A ∈ sets M" "B ∈ sets M"
  shows "set_integrable M (A ∪ B) f"
proof -
  have "set_integrable M (A - B) f"
    using f_A by (rule set_integrable_subset) auto
  from integrable_add[OF this f_B] show ?thesis
    by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
qed

lemma set_integrable_UN:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "finite I" "⋀i. i∈I ⟹ set_integrable M (A i) f"
    "⋀i. i∈I ⟹ A i ∈ sets M"
  shows "set_integrable M (⋃i∈I. A i) f"
using assms by (induct I) (auto intro!: set_integrable_Un)

lemma set_integral_Un:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "A ∩ B = {}"
  and "set_integrable M A f"
  and "set_integrable M B f"
  shows "LINT x:A∪B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
      scaleR_add_left assms)

lemma set_integral_cong_set:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
    and ae: "AE x in M. x ∈ A ⟷ x ∈ B"
  shows "LINT x:B|M. f x = LINT x:A|M. f x"
proof (rule integral_cong_AE)
  show "AE x in M. indicator B x *⇩R f x = indicator A x *⇩R f x"
    using ae by (auto simp: subset_eq split: split_indicator)
qed fact+

lemma set_borel_measurable_subset:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes [measurable]: "set_borel_measurable M A f" "B ∈ sets M" and "B ⊆ A"
  shows "set_borel_measurable M B f"
proof -
  have "set_borel_measurable M B (λx. indicator A x *⇩R f x)"
    by measurable
  also have "(λx. indicator B x *⇩R indicator A x *⇩R f x) = (λx. indicator B x *⇩R f x)"
    using ‹B ⊆ A› by (auto simp: fun_eq_iff split: split_indicator)
  finally show ?thesis .
qed

lemma set_integral_Un_AE:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes ae: "AE x in M. ¬ (x ∈ A ∧ x ∈ B)" and [measurable]: "A ∈ sets M" "B ∈ sets M"
  and "set_integrable M A f"
  and "set_integrable M B f"
  shows "LINT x:A∪B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
proof -
  have f: "set_integrable M (A ∪ B) f"
    by (intro set_integrable_Un assms)
  then have f': "set_borel_measurable M (A ∪ B) f"
    by (rule borel_measurable_integrable)
  have "LINT x:A∪B|M. f x = LINT x:(A - A ∩ B) ∪ (B - A ∩ B)|M. f x"
  proof (rule set_integral_cong_set)
    show "AE x in M. (x ∈ A - A ∩ B ∪ (B - A ∩ B)) = (x ∈ A ∪ B)"
      using ae by auto
    show "set_borel_measurable M (A - A ∩ B ∪ (B - A ∩ B)) f"
      using f' by (rule set_borel_measurable_subset) auto
  qed fact
  also have "… = (LINT x:(A - A ∩ B)|M. f x) + (LINT x:(B - A ∩ B)|M. f x)"
    by (auto intro!: set_integral_Un set_integrable_subset[OF f])
  also have "… = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
    using ae
    by (intro arg_cong2[where f="op+"] set_integral_cong_set)
       (auto intro!: set_borel_measurable_subset[OF f'])
  finally show ?thesis .
qed

lemma set_integral_finite_Union:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "finite I" "disjoint_family_on A I"
    and "⋀i. i ∈ I ⟹ set_integrable M (A i) f" "⋀i. i ∈ I ⟹ A i ∈ sets M"
  shows "(LINT x:(⋃i∈I. A i)|M. f x) = (∑i∈I. LINT x:A i|M. f x)"
  using assms
  apply induct
  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
by (subst set_integral_Un, auto intro: set_integrable_UN)

(* TODO: find a better name? *)
lemma pos_integrable_to_top:
  fixes l::real
  assumes "⋀i. A i ∈ sets M" "mono A"
  assumes nneg: "⋀x i. x ∈ A i ⟹ 0 ≤ f x"
  and intgbl: "⋀i::nat. set_integrable M (A i) f"
  and lim: "(λi::nat. LINT x:A i|M. f x) ⇢ l"
  shows "set_integrable M (⋃i. A i) f"
  apply (rule integrable_monotone_convergence[where f = "λi::nat. λx. indicator (A i) x *⇩R f x" and x = l])
  apply (rule intgbl)
  prefer 3 apply (rule lim)
  apply (rule AE_I2)
  using ‹mono A› apply (auto simp: mono_def nneg split: split_indicator) []
proof (rule AE_I2)
  { fix x assume "x ∈ space M"
    show "(λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋃i. A i) x *⇩R f x"
    proof cases
      assume "∃i. x ∈ A i"
      then guess i ..
      then have *: "eventually (λi. x ∈ A i) sequentially"
        using ‹x ∈ A i› ‹mono A› by (auto simp: eventually_sequentially mono_def)
      show ?thesis
        apply (intro Lim_eventually)
        using *
        apply eventually_elim
        apply (auto split: split_indicator)
        done
    qed auto }
  then show "(λx. indicator (⋃i. A i) x *⇩R f x) ∈ borel_measurable M"
    apply (rule borel_measurable_LIMSEQ_real)
    apply assumption
    apply (intro borel_measurable_integrable intgbl)
    done
qed

(* Proof from Royden Real Analysis, p. 91. *)
lemma lebesgue_integral_countable_add:
  fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
  assumes meas[intro]: "⋀i::nat. A i ∈ sets M"
    and disj: "⋀i j. i ≠ j ⟹ A i ∩ A j = {}"
    and intgbl: "set_integrable M (⋃i. A i) f"
  shows "LINT x:(⋃i. A i)|M. f x = (∑i. (LINT x:(A i)|M. f x))"
proof (subst integral_suminf[symmetric])
  show int_A: "⋀i. set_integrable M (A i) f"
    using intgbl by (rule set_integrable_subset) auto
  { fix x assume "x ∈ space M"
    have "(λi. indicator (A i) x *⇩R f x) sums (indicator (⋃i. A i) x *⇩R f x)"
      by (intro sums_scaleR_left indicator_sums) fact }
  note sums = this

  have norm_f: "⋀i. set_integrable M (A i) (λx. norm (f x))"
    using int_A[THEN integrable_norm] by auto

  show "AE x in M. summable (λi. norm (indicator (A i) x *⇩R f x))"
    using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])

  show "summable (λi. LINT x|M. norm (indicator (A i) x *⇩R f x))"
  proof (rule summableI_nonneg_bounded)
    fix n
    show "0 ≤ LINT x|M. norm (indicator (A n) x *⇩R f x)"
      using norm_f by (auto intro!: integral_nonneg_AE)

    have "(∑i<n. LINT x|M. norm (indicator (A i) x *⇩R f x)) =
      (∑i<n. set_lebesgue_integral M (A i) (λx. norm (f x)))"
      by (simp add: abs_mult)
    also have "… = set_lebesgue_integral M (⋃i<n. A i) (λx. norm (f x))"
      using norm_f
      by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
    also have "… ≤ set_lebesgue_integral M (⋃i. A i) (λx. norm (f x))"
      using intgbl[THEN integrable_norm]
      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
         (auto split: split_indicator)
    finally show "(∑i<n. LINT x|M. norm (indicator (A i) x *⇩R f x)) ≤
      set_lebesgue_integral M (⋃i. A i) (λx. norm (f x))"
      by simp
  qed
  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (∑i. indicator (A i) x *⇩R f x)"
    apply (rule integral_cong[OF refl])
    apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
    using sums_unique[OF indicator_sums[OF disj]]
    apply auto
    done
qed

lemma set_integral_cont_up:
  fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
  assumes [measurable]: "⋀i. A i ∈ sets M" and A: "incseq A"
  and intgbl: "set_integrable M (⋃i. A i) f"
  shows "(λi. LINT x:(A i)|M. f x) ⇢ LINT x:(⋃i. A i)|M. f x"
proof (intro integral_dominated_convergence[where w="λx. indicator (⋃i. A i) x *⇩R norm (f x)"])
  have int_A: "⋀i. set_integrable M (A i) f"
    using intgbl by (rule set_integrable_subset) auto
  then show "⋀i. set_borel_measurable M (A i) f" "set_borel_measurable M (⋃i. A i) f"
    "set_integrable M (⋃i. A i) (λx. norm (f x))"
    using intgbl integrable_norm[OF intgbl] by auto

  { fix x i assume "x ∈ A i"
    with A have "(λxa. indicator (A xa) x::real) ⇢ 1 ⟷ (λxa. 1::real) ⇢ 1"
      by (intro filterlim_cong refl)
         (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
  then show "AE x in M. (λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋃i. A i) x *⇩R f x"
    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed (auto split: split_indicator)

(* Can the int0 hypothesis be dropped? *)
lemma set_integral_cont_down:
  fixes f :: "_ ⇒ 'a :: {banach, second_countable_topology}"
  assumes [measurable]: "⋀i. A i ∈ sets M" and A: "decseq A"
  and int0: "set_integrable M (A 0) f"
  shows "(λi::nat. LINT x:(A i)|M. f x) ⇢ LINT x:(⋂i. A i)|M. f x"
proof (rule integral_dominated_convergence)
  have int_A: "⋀i. set_integrable M (A i) f"
    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
  show "set_integrable M (A 0) (λx. norm (f x))"
    using int0[THEN integrable_norm] by simp
  have "set_integrable M (⋂i. A i) f"
    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
  with int_A show "set_borel_measurable M (⋂i. A i) f" "⋀i. set_borel_measurable M (A i) f"
    by auto
  show "⋀i. AE x in M. norm (indicator (A i) x *⇩R f x) ≤ indicator (A 0) x *⇩R norm (f x)"
    using A by (auto split: split_indicator simp: decseq_def)
  { fix x i assume "x ∈ space M" "x ∉ A i"
    with A have "(λi. indicator (A i) x::real) ⇢ 0 ⟷ (λi. 0::real) ⇢ 0"
      by (intro filterlim_cong refl)
         (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
  then show "AE x in M. (λi. indicator (A i) x *⇩R f x) ⇢ indicator (⋂i. A i) x *⇩R f x"
    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
qed

lemma set_integral_at_point:
  fixes a :: real
  assumes "set_integrable M {a} f"
  and [simp]: "{a} ∈ sets M" and "(emeasure M) {a} ≠ ∞"
  shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
proof-
  have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
    by (intro set_lebesgue_integral_cong) simp_all
  then show ?thesis using assms by simp
qed


abbreviation complex_integrable :: "'a measure ⇒ ('a ⇒ complex) ⇒ bool" where
  "complex_integrable M f ≡ integrable M f"

abbreviation complex_lebesgue_integral :: "'a measure ⇒ ('a ⇒ complex) ⇒ complex" ("integral⇧C") where
  "integral⇧C M f == integral⇧L M f"

syntax
  "_complex_lebesgue_integral" :: "pttrn ⇒ complex ⇒ 'a measure ⇒ complex"
 ("∫⇧C _. _ ∂_" [60,61] 110)

translations
  "∫⇧Cx. f ∂M" == "CONST complex_lebesgue_integral M (λx. f)"

syntax
  "_ascii_complex_lebesgue_integral" :: "pttrn ⇒ 'a measure ⇒ real ⇒ real"
  ("(3CLINT _|_. _)" [0,110,60] 60)

translations
  "CLINT x|M. f" == "CONST complex_lebesgue_integral M (λx. f)"

lemma complex_integrable_cnj [simp]:
  "complex_integrable M (λx. cnj (f x)) ⟷ complex_integrable M f"
proof
  assume "complex_integrable M (λx. cnj (f x))"
  then have "complex_integrable M (λx. cnj (cnj (f x)))"
    by (rule integrable_cnj)
  then show "complex_integrable M f"
    by simp
qed simp

lemma complex_of_real_integrable_eq:
  "complex_integrable M (λx. complex_of_real (f x)) ⟷ integrable M f"
proof
  assume "complex_integrable M (λx. complex_of_real (f x))"
  then have "integrable M (λx. Re (complex_of_real (f x)))"
    by (rule integrable_Re)
  then show "integrable M f"
    by simp
qed simp


abbreviation complex_set_integrable :: "'a measure ⇒ 'a set ⇒ ('a ⇒ complex) ⇒ bool" where
  "complex_set_integrable M A f ≡ set_integrable M A f"

abbreviation complex_set_lebesgue_integral :: "'a measure ⇒ 'a set ⇒ ('a ⇒ complex) ⇒ complex" where
  "complex_set_lebesgue_integral M A f ≡ set_lebesgue_integral M A f"

syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn ⇒ 'a set ⇒ 'a measure ⇒ real ⇒ real"
("(4CLINT _:_|_. _)" [0,60,110,61] 60)

translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (λx. f)"

(*
lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = ¦a¦ * cmod x"
  apply (simp add: norm_mult)
  by (subst norm_mult, auto)
*)

lemma borel_integrable_atLeastAtMost':
  fixes f :: "real ⇒ 'a::{banach, second_countable_topology}"
  assumes f: "continuous_on {a..b} f"
  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
  by (intro borel_integrable_compact compact_Icc f)

lemma integral_FTC_atLeastAtMost:
  fixes f :: "real ⇒ 'a :: euclidean_space"
  assumes "a ≤ b"
    and F: "⋀x. a ≤ x ⟹ x ≤ b ⟹ (F has_vector_derivative f x) (at x within {a .. b})"
    and f: "continuous_on {a .. b} f"
  shows "integral⇧L lborel (λx. indicator {a .. b} x *⇩R f x) = F b - F a"
proof -
  let ?f = "λx. indicator {a .. b} x *⇩R f x"
  have "(?f has_integral (∫x. ?f x ∂lborel)) UNIV"
    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
  moreover
  have "(f has_integral F b - F a) {a .. b}"
    by (intro fundamental_theorem_of_calculus ballI assms) auto
  then have "(?f has_integral F b - F a) {a .. b}"
    by (subst has_integral_cong[where g=f]) auto
  then have "(?f has_integral F b - F a) UNIV"
    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
  ultimately show "integral⇧L lborel ?f = F b - F a"
    by (rule has_integral_unique)
qed

lemma set_borel_integral_eq_integral:
  fixes f :: "real ⇒ 'a::euclidean_space"
  assumes "set_integrable lborel S f"
  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
proof -
  let ?f = "λx. indicator S x *⇩R f x"
  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
    by (rule has_integral_integral_lborel) fact
  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
    apply (subst has_integral_restrict_univ [symmetric])
    apply (rule has_integral_eq)
    by auto
  thus "f integrable_on S"
    by (auto simp add: integrable_on_def)
  with 1 have "(f has_integral (integral S f)) S"
    by (intro integrable_integral, auto simp add: integrable_on_def)
  thus "LINT x : S | lborel. f x = integral S f"
    by (intro has_integral_unique [OF 1])
qed

lemma set_borel_measurable_continuous:
  fixes f :: "_ ⇒ _::real_normed_vector"
  assumes "S ∈ sets borel" "continuous_on S f"
  shows "set_borel_measurable borel S f"
proof -
  have "(λx. if x ∈ S then f x else 0) ∈ borel_measurable borel"
    by (intro assms borel_measurable_continuous_on_if continuous_on_const)
  also have "(λx. if x ∈ S then f x else 0) = (λx. indicator S x *⇩R f x)"
    by auto
  finally show ?thesis .
qed

lemma set_measurable_continuous_on_ivl:
  assumes "continuous_on {a..b} (f :: real ⇒ real)"
  shows "set_borel_measurable borel {a..b} f"
  by (rule set_borel_measurable_continuous[OF _ assms]) simp

end