src/HOL/Probability/Set_Integral.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59867 58043346ca64
child 60615 e5fa1d5d3952
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (*  Title:      HOL/Probability/Set_Integral.thy
     2     Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin
     3 
     4 Notation and useful facts for working with integrals over a set.
     5 
     6 TODO: keep all these? Need unicode translations as well.
     7 *)
     8 
     9 theory Set_Integral
    10   imports Bochner_Integration Lebesgue_Measure
    11 begin
    12 
    13 (* 
    14     Notation
    15 *)
    16 
    17 syntax
    18 "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    19 ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
    20 
    21 translations
    22 "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
    23 
    24 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
    25 
    26 abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    27 
    28 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
    29 
    30 syntax
    31 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    32 ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
    33 
    34 translations
    35 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
    36 
    37 abbreviation
    38   "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
    39 
    40 syntax
    41   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
    42 ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
    43 
    44 translations
    45   "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
    46 
    47 (*
    48     Notation for integration wrt lebesgue measure on the reals:
    49 
    50       LBINT x. f
    51       LBINT x : A. f
    52 
    53     TODO: keep all these? Need unicode.
    54 *)
    55 
    56 syntax
    57 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
    58 ("(2LBINT _./ _)" [0,60] 60)
    59 
    60 translations
    61 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
    62 
    63 syntax
    64 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
    65 ("(3LBINT _:_./ _)" [0,60,61] 60)
    66 
    67 translations
    68 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    69 
    70 (* 
    71     Basic properties 
    72 *)
    73 
    74 (*
    75 lemma indicator_abs_eq: "\<And>A x. abs (indicator A x) = ((indicator A x) :: real)"
    76   by (auto simp add: indicator_def)
    77 *)
    78 
    79 lemma set_lebesgue_integral_cong:
    80   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
    81   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
    82   using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
    83 
    84 lemma set_lebesgue_integral_cong_AE:
    85   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
    86   assumes "AE x \<in> A in M. f x = g x"
    87   shows "LINT x:A|M. f x = LINT x:A|M. g x"
    88 proof-
    89   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
    90     using assms by auto
    91   thus ?thesis by (intro integral_cong_AE) auto
    92 qed
    93 
    94 lemma set_integrable_cong_AE:
    95     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
    96     AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
    97     set_integrable M A f = set_integrable M A g"
    98   by (rule integrable_cong_AE) auto
    99 
   100 lemma set_integrable_subset: 
   101   fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   102   assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"  
   103   shows "set_integrable M B f"
   104 proof -
   105   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   106     by (rule integrable_mult_indicator) fact+
   107   with `B \<subseteq> A` show ?thesis
   108     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
   109 qed
   110 
   111 (* TODO: integral_cmul_indicator should be named set_integral_const *)
   112 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
   113 
   114 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
   115   by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
   116 
   117 lemma set_integral_mult_right [simp]: 
   118   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   119   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
   120   by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
   121 
   122 lemma set_integral_mult_left [simp]: 
   123   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   124   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
   125   by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
   126 
   127 lemma set_integral_divide_zero [simp]: 
   128   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   129   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
   130   by (subst integral_divide_zero[symmetric], intro integral_cong)
   131      (auto split: split_indicator)
   132 
   133 lemma set_integrable_scaleR_right [simp, intro]:
   134   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
   135   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
   136 
   137 lemma set_integrable_scaleR_left [simp, intro]:
   138   fixes a :: "_ :: {banach, second_countable_topology}"
   139   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
   140   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   141 
   142 lemma set_integrable_mult_right [simp, intro]:
   143   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   144   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
   145   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   146 
   147 lemma set_integrable_mult_left [simp, intro]:
   148   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   149   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
   150   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   151 
   152 lemma set_integrable_divide [simp, intro]:
   153   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   154   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
   155   shows "set_integrable M A (\<lambda>t. f t / a)"
   156 proof -
   157   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
   158     using assms by (rule integrable_divide_zero)
   159   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
   160     by (auto split: split_indicator)
   161   finally show ?thesis .
   162 qed
   163 
   164 lemma set_integral_add [simp, intro]:
   165   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   166   assumes "set_integrable M A f" "set_integrable M A g"
   167   shows "set_integrable M A (\<lambda>x. f x + g x)"
   168     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
   169   using assms by (simp_all add: scaleR_add_right)
   170 
   171 lemma set_integral_diff [simp, intro]:
   172   assumes "set_integrable M A f" "set_integrable M A g"
   173   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
   174     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   175   using assms by (simp_all add: scaleR_diff_right)
   176 
   177 lemma set_integral_reflect:
   178   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   179   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   180   using assms
   181   by (subst lborel_integral_real_affine[where c="-1" and t=0])
   182      (auto intro!: integral_cong split: split_indicator)
   183 
   184 (* question: why do we have this for negation, but multiplication by a constant
   185    requires an integrability assumption? *)
   186 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
   187   by (subst integral_minus[symmetric]) simp_all
   188 
   189 lemma set_integral_complex_of_real:
   190   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   191   by (subst integral_complex_of_real[symmetric])
   192      (auto intro!: integral_cong split: split_indicator)
   193 
   194 lemma set_integral_mono:
   195   fixes f g :: "_ \<Rightarrow> real"
   196   assumes "set_integrable M A f" "set_integrable M A g"
   197     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   198   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   199 using assms by (auto intro: integral_mono split: split_indicator)
   200 
   201 lemma set_integral_mono_AE: 
   202   fixes f g :: "_ \<Rightarrow> real"
   203   assumes "set_integrable M A f" "set_integrable M A g"
   204     "AE x \<in> A in M. f x \<le> g x"
   205   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   206 using assms by (auto intro: integral_mono_AE split: split_indicator)
   207 
   208 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
   209   using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
   210 
   211 lemma set_integrable_abs_iff:
   212   fixes f :: "_ \<Rightarrow> real"
   213   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" 
   214   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
   215 
   216 lemma set_integrable_abs_iff':
   217   fixes f :: "_ \<Rightarrow> real"
   218   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
   219     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
   220 by (intro set_integrable_abs_iff) auto
   221 
   222 lemma set_integrable_discrete_difference:
   223   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   224   assumes "countable X"
   225   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   226   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   227   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
   228 proof (rule integrable_discrete_difference[where X=X])
   229   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"
   230     using diff by (auto split: split_indicator)
   231 qed fact+
   232 
   233 lemma set_integral_discrete_difference:
   234   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   235   assumes "countable X"
   236   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   237   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   238   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
   239 proof (rule integral_discrete_difference[where X=X])
   240   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"
   241     using diff by (auto split: split_indicator)
   242 qed fact+
   243 
   244 lemma set_integrable_Un:
   245   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   246   assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
   247     and [measurable]: "A \<in> sets M" "B \<in> sets M"
   248   shows "set_integrable M (A \<union> B) f"
   249 proof -
   250   have "set_integrable M (A - B) f"
   251     using f_A by (rule set_integrable_subset) auto
   252   from integrable_add[OF this f_B] show ?thesis
   253     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
   254 qed
   255 
   256 lemma set_integrable_UN:
   257   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   258   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
   259     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   260   shows "set_integrable M (\<Union>i\<in>I. A i) f"
   261 using assms by (induct I) (auto intro!: set_integrable_Un)
   262 
   263 lemma set_integral_Un:
   264   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   265   assumes "A \<inter> B = {}"
   266   and "set_integrable M A f"
   267   and "set_integrable M B f"
   268   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   269 by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
   270       scaleR_add_left assms)
   271 
   272 lemma set_integral_cong_set:
   273   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   274   assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
   275     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   276   shows "LINT x:B|M. f x = LINT x:A|M. f x"
   277 proof (rule integral_cong_AE)
   278   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
   279     using ae by (auto simp: subset_eq split: split_indicator)
   280 qed fact+
   281 
   282 lemma set_borel_measurable_subset:
   283   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   284   assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
   285   shows "set_borel_measurable M B f"
   286 proof -
   287   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   288     by measurable
   289   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)"
   290     using `B \<subseteq> A` by (auto simp: fun_eq_iff split: split_indicator)
   291   finally show ?thesis .
   292 qed
   293 
   294 lemma set_integral_Un_AE:
   295   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   296   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
   297   and "set_integrable M A f"
   298   and "set_integrable M B f"
   299   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   300 proof -
   301   have f: "set_integrable M (A \<union> B) f"
   302     by (intro set_integrable_Un assms)
   303   then have f': "set_borel_measurable M (A \<union> B) f"
   304     by (rule borel_measurable_integrable)
   305   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
   306   proof (rule set_integral_cong_set)  
   307     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
   308       using ae by auto
   309     show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
   310       using f' by (rule set_borel_measurable_subset) auto
   311   qed fact
   312   also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
   313     by (auto intro!: set_integral_Un set_integrable_subset[OF f])
   314   also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   315     using ae
   316     by (intro arg_cong2[where f="op+"] set_integral_cong_set)
   317        (auto intro!: set_borel_measurable_subset[OF f'])
   318   finally show ?thesis .
   319 qed
   320 
   321 lemma set_integral_finite_Union:
   322   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   323   assumes "finite I" "disjoint_family_on A I"
   324     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   325   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   326   using assms
   327   apply induct
   328   apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
   329 by (subst set_integral_Un, auto intro: set_integrable_UN)
   330 
   331 (* TODO: find a better name? *)
   332 lemma pos_integrable_to_top:
   333   fixes l::real
   334   assumes "\<And>i. A i \<in> sets M" "mono A"
   335   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
   336   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   337   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) ----> l"
   338   shows "set_integrable M (\<Union>i. A i) f"
   339   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
   340   apply (rule intgbl)
   341   prefer 3 apply (rule lim)
   342   apply (rule AE_I2)
   343   using `mono A` apply (auto simp: mono_def nneg split: split_indicator) []
   344 proof (rule AE_I2)
   345   { fix x assume "x \<in> space M"
   346     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
   347     proof cases
   348       assume "\<exists>i. x \<in> A i"
   349       then guess i ..
   350       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
   351         using `x \<in> A i` `mono A` by (auto simp: eventually_sequentially mono_def)
   352       show ?thesis
   353         apply (intro Lim_eventually)
   354         using *
   355         apply eventually_elim
   356         apply (auto split: split_indicator)
   357         done
   358     qed auto }
   359   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
   360     apply (rule borel_measurable_LIMSEQ)
   361     apply assumption
   362     apply (intro borel_measurable_integrable intgbl)
   363     done
   364 qed
   365 
   366 (* Proof from Royden Real Analysis, p. 91. *)
   367 lemma lebesgue_integral_countable_add:
   368   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   369   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
   370     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   371     and intgbl: "set_integrable M (\<Union>i. A i) f"
   372   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
   373 proof (subst integral_suminf[symmetric])
   374   show int_A: "\<And>i. set_integrable M (A i) f"
   375     using intgbl by (rule set_integrable_subset) auto
   376   { fix x assume "x \<in> space M"
   377     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
   378       by (intro sums_scaleR_left indicator_sums) fact }
   379   note sums = this
   380 
   381   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
   382     using int_A[THEN integrable_norm] by auto
   383 
   384   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
   385     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
   386 
   387   show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
   388   proof (rule summableI_nonneg_bounded)
   389     fix n
   390     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
   391       using norm_f by (auto intro!: integral_nonneg_AE)
   392     
   393     have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
   394       (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
   395       by (simp add: abs_mult)
   396     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
   397       using norm_f
   398       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
   399     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   400       using intgbl[THEN integrable_norm]
   401       by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
   402          (auto split: split_indicator)
   403     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
   404       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   405       by simp
   406   qed
   407   show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   408     apply (rule integral_cong[OF refl])
   409     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
   410     using sums_unique[OF indicator_sums[OF disj]]
   411     apply auto
   412     done
   413 qed
   414 
   415 lemma set_integral_cont_up:
   416   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   417   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   418   and intgbl: "set_integrable M (\<Union>i. A i) f"
   419   shows "(\<lambda>i. LINT x:(A i)|M. f x) ----> LINT x:(\<Union>i. A i)|M. f x"
   420 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   421   have int_A: "\<And>i. set_integrable M (A i) f"
   422     using intgbl by (rule set_integrable_subset) auto
   423   then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
   424     "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   425     using intgbl integrable_norm[OF intgbl] by auto
   426   
   427   { fix x i assume "x \<in> A i"
   428     with A have "(\<lambda>xa. indicator (A xa) x::real) ----> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) ----> 1"
   429       by (intro filterlim_cong refl)
   430          (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
   431   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
   432     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   433 qed (auto split: split_indicator)
   434         
   435 (* Can the int0 hypothesis be dropped? *)
   436 lemma set_integral_cont_down:
   437   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   438   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   439   and int0: "set_integrable M (A 0) f"
   440   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) ----> LINT x:(\<Inter>i. A i)|M. f x"
   441 proof (rule integral_dominated_convergence)
   442   have int_A: "\<And>i. set_integrable M (A i) f"
   443     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   444   show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
   445     using int0[THEN integrable_norm] by simp
   446   have "set_integrable M (\<Inter>i. A i) f"
   447     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   448   with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
   449     by auto
   450   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)"
   451     using A by (auto split: split_indicator simp: decseq_def)
   452   { fix x i assume "x \<in> space M" "x \<notin> A i"
   453     with A have "(\<lambda>i. indicator (A i) x::real) ----> 0 \<longleftrightarrow> (\<lambda>i. 0::real) ----> 0"
   454       by (intro filterlim_cong refl)
   455          (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
   456   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Inter>i. A i) x *\<^sub>R f x"
   457     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   458 qed
   459 
   460 lemma set_integral_at_point:
   461   fixes a :: real
   462   assumes "set_integrable M {a} f"
   463   and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
   464   shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
   465 proof-
   466   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
   467     by (intro set_lebesgue_integral_cong) simp_all
   468   then show ?thesis using assms by simp
   469 qed
   470 
   471 
   472 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   473   "complex_integrable M f \<equiv> integrable M f"
   474 
   475 abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
   476   "integral\<^sup>C M f == integral\<^sup>L M f"
   477 
   478 syntax
   479   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
   480  ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
   481 
   482 translations
   483   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   484 
   485 syntax
   486   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   487   ("(3CLINT _|_. _)" [0,110,60] 60)
   488 
   489 translations
   490   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   491 
   492 lemma complex_integrable_cnj [simp]:
   493   "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
   494 proof
   495   assume "complex_integrable M (\<lambda>x. cnj (f x))"
   496   then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
   497     by (rule integrable_cnj)
   498   then show "complex_integrable M f"
   499     by simp
   500 qed simp
   501 
   502 lemma complex_of_real_integrable_eq:
   503   "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
   504 proof
   505   assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
   506   then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
   507     by (rule integrable_Re)
   508   then show "integrable M f"
   509     by simp
   510 qed simp
   511 
   512 
   513 abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   514   "complex_set_integrable M A f \<equiv> set_integrable M A f"
   515 
   516 abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
   517   "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
   518 
   519 syntax
   520 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   521 ("(4CLINT _:_|_. _)" [0,60,110,61] 60)
   522 
   523 translations
   524 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
   525 
   526 (*
   527 lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = abs a * cmod x"
   528   apply (simp add: norm_mult)
   529   by (subst norm_mult, auto)
   530 *)
   531 
   532 lemma borel_integrable_atLeastAtMost':
   533   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   534   assumes f: "continuous_on {a..b} f"
   535   shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
   536   by (intro borel_integrable_compact compact_Icc f)
   537 
   538 lemma integral_FTC_atLeastAtMost:
   539   fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   540   assumes "a \<le> b"
   541     and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   542     and f: "continuous_on {a .. b} f"
   543   shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
   544 proof -
   545   let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   546   have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
   547     using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
   548   moreover
   549   have "(f has_integral F b - F a) {a .. b}"
   550     by (intro fundamental_theorem_of_calculus ballI assms) auto
   551   then have "(?f has_integral F b - F a) {a .. b}"
   552     by (subst has_integral_eq_eq[where g=f]) auto
   553   then have "(?f has_integral F b - F a) UNIV"
   554     by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
   555   ultimately show "integral\<^sup>L lborel ?f = F b - F a"
   556     by (rule has_integral_unique)
   557 qed
   558 
   559 lemma set_borel_integral_eq_integral:
   560   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   561   assumes "set_integrable lborel S f"
   562   shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
   563 proof -
   564   let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   565   have "(?f has_integral LINT x : S | lborel. f x) UNIV"
   566     by (rule has_integral_integral_lborel) fact
   567   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
   568     apply (subst has_integral_restrict_univ [symmetric])
   569     apply (rule has_integral_eq)
   570     by auto
   571   thus "f integrable_on S"
   572     by (auto simp add: integrable_on_def)
   573   with 1 have "(f has_integral (integral S f)) S"
   574     by (intro integrable_integral, auto simp add: integrable_on_def)
   575   thus "LINT x : S | lborel. f x = integral S f"
   576     by (intro has_integral_unique [OF 1])
   577 qed
   578 
   579 lemma set_borel_measurable_continuous:
   580   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   581   assumes "S \<in> sets borel" "continuous_on S f"
   582   shows "set_borel_measurable borel S f"
   583 proof -
   584   have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
   585     by (intro assms borel_measurable_continuous_on_if continuous_on_const)
   586   also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
   587     by auto
   588   finally show ?thesis .
   589 qed
   590 
   591 lemma set_measurable_continuous_on_ivl:
   592   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
   593   shows "set_borel_measurable borel {a..b} f"
   594   by (rule set_borel_measurable_continuous[OF _ assms]) simp
   595 
   596 end
   597