src/HOL/Analysis/Set_Integral.thy
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63886 685fb01256af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,602 @@
     1.4 +(*  Title:      HOL/Analysis/Set_Integral.thy
     1.5 +    Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
     1.6 +
     1.7 +Notation and useful facts for working with integrals over a set.
     1.8 +
     1.9 +TODO: keep all these? Need unicode translations as well.
    1.10 +*)
    1.11 +
    1.12 +theory Set_Integral
    1.13 +  imports Bochner_Integration Lebesgue_Measure
    1.14 +begin
    1.15 +
    1.16 +(*
    1.17 +    Notation
    1.18 +*)
    1.19 +
    1.20 +abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
    1.21 +
    1.22 +abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    1.23 +
    1.24 +abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
    1.25 +
    1.26 +syntax
    1.27 +"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    1.28 +("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
    1.29 +
    1.30 +translations
    1.31 +"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
    1.32 +
    1.33 +abbreviation
    1.34 +  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
    1.35 +
    1.36 +syntax
    1.37 +  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
    1.38 +("AE _\<in>_ in _./ _" [0,0,0,10] 10)
    1.39 +
    1.40 +translations
    1.41 +  "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
    1.42 +
    1.43 +(*
    1.44 +    Notation for integration wrt lebesgue measure on the reals:
    1.45 +
    1.46 +      LBINT x. f
    1.47 +      LBINT x : A. f
    1.48 +
    1.49 +    TODO: keep all these? Need unicode.
    1.50 +*)
    1.51 +
    1.52 +syntax
    1.53 +"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
    1.54 +("(2LBINT _./ _)" [0,60] 60)
    1.55 +
    1.56 +translations
    1.57 +"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
    1.58 +
    1.59 +syntax
    1.60 +"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
    1.61 +("(3LBINT _:_./ _)" [0,60,61] 60)
    1.62 +
    1.63 +translations
    1.64 +"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    1.65 +
    1.66 +(*
    1.67 +    Basic properties
    1.68 +*)
    1.69 +
    1.70 +(*
    1.71 +lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
    1.72 +  by (auto simp add: indicator_def)
    1.73 +*)
    1.74 +
    1.75 +lemma set_borel_measurable_sets:
    1.76 +  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
    1.77 +  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
    1.78 +  shows "f -` B \<inter> X \<in> sets M"
    1.79 +proof -
    1.80 +  have "f \<in> borel_measurable (restrict_space M X)"
    1.81 +    using assms by (subst borel_measurable_restrict_space_iff) auto
    1.82 +  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
    1.83 +    by (rule measurable_sets) fact
    1.84 +  with \<open>X \<in> sets M\<close> show ?thesis
    1.85 +    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
    1.86 +qed
    1.87 +
    1.88 +lemma set_lebesgue_integral_cong:
    1.89 +  assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
    1.90 +  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
    1.91 +  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
    1.92 +
    1.93 +lemma set_lebesgue_integral_cong_AE:
    1.94 +  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
    1.95 +  assumes "AE x \<in> A in M. f x = g x"
    1.96 +  shows "LINT x:A|M. f x = LINT x:A|M. g x"
    1.97 +proof-
    1.98 +  have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
    1.99 +    using assms by auto
   1.100 +  thus ?thesis by (intro integral_cong_AE) auto
   1.101 +qed
   1.102 +
   1.103 +lemma set_integrable_cong_AE:
   1.104 +    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
   1.105 +    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
   1.106 +    set_integrable M A f = set_integrable M A g"
   1.107 +  by (rule integrable_cong_AE) auto
   1.108 +
   1.109 +lemma set_integrable_subset:
   1.110 +  fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.111 +  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
   1.112 +  shows "set_integrable M B f"
   1.113 +proof -
   1.114 +  have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   1.115 +    by (rule integrable_mult_indicator) fact+
   1.116 +  with \<open>B \<subseteq> A\<close> show ?thesis
   1.117 +    by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
   1.118 +qed
   1.119 +
   1.120 +(* TODO: integral_cmul_indicator should be named set_integral_const *)
   1.121 +(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
   1.122 +
   1.123 +lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
   1.124 +  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
   1.125 +
   1.126 +lemma set_integral_mult_right [simp]:
   1.127 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   1.128 +  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
   1.129 +  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
   1.130 +
   1.131 +lemma set_integral_mult_left [simp]:
   1.132 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   1.133 +  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
   1.134 +  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
   1.135 +
   1.136 +lemma set_integral_divide_zero [simp]:
   1.137 +  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   1.138 +  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
   1.139 +  by (subst integral_divide_zero[symmetric], intro integral_cong)
   1.140 +     (auto split: split_indicator)
   1.141 +
   1.142 +lemma set_integrable_scaleR_right [simp, intro]:
   1.143 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
   1.144 +  unfolding scaleR_left_commute by (rule integrable_scaleR_right)
   1.145 +
   1.146 +lemma set_integrable_scaleR_left [simp, intro]:
   1.147 +  fixes a :: "_ :: {banach, second_countable_topology}"
   1.148 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
   1.149 +  using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   1.150 +
   1.151 +lemma set_integrable_mult_right [simp, intro]:
   1.152 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   1.153 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
   1.154 +  using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   1.155 +
   1.156 +lemma set_integrable_mult_left [simp, intro]:
   1.157 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   1.158 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
   1.159 +  using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   1.160 +
   1.161 +lemma set_integrable_divide [simp, intro]:
   1.162 +  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   1.163 +  assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
   1.164 +  shows "set_integrable M A (\<lambda>t. f t / a)"
   1.165 +proof -
   1.166 +  have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
   1.167 +    using assms by (rule integrable_divide_zero)
   1.168 +  also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
   1.169 +    by (auto split: split_indicator)
   1.170 +  finally show ?thesis .
   1.171 +qed
   1.172 +
   1.173 +lemma set_integral_add [simp, intro]:
   1.174 +  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.175 +  assumes "set_integrable M A f" "set_integrable M A g"
   1.176 +  shows "set_integrable M A (\<lambda>x. f x + g x)"
   1.177 +    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
   1.178 +  using assms by (simp_all add: scaleR_add_right)
   1.179 +
   1.180 +lemma set_integral_diff [simp, intro]:
   1.181 +  assumes "set_integrable M A f" "set_integrable M A g"
   1.182 +  shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
   1.183 +    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   1.184 +  using assms by (simp_all add: scaleR_diff_right)
   1.185 +
   1.186 +lemma set_integral_reflect:
   1.187 +  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.188 +  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   1.189 +  by (subst lborel_integral_real_affine[where c="-1" and t=0])
   1.190 +     (auto intro!: integral_cong split: split_indicator)
   1.191 +
   1.192 +(* question: why do we have this for negation, but multiplication by a constant
   1.193 +   requires an integrability assumption? *)
   1.194 +lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
   1.195 +  by (subst integral_minus[symmetric]) simp_all
   1.196 +
   1.197 +lemma set_integral_complex_of_real:
   1.198 +  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   1.199 +  by (subst integral_complex_of_real[symmetric])
   1.200 +     (auto intro!: integral_cong split: split_indicator)
   1.201 +
   1.202 +lemma set_integral_mono:
   1.203 +  fixes f g :: "_ \<Rightarrow> real"
   1.204 +  assumes "set_integrable M A f" "set_integrable M A g"
   1.205 +    "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   1.206 +  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   1.207 +using assms by (auto intro: integral_mono split: split_indicator)
   1.208 +
   1.209 +lemma set_integral_mono_AE:
   1.210 +  fixes f g :: "_ \<Rightarrow> real"
   1.211 +  assumes "set_integrable M A f" "set_integrable M A g"
   1.212 +    "AE x \<in> A in M. f x \<le> g x"
   1.213 +  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   1.214 +using assms by (auto intro: integral_mono_AE split: split_indicator)
   1.215 +
   1.216 +lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
   1.217 +  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
   1.218 +
   1.219 +lemma set_integrable_abs_iff:
   1.220 +  fixes f :: "_ \<Rightarrow> real"
   1.221 +  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
   1.222 +  by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
   1.223 +
   1.224 +lemma set_integrable_abs_iff':
   1.225 +  fixes f :: "_ \<Rightarrow> real"
   1.226 +  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
   1.227 +    set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
   1.228 +by (intro set_integrable_abs_iff) auto
   1.229 +
   1.230 +lemma set_integrable_discrete_difference:
   1.231 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.232 +  assumes "countable X"
   1.233 +  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   1.234 +  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   1.235 +  shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
   1.236 +proof (rule integrable_discrete_difference[where X=X])
   1.237 +  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
   1.238 +    using diff by (auto split: split_indicator)
   1.239 +qed fact+
   1.240 +
   1.241 +lemma set_integral_discrete_difference:
   1.242 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.243 +  assumes "countable X"
   1.244 +  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   1.245 +  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   1.246 +  shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
   1.247 +proof (rule integral_discrete_difference[where X=X])
   1.248 +  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
   1.249 +    using diff by (auto split: split_indicator)
   1.250 +qed fact+
   1.251 +
   1.252 +lemma set_integrable_Un:
   1.253 +  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.254 +  assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
   1.255 +    and [measurable]: "A \<in> sets M" "B \<in> sets M"
   1.256 +  shows "set_integrable M (A \<union> B) f"
   1.257 +proof -
   1.258 +  have "set_integrable M (A - B) f"
   1.259 +    using f_A by (rule set_integrable_subset) auto
   1.260 +  from integrable_add[OF this f_B] show ?thesis
   1.261 +    by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
   1.262 +qed
   1.263 +
   1.264 +lemma set_integrable_UN:
   1.265 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.266 +  assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
   1.267 +    "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   1.268 +  shows "set_integrable M (\<Union>i\<in>I. A i) f"
   1.269 +using assms by (induct I) (auto intro!: set_integrable_Un)
   1.270 +
   1.271 +lemma set_integral_Un:
   1.272 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.273 +  assumes "A \<inter> B = {}"
   1.274 +  and "set_integrable M A f"
   1.275 +  and "set_integrable M B f"
   1.276 +  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   1.277 +by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
   1.278 +      scaleR_add_left assms)
   1.279 +
   1.280 +lemma set_integral_cong_set:
   1.281 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.282 +  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
   1.283 +    and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   1.284 +  shows "LINT x:B|M. f x = LINT x:A|M. f x"
   1.285 +proof (rule integral_cong_AE)
   1.286 +  show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
   1.287 +    using ae by (auto simp: subset_eq split: split_indicator)
   1.288 +qed fact+
   1.289 +
   1.290 +lemma set_borel_measurable_subset:
   1.291 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.292 +  assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
   1.293 +  shows "set_borel_measurable M B f"
   1.294 +proof -
   1.295 +  have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   1.296 +    by measurable
   1.297 +  also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
   1.298 +    using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
   1.299 +  finally show ?thesis .
   1.300 +qed
   1.301 +
   1.302 +lemma set_integral_Un_AE:
   1.303 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.304 +  assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
   1.305 +  and "set_integrable M A f"
   1.306 +  and "set_integrable M B f"
   1.307 +  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   1.308 +proof -
   1.309 +  have f: "set_integrable M (A \<union> B) f"
   1.310 +    by (intro set_integrable_Un assms)
   1.311 +  then have f': "set_borel_measurable M (A \<union> B) f"
   1.312 +    by (rule borel_measurable_integrable)
   1.313 +  have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
   1.314 +  proof (rule set_integral_cong_set)
   1.315 +    show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
   1.316 +      using ae by auto
   1.317 +    show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
   1.318 +      using f' by (rule set_borel_measurable_subset) auto
   1.319 +  qed fact
   1.320 +  also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
   1.321 +    by (auto intro!: set_integral_Un set_integrable_subset[OF f])
   1.322 +  also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   1.323 +    using ae
   1.324 +    by (intro arg_cong2[where f="op+"] set_integral_cong_set)
   1.325 +       (auto intro!: set_borel_measurable_subset[OF f'])
   1.326 +  finally show ?thesis .
   1.327 +qed
   1.328 +
   1.329 +lemma set_integral_finite_Union:
   1.330 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   1.331 +  assumes "finite I" "disjoint_family_on A I"
   1.332 +    and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   1.333 +  shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   1.334 +  using assms
   1.335 +  apply induct
   1.336 +  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
   1.337 +by (subst set_integral_Un, auto intro: set_integrable_UN)
   1.338 +
   1.339 +(* TODO: find a better name? *)
   1.340 +lemma pos_integrable_to_top:
   1.341 +  fixes l::real
   1.342 +  assumes "\<And>i. A i \<in> sets M" "mono A"
   1.343 +  assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
   1.344 +  and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   1.345 +  and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
   1.346 +  shows "set_integrable M (\<Union>i. A i) f"
   1.347 +  apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
   1.348 +  apply (rule intgbl)
   1.349 +  prefer 3 apply (rule lim)
   1.350 +  apply (rule AE_I2)
   1.351 +  using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
   1.352 +proof (rule AE_I2)
   1.353 +  { fix x assume "x \<in> space M"
   1.354 +    show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
   1.355 +    proof cases
   1.356 +      assume "\<exists>i. x \<in> A i"
   1.357 +      then guess i ..
   1.358 +      then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
   1.359 +        using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
   1.360 +      show ?thesis
   1.361 +        apply (intro Lim_eventually)
   1.362 +        using *
   1.363 +        apply eventually_elim
   1.364 +        apply (auto split: split_indicator)
   1.365 +        done
   1.366 +    qed auto }
   1.367 +  then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
   1.368 +    apply (rule borel_measurable_LIMSEQ_real)
   1.369 +    apply assumption
   1.370 +    apply (intro borel_measurable_integrable intgbl)
   1.371 +    done
   1.372 +qed
   1.373 +
   1.374 +(* Proof from Royden Real Analysis, p. 91. *)
   1.375 +lemma lebesgue_integral_countable_add:
   1.376 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.377 +  assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
   1.378 +    and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   1.379 +    and intgbl: "set_integrable M (\<Union>i. A i) f"
   1.380 +  shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
   1.381 +proof (subst integral_suminf[symmetric])
   1.382 +  show int_A: "\<And>i. set_integrable M (A i) f"
   1.383 +    using intgbl by (rule set_integrable_subset) auto
   1.384 +  { fix x assume "x \<in> space M"
   1.385 +    have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
   1.386 +      by (intro sums_scaleR_left indicator_sums) fact }
   1.387 +  note sums = this
   1.388 +
   1.389 +  have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
   1.390 +    using int_A[THEN integrable_norm] by auto
   1.391 +
   1.392 +  show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
   1.393 +    using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
   1.394 +
   1.395 +  show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
   1.396 +  proof (rule summableI_nonneg_bounded)
   1.397 +    fix n
   1.398 +    show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
   1.399 +      using norm_f by (auto intro!: integral_nonneg_AE)
   1.400 +
   1.401 +    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
   1.402 +      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
   1.403 +      by (simp add: abs_mult)
   1.404 +    also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
   1.405 +      using norm_f
   1.406 +      by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
   1.407 +    also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   1.408 +      using intgbl[THEN integrable_norm]
   1.409 +      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
   1.410 +         (auto split: split_indicator)
   1.411 +    finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
   1.412 +      set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   1.413 +      by simp
   1.414 +  qed
   1.415 +  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   1.416 +    apply (rule integral_cong[OF refl])
   1.417 +    apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
   1.418 +    using sums_unique[OF indicator_sums[OF disj]]
   1.419 +    apply auto
   1.420 +    done
   1.421 +qed
   1.422 +
   1.423 +lemma set_integral_cont_up:
   1.424 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.425 +  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   1.426 +  and intgbl: "set_integrable M (\<Union>i. A i) f"
   1.427 +  shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
   1.428 +proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   1.429 +  have int_A: "\<And>i. set_integrable M (A i) f"
   1.430 +    using intgbl by (rule set_integrable_subset) auto
   1.431 +  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
   1.432 +    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   1.433 +    using intgbl integrable_norm[OF intgbl] by auto
   1.434 +
   1.435 +  { fix x i assume "x \<in> A i"
   1.436 +    with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
   1.437 +      by (intro filterlim_cong refl)
   1.438 +         (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
   1.439 +  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
   1.440 +    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   1.441 +qed (auto split: split_indicator)
   1.442 +
   1.443 +(* Can the int0 hypothesis be dropped? *)
   1.444 +lemma set_integral_cont_down:
   1.445 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.446 +  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   1.447 +  and int0: "set_integrable M (A 0) f"
   1.448 +  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
   1.449 +proof (rule integral_dominated_convergence)
   1.450 +  have int_A: "\<And>i. set_integrable M (A i) f"
   1.451 +    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   1.452 +  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
   1.453 +    using int0[THEN integrable_norm] by simp
   1.454 +  have "set_integrable M (\<Inter>i. A i) f"
   1.455 +    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   1.456 +  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
   1.457 +    by auto
   1.458 +  show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
   1.459 +    using A by (auto split: split_indicator simp: decseq_def)
   1.460 +  { fix x i assume "x \<in> space M" "x \<notin> A i"
   1.461 +    with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
   1.462 +      by (intro filterlim_cong refl)
   1.463 +         (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
   1.464 +  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x"
   1.465 +    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   1.466 +qed
   1.467 +
   1.468 +lemma set_integral_at_point:
   1.469 +  fixes a :: real
   1.470 +  assumes "set_integrable M {a} f"
   1.471 +  and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
   1.472 +  shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
   1.473 +proof-
   1.474 +  have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
   1.475 +    by (intro set_lebesgue_integral_cong) simp_all
   1.476 +  then show ?thesis using assms by simp
   1.477 +qed
   1.478 +
   1.479 +
   1.480 +abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   1.481 +  "complex_integrable M f \<equiv> integrable M f"
   1.482 +
   1.483 +abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
   1.484 +  "integral\<^sup>C M f == integral\<^sup>L M f"
   1.485 +
   1.486 +syntax
   1.487 +  "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
   1.488 + ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
   1.489 +
   1.490 +translations
   1.491 +  "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   1.492 +
   1.493 +syntax
   1.494 +  "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   1.495 +  ("(3CLINT _|_. _)" [0,110,60] 60)
   1.496 +
   1.497 +translations
   1.498 +  "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   1.499 +
   1.500 +lemma complex_integrable_cnj [simp]:
   1.501 +  "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
   1.502 +proof
   1.503 +  assume "complex_integrable M (\<lambda>x. cnj (f x))"
   1.504 +  then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
   1.505 +    by (rule integrable_cnj)
   1.506 +  then show "complex_integrable M f"
   1.507 +    by simp
   1.508 +qed simp
   1.509 +
   1.510 +lemma complex_of_real_integrable_eq:
   1.511 +  "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
   1.512 +proof
   1.513 +  assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
   1.514 +  then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
   1.515 +    by (rule integrable_Re)
   1.516 +  then show "integrable M f"
   1.517 +    by simp
   1.518 +qed simp
   1.519 +
   1.520 +
   1.521 +abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   1.522 +  "complex_set_integrable M A f \<equiv> set_integrable M A f"
   1.523 +
   1.524 +abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
   1.525 +  "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
   1.526 +
   1.527 +syntax
   1.528 +"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   1.529 +("(4CLINT _:_|_. _)" [0,60,110,61] 60)
   1.530 +
   1.531 +translations
   1.532 +"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
   1.533 +
   1.534 +(*
   1.535 +lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
   1.536 +  apply (simp add: norm_mult)
   1.537 +  by (subst norm_mult, auto)
   1.538 +*)
   1.539 +
   1.540 +lemma borel_integrable_atLeastAtMost':
   1.541 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   1.542 +  assumes f: "continuous_on {a..b} f"
   1.543 +  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
   1.544 +  by (intro borel_integrable_compact compact_Icc f)
   1.545 +
   1.546 +lemma integral_FTC_atLeastAtMost:
   1.547 +  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   1.548 +  assumes "a \<le> b"
   1.549 +    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   1.550 +    and f: "continuous_on {a .. b} f"
   1.551 +  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
   1.552 +proof -
   1.553 +  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   1.554 +  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
   1.555 +    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
   1.556 +  moreover
   1.557 +  have "(f has_integral F b - F a) {a .. b}"
   1.558 +    by (intro fundamental_theorem_of_calculus ballI assms) auto
   1.559 +  then have "(?f has_integral F b - F a) {a .. b}"
   1.560 +    by (subst has_integral_cong[where g=f]) auto
   1.561 +  then have "(?f has_integral F b - F a) UNIV"
   1.562 +    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
   1.563 +  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
   1.564 +    by (rule has_integral_unique)
   1.565 +qed
   1.566 +
   1.567 +lemma set_borel_integral_eq_integral:
   1.568 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   1.569 +  assumes "set_integrable lborel S f"
   1.570 +  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
   1.571 +proof -
   1.572 +  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   1.573 +  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
   1.574 +    by (rule has_integral_integral_lborel) fact
   1.575 +  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
   1.576 +    apply (subst has_integral_restrict_univ [symmetric])
   1.577 +    apply (rule has_integral_eq)
   1.578 +    by auto
   1.579 +  thus "f integrable_on S"
   1.580 +    by (auto simp add: integrable_on_def)
   1.581 +  with 1 have "(f has_integral (integral S f)) S"
   1.582 +    by (intro integrable_integral, auto simp add: integrable_on_def)
   1.583 +  thus "LINT x : S | lborel. f x = integral S f"
   1.584 +    by (intro has_integral_unique [OF 1])
   1.585 +qed
   1.586 +
   1.587 +lemma set_borel_measurable_continuous:
   1.588 +  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   1.589 +  assumes "S \<in> sets borel" "continuous_on S f"
   1.590 +  shows "set_borel_measurable borel S f"
   1.591 +proof -
   1.592 +  have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
   1.593 +    by (intro assms borel_measurable_continuous_on_if continuous_on_const)
   1.594 +  also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
   1.595 +    by auto
   1.596 +  finally show ?thesis .
   1.597 +qed
   1.598 +
   1.599 +lemma set_measurable_continuous_on_ivl:
   1.600 +  assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
   1.601 +  shows "set_borel_measurable borel {a..b} f"
   1.602 +  by (rule set_borel_measurable_continuous[OF _ assms]) simp
   1.603 +
   1.604 +end
   1.605 +