src/HOL/Probability/Bochner_Integration.thy
author hoelzl
Fri May 30 15:56:30 2014 +0200 (2014-05-30)
changeset 57137 f174712d0a84
parent 57036 22568fb89165
child 57166 5cfcc616d485
permissions -rw-r--r--
better support for restrict_space
hoelzl@56993
     1
(*  Title:      HOL/Probability/Bochner_Integration.thy
hoelzl@56993
     2
    Author:     Johannes Hölzl, TU München
hoelzl@56993
     3
*)
hoelzl@56993
     4
hoelzl@56993
     5
header {* Bochner Integration for Vector-Valued Functions *}
hoelzl@56993
     6
hoelzl@56993
     7
theory Bochner_Integration
hoelzl@56993
     8
  imports Finite_Product_Measure
hoelzl@56993
     9
begin
hoelzl@56993
    10
hoelzl@56993
    11
text {*
hoelzl@56993
    12
hoelzl@56993
    13
In the following development of the Bochner integral we use second countable topologies instead
hoelzl@56993
    14
of separable spaces. A second countable topology is also separable.
hoelzl@56993
    15
hoelzl@56993
    16
*}
hoelzl@56993
    17
hoelzl@56993
    18
lemma borel_measurable_implies_sequence_metric:
hoelzl@56993
    19
  fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}"
hoelzl@56993
    20
  assumes [measurable]: "f \<in> borel_measurable M"
hoelzl@56993
    21
  shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) ----> f x) \<and>
hoelzl@56993
    22
    (\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
hoelzl@56993
    23
proof -
hoelzl@56993
    24
  obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
hoelzl@56993
    25
    by (erule countable_dense_setE)
hoelzl@56993
    26
hoelzl@56993
    27
  def e \<equiv> "from_nat_into D"
hoelzl@56993
    28
  { fix n x
hoelzl@56993
    29
    obtain d where "d \<in> D" and d: "d \<in> ball x (1 / Suc n)"
hoelzl@56993
    30
      using D[of "ball x (1 / Suc n)"] by auto
hoelzl@56993
    31
    from `d \<in> D` D[of UNIV] `countable D` obtain i where "d = e i"
hoelzl@56993
    32
      unfolding e_def by (auto dest: from_nat_into_surj)
hoelzl@56993
    33
    with d have "\<exists>i. dist x (e i) < 1 / Suc n"
hoelzl@56993
    34
      by auto }
hoelzl@56993
    35
  note e = this
hoelzl@56993
    36
hoelzl@56993
    37
  def A \<equiv> "\<lambda>m n. {x\<in>space M. dist (f x) (e n) < 1 / (Suc m) \<and> 1 / (Suc m) \<le> dist (f x) z}"
hoelzl@56993
    38
  def B \<equiv> "\<lambda>m. disjointed (A m)"
hoelzl@56993
    39
  
hoelzl@56993
    40
  def m \<equiv> "\<lambda>N x. Max {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}"
hoelzl@56993
    41
  def F \<equiv> "\<lambda>N::nat. \<lambda>x. if (\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)) \<and> (\<exists>n\<le>N. x \<in> B (m N x) n) 
hoelzl@56993
    42
    then e (LEAST n. x \<in> B (m N x) n) else z"
hoelzl@56993
    43
hoelzl@56993
    44
  have B_imp_A[intro, simp]: "\<And>x m n. x \<in> B m n \<Longrightarrow> x \<in> A m n"
hoelzl@56993
    45
    using disjointed_subset[of "A m" for m] unfolding B_def by auto
hoelzl@56993
    46
hoelzl@56993
    47
  { fix m
hoelzl@56993
    48
    have "\<And>n. A m n \<in> sets M"
hoelzl@56993
    49
      by (auto simp: A_def)
hoelzl@56993
    50
    then have "\<And>n. B m n \<in> sets M"
hoelzl@56993
    51
      using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) }
hoelzl@56993
    52
  note this[measurable]
hoelzl@56993
    53
hoelzl@56993
    54
  { fix N i x assume "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)"
hoelzl@56993
    55
    then have "m N x \<in> {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}"
hoelzl@56993
    56
      unfolding m_def by (intro Max_in) auto
hoelzl@56993
    57
    then have "m N x \<le> N" "\<exists>n\<le>N. x \<in> B (m N x) n"
hoelzl@56993
    58
      by auto }
hoelzl@56993
    59
  note m = this
hoelzl@56993
    60
hoelzl@56993
    61
  { fix j N i x assume "j \<le> N" "i \<le> N" "x \<in> B j i"
hoelzl@56993
    62
    then have "j \<le> m N x"
hoelzl@56993
    63
      unfolding m_def by (intro Max_ge) auto }
hoelzl@56993
    64
  note m_upper = this
hoelzl@56993
    65
hoelzl@56993
    66
  show ?thesis
hoelzl@56993
    67
    unfolding simple_function_def
hoelzl@56993
    68
  proof (safe intro!: exI[of _ F])
hoelzl@56993
    69
    have [measurable]: "\<And>i. F i \<in> borel_measurable M"
hoelzl@56993
    70
      unfolding F_def m_def by measurable
hoelzl@56993
    71
    show "\<And>x i. F i -` {x} \<inter> space M \<in> sets M"
hoelzl@56993
    72
      by measurable
hoelzl@56993
    73
hoelzl@56993
    74
    { fix i
hoelzl@56993
    75
      { fix n x assume "x \<in> B (m i x) n"
hoelzl@56993
    76
        then have "(LEAST n. x \<in> B (m i x) n) \<le> n"
hoelzl@56993
    77
          by (intro Least_le)
hoelzl@56993
    78
        also assume "n \<le> i" 
hoelzl@56993
    79
        finally have "(LEAST n. x \<in> B (m i x) n) \<le> i" . }
hoelzl@56993
    80
      then have "F i ` space M \<subseteq> {z} \<union> e ` {.. i}"
hoelzl@56993
    81
        by (auto simp: F_def)
hoelzl@56993
    82
      then show "finite (F i ` space M)"
hoelzl@56993
    83
        by (rule finite_subset) auto }
hoelzl@56993
    84
    
hoelzl@56993
    85
    { fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
hoelzl@56993
    86
      then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto
hoelzl@56993
    87
      from m[OF this] obtain n where n: "m N x \<le> N" "n \<le> N" "x \<in> B (m N x) n" by auto
hoelzl@56993
    88
      moreover
hoelzl@56993
    89
      def L \<equiv> "LEAST n. x \<in> B (m N x) n"
hoelzl@56993
    90
      have "dist (f x) (e L) < 1 / Suc (m N x)"
hoelzl@56993
    91
      proof -
hoelzl@56993
    92
        have "x \<in> B (m N x) L"
hoelzl@56993
    93
          using n(3) unfolding L_def by (rule LeastI)
hoelzl@56993
    94
        then have "x \<in> A (m N x) L"
hoelzl@56993
    95
          by auto
hoelzl@56993
    96
        then show ?thesis
hoelzl@56993
    97
          unfolding A_def by simp
hoelzl@56993
    98
      qed
hoelzl@56993
    99
      ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)"
hoelzl@56993
   100
        by (auto simp add: F_def L_def) }
hoelzl@56993
   101
    note * = this
hoelzl@56993
   102
hoelzl@56993
   103
    fix x assume "x \<in> space M"
hoelzl@56993
   104
    show "(\<lambda>i. F i x) ----> f x"
hoelzl@56993
   105
    proof cases
hoelzl@56993
   106
      assume "f x = z"
hoelzl@56993
   107
      then have "\<And>i n. x \<notin> A i n"
hoelzl@56993
   108
        unfolding A_def by auto
hoelzl@56993
   109
      then have "\<And>i. F i x = z"
hoelzl@56993
   110
        by (auto simp: F_def)
hoelzl@56993
   111
      then show ?thesis
hoelzl@56993
   112
        using `f x = z` by auto
hoelzl@56993
   113
    next
hoelzl@56993
   114
      assume "f x \<noteq> z"
hoelzl@56993
   115
hoelzl@56993
   116
      show ?thesis
hoelzl@56993
   117
      proof (rule tendstoI)
hoelzl@56993
   118
        fix e :: real assume "0 < e"
hoelzl@56993
   119
        with `f x \<noteq> z` obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z"
hoelzl@56993
   120
          by (metis dist_nz order_less_trans neq_iff nat_approx_posE)
hoelzl@56993
   121
        with `x\<in>space M` `f x \<noteq> z` have "x \<in> (\<Union>i. B n i)"
hoelzl@56993
   122
          unfolding A_def B_def UN_disjointed_eq using e by auto
hoelzl@56993
   123
        then obtain i where i: "x \<in> B n i" by auto
hoelzl@56993
   124
hoelzl@56993
   125
        show "eventually (\<lambda>i. dist (F i x) (f x) < e) sequentially"
hoelzl@56993
   126
          using eventually_ge_at_top[of "max n i"]
hoelzl@56993
   127
        proof eventually_elim
hoelzl@56993
   128
          fix j assume j: "max n i \<le> j"
hoelzl@56993
   129
          with i have "dist (f x) (F j x) < 1 / Suc (m j x)"
hoelzl@56993
   130
            by (intro *[OF _ _ i]) auto
hoelzl@56993
   131
          also have "\<dots> \<le> 1 / Suc n"
hoelzl@56993
   132
            using j m_upper[OF _ _ i]
hoelzl@56993
   133
            by (auto simp: field_simps)
hoelzl@56993
   134
          also note `1 / Suc n < e`
hoelzl@56993
   135
          finally show "dist (F j x) (f x) < e"
hoelzl@56993
   136
            by (simp add: less_imp_le dist_commute)
hoelzl@56993
   137
        qed
hoelzl@56993
   138
      qed
hoelzl@56993
   139
    qed
hoelzl@56993
   140
    fix i 
hoelzl@56993
   141
    { fix n m assume "x \<in> A n m"
hoelzl@56993
   142
      then have "dist (e m) (f x) + dist (f x) z \<le> 2 * dist (f x) z"
hoelzl@56993
   143
        unfolding A_def by (auto simp: dist_commute)
hoelzl@56993
   144
      also have "dist (e m) z \<le> dist (e m) (f x) + dist (f x) z"
hoelzl@56993
   145
        by (rule dist_triangle)
hoelzl@56993
   146
      finally (xtrans) have "dist (e m) z \<le> 2 * dist (f x) z" . }
hoelzl@56993
   147
    then show "dist (F i x) z \<le> 2 * dist (f x) z"
hoelzl@56993
   148
      unfolding F_def
hoelzl@56993
   149
      apply auto
hoelzl@56993
   150
      apply (rule LeastI2)
hoelzl@56993
   151
      apply auto
hoelzl@56993
   152
      done
hoelzl@56993
   153
  qed
hoelzl@56993
   154
qed
hoelzl@56993
   155
hoelzl@56993
   156
lemma real_indicator: "real (indicator A x :: ereal) = indicator A x"
hoelzl@56993
   157
  unfolding indicator_def by auto
hoelzl@56993
   158
hoelzl@56993
   159
lemma split_indicator_asm:
hoelzl@56993
   160
  "P (indicator S x) \<longleftrightarrow> \<not> ((x \<in> S \<and> \<not> P 1) \<or> (x \<notin> S \<and> \<not> P 0))"
hoelzl@56993
   161
  unfolding indicator_def by auto
hoelzl@56993
   162
hoelzl@56993
   163
lemma
hoelzl@56993
   164
  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
hoelzl@56993
   165
  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
hoelzl@56993
   166
  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
hoelzl@56993
   167
  unfolding indicator_def
hoelzl@56993
   168
  using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)
hoelzl@56993
   169
hoelzl@56993
   170
lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
hoelzl@56993
   171
  fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool"
hoelzl@56993
   172
  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
hoelzl@56993
   173
  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
hoelzl@56993
   174
  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
hoelzl@56993
   175
  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
hoelzl@56993
   176
  assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. U i x) ----> u x) \<Longrightarrow> P u"
hoelzl@56993
   177
  shows "P u"
hoelzl@56993
   178
proof -
hoelzl@56993
   179
  have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M" using u by auto
hoelzl@56993
   180
  from borel_measurable_implies_simple_function_sequence'[OF this]
hoelzl@56993
   181
  obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
hoelzl@56993
   182
    sup: "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
hoelzl@56993
   183
    by blast
hoelzl@56993
   184
hoelzl@56993
   185
  def U' \<equiv> "\<lambda>i x. indicator (space M) x * real (U i x)"
hoelzl@56993
   186
  then have U'_sf[measurable]: "\<And>i. simple_function M (U' i)"
hoelzl@56993
   187
    using U by (auto intro!: simple_function_compose1[where g=real])
hoelzl@56993
   188
hoelzl@56993
   189
  show "P u"
hoelzl@56993
   190
  proof (rule seq)
hoelzl@56993
   191
    fix i show "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x"
hoelzl@56993
   192
      using U nn by (auto
hoelzl@56993
   193
          intro: borel_measurable_simple_function 
hoelzl@56993
   194
          intro!: borel_measurable_real_of_ereal real_of_ereal_pos borel_measurable_times
hoelzl@56993
   195
          simp: U'_def zero_le_mult_iff)
hoelzl@56993
   196
    show "incseq U'"
hoelzl@56993
   197
      using U(2,3) nn
hoelzl@56993
   198
      by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def
hoelzl@56993
   199
               intro!: real_of_ereal_positive_mono)
hoelzl@56993
   200
  next
hoelzl@56993
   201
    fix x assume x: "x \<in> space M"
hoelzl@56993
   202
    have "(\<lambda>i. U i x) ----> (SUP i. U i x)"
hoelzl@56993
   203
      using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
hoelzl@56993
   204
    moreover have "(\<lambda>i. U i x) = (\<lambda>i. ereal (U' i x))"
hoelzl@56993
   205
      using x nn U(3) by (auto simp: fun_eq_iff U'_def ereal_real image_iff eq_commute)
hoelzl@56993
   206
    moreover have "(SUP i. U i x) = ereal (u x)"
hoelzl@56993
   207
      using sup u(2) by (simp add: max_def)
hoelzl@56993
   208
    ultimately show "(\<lambda>i. U' i x) ----> u x" 
hoelzl@56993
   209
      by simp
hoelzl@56993
   210
  next
hoelzl@56993
   211
    fix i
hoelzl@56993
   212
    have "U' i ` space M \<subseteq> real ` (U i ` space M)" "finite (U i ` space M)"
hoelzl@56993
   213
      unfolding U'_def using U(1) by (auto dest: simple_functionD)
hoelzl@56993
   214
    then have fin: "finite (U' i ` space M)"
hoelzl@56993
   215
      by (metis finite_subset finite_imageI)
hoelzl@56993
   216
    moreover have "\<And>z. {y. U' i z = y \<and> y \<in> U' i ` space M \<and> z \<in> space M} = (if z \<in> space M then {U' i z} else {})"
hoelzl@56993
   217
      by auto
hoelzl@56993
   218
    ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
hoelzl@56993
   219
      by (simp add: U'_def fun_eq_iff)
hoelzl@56993
   220
    have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
hoelzl@56993
   221
      using nn by (auto simp: U'_def real_of_ereal_pos)
hoelzl@56993
   222
    with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
hoelzl@56993
   223
    proof induct
hoelzl@56993
   224
      case empty from set[of "{}"] show ?case
hoelzl@56993
   225
        by (simp add: indicator_def[abs_def])
hoelzl@56993
   226
    next
hoelzl@56993
   227
      case (insert x F)
hoelzl@56993
   228
      then show ?case
hoelzl@56993
   229
        by (auto intro!: add mult set setsum_nonneg split: split_indicator split_indicator_asm
hoelzl@56993
   230
                 simp del: setsum_mult_indicator simp: setsum_nonneg_eq_0_iff )
hoelzl@56993
   231
    qed
hoelzl@56993
   232
    with U' show "P (U' i)" by simp
hoelzl@56993
   233
  qed
hoelzl@56993
   234
qed
hoelzl@56993
   235
hoelzl@56993
   236
lemma scaleR_cong_right:
hoelzl@56993
   237
  fixes x :: "'a :: real_vector"
hoelzl@56993
   238
  shows "(x \<noteq> 0 \<Longrightarrow> r = p) \<Longrightarrow> r *\<^sub>R x = p *\<^sub>R x"
hoelzl@56993
   239
  by (cases "x = 0") auto
hoelzl@56993
   240
hoelzl@56993
   241
inductive simple_bochner_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" for M f where
hoelzl@56993
   242
  "simple_function M f \<Longrightarrow> emeasure M {y\<in>space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
hoelzl@56993
   243
    simple_bochner_integrable M f"
hoelzl@56993
   244
hoelzl@56993
   245
lemma simple_bochner_integrable_compose2:
hoelzl@56993
   246
  assumes p_0: "p 0 0 = 0"
hoelzl@56993
   247
  shows "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integrable M g \<Longrightarrow>
hoelzl@56993
   248
    simple_bochner_integrable M (\<lambda>x. p (f x) (g x))"
hoelzl@56993
   249
proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI)
hoelzl@56993
   250
  assume sf: "simple_function M f" "simple_function M g"
hoelzl@56993
   251
  then show "simple_function M (\<lambda>x. p (f x) (g x))"
hoelzl@56993
   252
    by (rule simple_function_compose2)
hoelzl@56993
   253
hoelzl@56993
   254
  from sf have [measurable]:
hoelzl@56993
   255
      "f \<in> measurable M (count_space UNIV)"
hoelzl@56993
   256
      "g \<in> measurable M (count_space UNIV)"
hoelzl@56993
   257
    by (auto intro: measurable_simple_function)
hoelzl@56993
   258
hoelzl@56993
   259
  assume fin: "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" "emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity>"
hoelzl@56993
   260
   
hoelzl@56993
   261
  have "emeasure M {x\<in>space M. p (f x) (g x) \<noteq> 0} \<le>
hoelzl@56993
   262
      emeasure M ({x\<in>space M. f x \<noteq> 0} \<union> {x\<in>space M. g x \<noteq> 0})"
hoelzl@56993
   263
    by (intro emeasure_mono) (auto simp: p_0)
hoelzl@56993
   264
  also have "\<dots> \<le> emeasure M {x\<in>space M. f x \<noteq> 0} + emeasure M {x\<in>space M. g x \<noteq> 0}"
hoelzl@56993
   265
    by (intro emeasure_subadditive) auto
hoelzl@56993
   266
  finally show "emeasure M {y \<in> space M. p (f y) (g y) \<noteq> 0} \<noteq> \<infinity>"
hoelzl@56993
   267
    using fin by auto
hoelzl@56993
   268
qed
hoelzl@56993
   269
hoelzl@56993
   270
lemma simple_function_finite_support:
hoelzl@56993
   271
  assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and nn: "\<And>x. 0 \<le> f x"
hoelzl@56993
   272
  shows "emeasure M {x\<in>space M. f x \<noteq> 0} \<noteq> \<infinity>"
hoelzl@56993
   273
proof cases
hoelzl@56993
   274
  from f have meas[measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   275
    by (rule borel_measurable_simple_function)
hoelzl@56993
   276
hoelzl@56993
   277
  assume non_empty: "\<exists>x\<in>space M. f x \<noteq> 0"
hoelzl@56993
   278
hoelzl@56993
   279
  def m \<equiv> "Min (f`space M - {0})"
hoelzl@56993
   280
  have "m \<in> f`space M - {0}"
hoelzl@56993
   281
    unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def)
hoelzl@56993
   282
  then have m: "0 < m"
hoelzl@56993
   283
    using nn by (auto simp: less_le)
hoelzl@56993
   284
hoelzl@56993
   285
  from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} = 
hoelzl@56993
   286
    (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
hoelzl@56996
   287
    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
hoelzl@56993
   288
  also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
hoelzl@56993
   289
    using AE_space
hoelzl@56996
   290
  proof (intro nn_integral_mono_AE, eventually_elim)
hoelzl@56993
   291
    fix x assume "x \<in> space M"
hoelzl@56993
   292
    with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
hoelzl@56993
   293
      using f by (auto split: split_indicator simp: simple_function_def m_def)
hoelzl@56993
   294
  qed
hoelzl@56993
   295
  also note `\<dots> < \<infinity>`
hoelzl@56993
   296
  finally show ?thesis
hoelzl@56993
   297
    using m by auto 
hoelzl@56993
   298
next
hoelzl@56993
   299
  assume "\<not> (\<exists>x\<in>space M. f x \<noteq> 0)"
hoelzl@56993
   300
  with nn have *: "{x\<in>space M. f x \<noteq> 0} = {}"
hoelzl@56993
   301
    by auto
hoelzl@56993
   302
  show ?thesis unfolding * by simp
hoelzl@56993
   303
qed
hoelzl@56993
   304
hoelzl@56993
   305
lemma simple_bochner_integrableI_bounded:
hoelzl@56993
   306
  assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
hoelzl@56993
   307
  shows "simple_bochner_integrable M f"
hoelzl@56993
   308
proof
hoelzl@56993
   309
  have "emeasure M {y \<in> space M. ereal (norm (f y)) \<noteq> 0} \<noteq> \<infinity>"
hoelzl@56993
   310
  proof (rule simple_function_finite_support)
hoelzl@56993
   311
    show "simple_function M (\<lambda>x. ereal (norm (f x)))"
hoelzl@56993
   312
      using f by (rule simple_function_compose1)
hoelzl@56993
   313
    show "(\<integral>\<^sup>+ y. ereal (norm (f y)) \<partial>M) < \<infinity>" by fact
hoelzl@56993
   314
  qed simp
hoelzl@56993
   315
  then show "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp
hoelzl@56993
   316
qed fact
hoelzl@56993
   317
hoelzl@56993
   318
definition simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
hoelzl@56993
   319
  "simple_bochner_integral M f = (\<Sum>y\<in>f`space M. measure M {x\<in>space M. f x = y} *\<^sub>R y)"
hoelzl@56993
   320
hoelzl@56993
   321
lemma simple_bochner_integral_partition:
hoelzl@56993
   322
  assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
hoelzl@56993
   323
  assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"
hoelzl@56993
   324
  assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"
hoelzl@56993
   325
  shows "simple_bochner_integral M f = (\<Sum>y\<in>g ` space M. measure M {x\<in>space M. g x = y} *\<^sub>R v y)"
hoelzl@56993
   326
    (is "_ = ?r")
hoelzl@56993
   327
proof -
hoelzl@56993
   328
  from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
hoelzl@56993
   329
    by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)
hoelzl@56993
   330
hoelzl@56993
   331
  from f have [measurable]: "f \<in> measurable M (count_space UNIV)"
hoelzl@56993
   332
    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   333
hoelzl@56993
   334
  from g have [measurable]: "g \<in> measurable M (count_space UNIV)"
hoelzl@56993
   335
    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   336
hoelzl@56993
   337
  { fix y assume "y \<in> space M"
hoelzl@56993
   338
    then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}"
hoelzl@56993
   339
      by (auto cong: sub simp: v[symmetric]) }
hoelzl@56993
   340
  note eq = this
hoelzl@56993
   341
hoelzl@56993
   342
  have "simple_bochner_integral M f =
hoelzl@56993
   343
    (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
hoelzl@56993
   344
      if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} else 0) *\<^sub>R y)"
hoelzl@56993
   345
    unfolding simple_bochner_integral_def
hoelzl@56993
   346
  proof (safe intro!: setsum_cong scaleR_cong_right)
hoelzl@56993
   347
    fix y assume y: "y \<in> space M" "f y \<noteq> 0"
hoelzl@56993
   348
    have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
hoelzl@56993
   349
        {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
hoelzl@56993
   350
      by auto
hoelzl@56993
   351
    have eq:"{x \<in> space M. f x = f y} =
hoelzl@56993
   352
        (\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i})"
hoelzl@56993
   353
      by (auto simp: eq_commute cong: sub rev_conj_cong)
hoelzl@56993
   354
    have "finite (g`space M)" by simp
hoelzl@56993
   355
    then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
hoelzl@56993
   356
      by (rule rev_finite_subset) auto
hoelzl@56993
   357
    moreover
hoelzl@56993
   358
    { fix x assume "x \<in> space M" "f x = f y"
hoelzl@56993
   359
      then have "x \<in> space M" "f x \<noteq> 0"
hoelzl@56993
   360
        using y by auto
hoelzl@56993
   361
      then have "emeasure M {y \<in> space M. g y = g x} \<le> emeasure M {y \<in> space M. f y \<noteq> 0}"
hoelzl@56993
   362
        by (auto intro!: emeasure_mono cong: sub)
hoelzl@56993
   363
      then have "emeasure M {xa \<in> space M. g xa = g x} < \<infinity>"
hoelzl@56993
   364
        using f by (auto simp: simple_bochner_integrable.simps) }
hoelzl@56993
   365
    ultimately
hoelzl@56993
   366
    show "measure M {x \<in> space M. f x = f y} =
hoelzl@56993
   367
      (\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then measure M {x \<in> space M. g x = z} else 0)"
hoelzl@56993
   368
      apply (simp add: setsum_cases eq)
hoelzl@56993
   369
      apply (subst measure_finite_Union[symmetric])
hoelzl@56993
   370
      apply (auto simp: disjoint_family_on_def)
hoelzl@56993
   371
      done
hoelzl@56993
   372
  qed
hoelzl@56993
   373
  also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
hoelzl@56993
   374
      if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} *\<^sub>R y else 0))"
hoelzl@56993
   375
    by (auto intro!: setsum_cong simp: scaleR_setsum_left)
hoelzl@56993
   376
  also have "\<dots> = ?r"
hoelzl@56993
   377
    by (subst setsum_commute)
hoelzl@56993
   378
       (auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq)
hoelzl@56993
   379
  finally show "simple_bochner_integral M f = ?r" .
hoelzl@56993
   380
qed
hoelzl@56993
   381
hoelzl@56993
   382
lemma simple_bochner_integral_add:
hoelzl@56993
   383
  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
hoelzl@56993
   384
  shows "simple_bochner_integral M (\<lambda>x. f x + g x) =
hoelzl@56993
   385
    simple_bochner_integral M f + simple_bochner_integral M g"
hoelzl@56993
   386
proof -
hoelzl@56993
   387
  from f g have "simple_bochner_integral M (\<lambda>x. f x + g x) =
hoelzl@56993
   388
    (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R (fst y + snd y))"
hoelzl@56993
   389
    by (intro simple_bochner_integral_partition)
hoelzl@56993
   390
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
hoelzl@56993
   391
  moreover from f g have "simple_bochner_integral M f =
hoelzl@56993
   392
    (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R fst y)"
hoelzl@56993
   393
    by (intro simple_bochner_integral_partition)
hoelzl@56993
   394
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
hoelzl@56993
   395
  moreover from f g have "simple_bochner_integral M g =
hoelzl@56993
   396
    (\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R snd y)"
hoelzl@56993
   397
    by (intro simple_bochner_integral_partition)
hoelzl@56993
   398
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
hoelzl@56993
   399
  ultimately show ?thesis
hoelzl@56993
   400
    by (simp add: setsum_addf[symmetric] scaleR_add_right)
hoelzl@56993
   401
qed
hoelzl@56993
   402
hoelzl@56993
   403
lemma (in linear) simple_bochner_integral_linear:
hoelzl@56993
   404
  assumes g: "simple_bochner_integrable M g"
hoelzl@56993
   405
  shows "simple_bochner_integral M (\<lambda>x. f (g x)) = f (simple_bochner_integral M g)"
hoelzl@56993
   406
proof -
hoelzl@56993
   407
  from g have "simple_bochner_integral M (\<lambda>x. f (g x)) =
hoelzl@56993
   408
    (\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)"
hoelzl@56993
   409
    by (intro simple_bochner_integral_partition)
hoelzl@56993
   410
       (auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"] zero
hoelzl@56993
   411
             elim: simple_bochner_integrable.cases)
hoelzl@56993
   412
  also have "\<dots> = f (simple_bochner_integral M g)"
hoelzl@56993
   413
    by (simp add: simple_bochner_integral_def setsum scaleR)
hoelzl@56993
   414
  finally show ?thesis .
hoelzl@56993
   415
qed
hoelzl@56993
   416
hoelzl@56993
   417
lemma simple_bochner_integral_minus:
hoelzl@56993
   418
  assumes f: "simple_bochner_integrable M f"
hoelzl@56993
   419
  shows "simple_bochner_integral M (\<lambda>x. - f x) = - simple_bochner_integral M f"
hoelzl@56993
   420
proof -
hoelzl@56993
   421
  interpret linear uminus by unfold_locales auto
hoelzl@56993
   422
  from f show ?thesis
hoelzl@56993
   423
    by (rule simple_bochner_integral_linear)
hoelzl@56993
   424
qed
hoelzl@56993
   425
hoelzl@56993
   426
lemma simple_bochner_integral_diff:
hoelzl@56993
   427
  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
hoelzl@56993
   428
  shows "simple_bochner_integral M (\<lambda>x. f x - g x) =
hoelzl@56993
   429
    simple_bochner_integral M f - simple_bochner_integral M g"
hoelzl@56993
   430
  unfolding diff_conv_add_uminus using f g
hoelzl@56993
   431
  by (subst simple_bochner_integral_add)
hoelzl@56993
   432
     (auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="\<lambda>x y. - y"])
hoelzl@56993
   433
hoelzl@56993
   434
lemma simple_bochner_integral_norm_bound:
hoelzl@56993
   435
  assumes f: "simple_bochner_integrable M f"
hoelzl@56993
   436
  shows "norm (simple_bochner_integral M f) \<le> simple_bochner_integral M (\<lambda>x. norm (f x))"
hoelzl@56993
   437
proof -
hoelzl@56993
   438
  have "norm (simple_bochner_integral M f) \<le> 
hoelzl@56993
   439
    (\<Sum>y\<in>f ` space M. norm (measure M {x \<in> space M. f x = y} *\<^sub>R y))"
hoelzl@56993
   440
    unfolding simple_bochner_integral_def by (rule norm_setsum)
hoelzl@56993
   441
  also have "\<dots> = (\<Sum>y\<in>f ` space M. measure M {x \<in> space M. f x = y} *\<^sub>R norm y)"
hoelzl@56993
   442
    by (simp add: measure_nonneg)
hoelzl@56993
   443
  also have "\<dots> = simple_bochner_integral M (\<lambda>x. norm (f x))"
hoelzl@56993
   444
    using f
hoelzl@56993
   445
    by (intro simple_bochner_integral_partition[symmetric])
hoelzl@56993
   446
       (auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
hoelzl@56993
   447
  finally show ?thesis .
hoelzl@56993
   448
qed
hoelzl@56993
   449
hoelzl@56996
   450
lemma simple_bochner_integral_eq_nn_integral:
hoelzl@56993
   451
  assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
hoelzl@56993
   452
  shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
hoelzl@56993
   453
proof -
hoelzl@56993
   454
  { fix x y z have "(x \<noteq> 0 \<Longrightarrow> y = z) \<Longrightarrow> ereal x * y = ereal x * z"
hoelzl@56993
   455
      by (cases "x = 0") (auto simp: zero_ereal_def[symmetric]) }
hoelzl@56993
   456
  note ereal_cong_mult = this
hoelzl@56993
   457
hoelzl@56993
   458
  have [measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   459
    using f(1) by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   460
hoelzl@56993
   461
  { fix y assume y: "y \<in> space M" "f y \<noteq> 0"
hoelzl@56993
   462
    have "ereal (measure M {x \<in> space M. f x = f y}) = emeasure M {x \<in> space M. f x = f y}"
hoelzl@56993
   463
    proof (rule emeasure_eq_ereal_measure[symmetric])
hoelzl@56993
   464
      have "emeasure M {x \<in> space M. f x = f y} \<le> emeasure M {x \<in> space M. f x \<noteq> 0}"
hoelzl@56993
   465
        using y by (intro emeasure_mono) auto
hoelzl@56993
   466
      with f show "emeasure M {x \<in> space M. f x = f y} \<noteq> \<infinity>"
hoelzl@56993
   467
        by (auto simp: simple_bochner_integrable.simps)
hoelzl@56993
   468
    qed
hoelzl@56993
   469
    moreover have "{x \<in> space M. f x = f y} = (\<lambda>x. ereal (f x)) -` {ereal (f y)} \<inter> space M"
hoelzl@56993
   470
      by auto
hoelzl@56993
   471
    ultimately have "ereal (measure M {x \<in> space M. f x = f y}) =
hoelzl@56993
   472
          emeasure M ((\<lambda>x. ereal (f x)) -` {ereal (f y)} \<inter> space M)" by simp }
hoelzl@56993
   473
  with f have "simple_bochner_integral M f = (\<integral>\<^sup>Sx. f x \<partial>M)"
hoelzl@56993
   474
    unfolding simple_integral_def
hoelzl@56993
   475
    by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real])
hoelzl@56993
   476
       (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
hoelzl@56993
   477
             intro!: setsum_cong ereal_cong_mult
hoelzl@56993
   478
             simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac
hoelzl@56993
   479
             simp del: setsum_ereal times_ereal.simps(1))
hoelzl@56993
   480
  also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
hoelzl@56993
   481
    using f
hoelzl@56996
   482
    by (intro nn_integral_eq_simple_integral[symmetric])
hoelzl@56993
   483
       (auto simp: simple_function_compose1 simple_bochner_integrable.simps)
hoelzl@56993
   484
  finally show ?thesis .
hoelzl@56993
   485
qed
hoelzl@56993
   486
hoelzl@56993
   487
lemma simple_bochner_integral_bounded:
hoelzl@56993
   488
  fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}"
hoelzl@56993
   489
  assumes f[measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   490
  assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
hoelzl@56993
   491
  shows "ereal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \<le>
hoelzl@56993
   492
    (\<integral>\<^sup>+ x. norm (f x - s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x - t x) \<partial>M)"
hoelzl@56993
   493
    (is "ereal (norm (?s - ?t)) \<le> ?S + ?T")
hoelzl@56993
   494
proof -
hoelzl@56993
   495
  have [measurable]: "s \<in> borel_measurable M" "t \<in> borel_measurable M"
hoelzl@56993
   496
    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   497
hoelzl@56993
   498
  have "ereal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))"
hoelzl@56993
   499
    using s t by (subst simple_bochner_integral_diff) auto
hoelzl@56993
   500
  also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))"
hoelzl@56993
   501
    using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
hoelzl@56993
   502
    by (auto intro!: simple_bochner_integral_norm_bound)
hoelzl@56993
   503
  also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
hoelzl@56993
   504
    using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
hoelzl@56996
   505
    by (auto intro!: simple_bochner_integral_eq_nn_integral)
hoelzl@56993
   506
  also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s x)) + ereal (norm (f x - t x)) \<partial>M)"
hoelzl@56996
   507
    by (auto intro!: nn_integral_mono)
hoelzl@56993
   508
       (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
hoelzl@56993
   509
              norm_minus_commute norm_triangle_ineq4 order_refl)
hoelzl@56993
   510
  also have "\<dots> = ?S + ?T"
hoelzl@56996
   511
   by (rule nn_integral_add) auto
hoelzl@56993
   512
  finally show ?thesis .
hoelzl@56993
   513
qed
hoelzl@56993
   514
hoelzl@56993
   515
inductive has_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::{real_normed_vector, second_countable_topology} \<Rightarrow> bool"
hoelzl@56993
   516
  for M f x where
hoelzl@56993
   517
  "f \<in> borel_measurable M \<Longrightarrow>
hoelzl@56993
   518
    (\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow>
hoelzl@56993
   519
    (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0 \<Longrightarrow>
hoelzl@56993
   520
    (\<lambda>i. simple_bochner_integral M (s i)) ----> x \<Longrightarrow>
hoelzl@56993
   521
    has_bochner_integral M f x"
hoelzl@56993
   522
hoelzl@56993
   523
lemma has_bochner_integral_cong:
hoelzl@56993
   524
  assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
hoelzl@56993
   525
  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
hoelzl@56993
   526
  unfolding has_bochner_integral.simps assms(1,3)
hoelzl@56996
   527
  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
hoelzl@56993
   528
hoelzl@56993
   529
lemma has_bochner_integral_cong_AE:
hoelzl@56993
   530
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
hoelzl@56993
   531
    has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
hoelzl@56993
   532
  unfolding has_bochner_integral.simps
hoelzl@56993
   533
  by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
hoelzl@56996
   534
            nn_integral_cong_AE)
hoelzl@56993
   535
     auto
hoelzl@56993
   536
hoelzl@56993
   537
lemma borel_measurable_has_bochner_integral[measurable_dest]:
hoelzl@56993
   538
  "has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M"
hoelzl@56993
   539
  by (auto elim: has_bochner_integral.cases)
hoelzl@56993
   540
hoelzl@56993
   541
lemma has_bochner_integral_simple_bochner_integrable:
hoelzl@56993
   542
  "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
hoelzl@56993
   543
  by (rule has_bochner_integral.intros[where s="\<lambda>_. f"])
hoelzl@56993
   544
     (auto intro: borel_measurable_simple_function 
hoelzl@56993
   545
           elim: simple_bochner_integrable.cases
hoelzl@56993
   546
           simp: zero_ereal_def[symmetric])
hoelzl@56993
   547
hoelzl@56993
   548
lemma has_bochner_integral_real_indicator:
hoelzl@56993
   549
  assumes [measurable]: "A \<in> sets M" and A: "emeasure M A < \<infinity>"
hoelzl@56993
   550
  shows "has_bochner_integral M (indicator A) (measure M A)"
hoelzl@56993
   551
proof -
hoelzl@56993
   552
  have sbi: "simple_bochner_integrable M (indicator A::'a \<Rightarrow> real)"
hoelzl@56993
   553
  proof
hoelzl@56993
   554
    have "{y \<in> space M. (indicator A y::real) \<noteq> 0} = A"
hoelzl@56993
   555
      using sets.sets_into_space[OF `A\<in>sets M`] by (auto split: split_indicator)
hoelzl@56993
   556
    then show "emeasure M {y \<in> space M. (indicator A y::real) \<noteq> 0} \<noteq> \<infinity>"
hoelzl@56993
   557
      using A by auto
hoelzl@56993
   558
  qed (rule simple_function_indicator assms)+
hoelzl@56993
   559
  moreover have "simple_bochner_integral M (indicator A) = measure M A"
hoelzl@56996
   560
    using simple_bochner_integral_eq_nn_integral[OF sbi] A
hoelzl@56993
   561
    by (simp add: ereal_indicator emeasure_eq_ereal_measure)
hoelzl@56993
   562
  ultimately show ?thesis
hoelzl@56993
   563
    by (metis has_bochner_integral_simple_bochner_integrable)
hoelzl@56993
   564
qed
hoelzl@56993
   565
hoelzl@57036
   566
lemma has_bochner_integral_add[intro]:
hoelzl@56993
   567
  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
hoelzl@56993
   568
    has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
hoelzl@56993
   569
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
hoelzl@56993
   570
  fix sf sg
hoelzl@56993
   571
  assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - sf i x) \<partial>M) ----> 0"
hoelzl@56993
   572
  assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x - sg i x) \<partial>M) ----> 0"
hoelzl@56993
   573
hoelzl@56993
   574
  assume sf: "\<forall>i. simple_bochner_integrable M (sf i)"
hoelzl@56993
   575
    and sg: "\<forall>i. simple_bochner_integrable M (sg i)"
hoelzl@56993
   576
  then have [measurable]: "\<And>i. sf i \<in> borel_measurable M" "\<And>i. sg i \<in> borel_measurable M"
hoelzl@56993
   577
    by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   578
  assume [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@56993
   579
hoelzl@56993
   580
  show "\<And>i. simple_bochner_integrable M (\<lambda>x. sf i x + sg i x)"
hoelzl@56993
   581
    using sf sg by (simp add: simple_bochner_integrable_compose2)
hoelzl@56993
   582
hoelzl@56993
   583
  show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \<partial>M) ----> 0"
hoelzl@56993
   584
    (is "?f ----> 0")
hoelzl@56993
   585
  proof (rule tendsto_sandwich)
hoelzl@56993
   586
    show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
hoelzl@56996
   587
      by (auto simp: nn_integral_nonneg)
hoelzl@56993
   588
    show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x - sg i x)) \<partial>M) sequentially"
hoelzl@56993
   589
      (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
hoelzl@56993
   590
    proof (intro always_eventually allI)
hoelzl@56993
   591
      fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ereal (norm (g x - sg i x)) \<partial>M)"
hoelzl@56996
   592
        by (auto intro!: nn_integral_mono norm_diff_triangle_ineq)
hoelzl@56993
   593
      also have "\<dots> = ?g i"
hoelzl@56996
   594
        by (intro nn_integral_add) auto
hoelzl@56993
   595
      finally show "?f i \<le> ?g i" .
hoelzl@56993
   596
    qed
hoelzl@56993
   597
    show "?g ----> 0"
hoelzl@56993
   598
      using tendsto_add_ereal[OF _ _ f_sf g_sg] by simp
hoelzl@56993
   599
  qed
hoelzl@56993
   600
qed (auto simp: simple_bochner_integral_add tendsto_add)
hoelzl@56993
   601
hoelzl@56993
   602
lemma has_bochner_integral_bounded_linear:
hoelzl@56993
   603
  assumes "bounded_linear T"
hoelzl@56993
   604
  shows "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M (\<lambda>x. T (f x)) (T x)"
hoelzl@56993
   605
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
hoelzl@56993
   606
  interpret T: bounded_linear T by fact
hoelzl@56993
   607
  have [measurable]: "T \<in> borel_measurable borel"
hoelzl@56993
   608
    by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
hoelzl@56993
   609
  assume [measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   610
  then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
hoelzl@56993
   611
    by auto
hoelzl@56993
   612
hoelzl@56993
   613
  fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0"
hoelzl@56993
   614
  assume s: "\<forall>i. simple_bochner_integrable M (s i)"
hoelzl@56993
   615
  then show "\<And>i. simple_bochner_integrable M (\<lambda>x. T (s i x))"
hoelzl@56993
   616
    by (auto intro: simple_bochner_integrable_compose2 T.zero)
hoelzl@56993
   617
hoelzl@56993
   618
  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
hoelzl@56993
   619
    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   620
hoelzl@56993
   621
  obtain K where K: "K > 0" "\<And>x i. norm (T (f x) - T (s i x)) \<le> norm (f x - s i x) * K"
hoelzl@56993
   622
    using T.pos_bounded by (auto simp: T.diff[symmetric])
hoelzl@56993
   623
hoelzl@56993
   624
  show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x) - T (s i x)) \<partial>M) ----> 0"
hoelzl@56993
   625
    (is "?f ----> 0")
hoelzl@56993
   626
  proof (rule tendsto_sandwich)
hoelzl@56993
   627
    show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
hoelzl@56996
   628
      by (auto simp: nn_integral_nonneg)
hoelzl@56993
   629
hoelzl@56993
   630
    show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
hoelzl@56993
   631
      (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
hoelzl@56993
   632
    proof (intro always_eventually allI)
hoelzl@56993
   633
      fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
hoelzl@56996
   634
        using K by (intro nn_integral_mono) (auto simp: mult_ac)
hoelzl@56993
   635
      also have "\<dots> = ?g i"
hoelzl@56996
   636
        using K by (intro nn_integral_cmult) auto
hoelzl@56993
   637
      finally show "?f i \<le> ?g i" .
hoelzl@56993
   638
    qed
hoelzl@56993
   639
    show "?g ----> 0"
hoelzl@56993
   640
      using ereal_lim_mult[OF f_s, of "ereal K"] by simp
hoelzl@56993
   641
  qed
hoelzl@56993
   642
hoelzl@56993
   643
  assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
hoelzl@56993
   644
  with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) ----> T x"
hoelzl@56993
   645
    by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear)
hoelzl@56993
   646
qed
hoelzl@56993
   647
hoelzl@56993
   648
lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0"
hoelzl@56993
   649
  by (auto intro!: has_bochner_integral.intros[where s="\<lambda>_ _. 0"]
hoelzl@56993
   650
           simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps
hoelzl@56993
   651
                 simple_bochner_integral_def image_constant_conv)
hoelzl@56993
   652
hoelzl@56993
   653
lemma has_bochner_integral_scaleR_left[intro]:
hoelzl@56993
   654
  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x *\<^sub>R c) (x *\<^sub>R c)"
hoelzl@56993
   655
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])
hoelzl@56993
   656
hoelzl@56993
   657
lemma has_bochner_integral_scaleR_right[intro]:
hoelzl@56993
   658
  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c *\<^sub>R f x) (c *\<^sub>R x)"
hoelzl@56993
   659
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])
hoelzl@56993
   660
hoelzl@56993
   661
lemma has_bochner_integral_mult_left[intro]:
hoelzl@56993
   662
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
   663
  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x * c) (x * c)"
hoelzl@56993
   664
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])
hoelzl@56993
   665
hoelzl@56993
   666
lemma has_bochner_integral_mult_right[intro]:
hoelzl@56993
   667
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
   668
  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c * f x) (c * x)"
hoelzl@56993
   669
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])
hoelzl@56993
   670
hoelzl@56993
   671
lemmas has_bochner_integral_divide = 
hoelzl@56993
   672
  has_bochner_integral_bounded_linear[OF bounded_linear_divide]
hoelzl@56993
   673
hoelzl@56993
   674
lemma has_bochner_integral_divide_zero[intro]:
hoelzl@56993
   675
  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
hoelzl@56993
   676
  shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
hoelzl@56993
   677
  using has_bochner_integral_divide by (cases "c = 0") auto
hoelzl@56993
   678
hoelzl@56993
   679
lemma has_bochner_integral_inner_left[intro]:
hoelzl@56993
   680
  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)"
hoelzl@56993
   681
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])
hoelzl@56993
   682
hoelzl@56993
   683
lemma has_bochner_integral_inner_right[intro]:
hoelzl@56993
   684
  "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c \<bullet> f x) (c \<bullet> x)"
hoelzl@56993
   685
  by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])
hoelzl@56993
   686
hoelzl@56993
   687
lemmas has_bochner_integral_minus =
hoelzl@56993
   688
  has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
hoelzl@56993
   689
lemmas has_bochner_integral_Re =
hoelzl@56993
   690
  has_bochner_integral_bounded_linear[OF bounded_linear_Re]
hoelzl@56993
   691
lemmas has_bochner_integral_Im =
hoelzl@56993
   692
  has_bochner_integral_bounded_linear[OF bounded_linear_Im]
hoelzl@56993
   693
lemmas has_bochner_integral_cnj =
hoelzl@56993
   694
  has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
hoelzl@56993
   695
lemmas has_bochner_integral_of_real =
hoelzl@56993
   696
  has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
hoelzl@56993
   697
lemmas has_bochner_integral_fst =
hoelzl@56993
   698
  has_bochner_integral_bounded_linear[OF bounded_linear_fst]
hoelzl@56993
   699
lemmas has_bochner_integral_snd =
hoelzl@56993
   700
  has_bochner_integral_bounded_linear[OF bounded_linear_snd]
hoelzl@56993
   701
hoelzl@56993
   702
lemma has_bochner_integral_indicator:
hoelzl@56993
   703
  "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
hoelzl@56993
   704
    has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)"
hoelzl@56993
   705
  by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)
hoelzl@56993
   706
hoelzl@56993
   707
lemma has_bochner_integral_diff:
hoelzl@56993
   708
  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
hoelzl@56993
   709
    has_bochner_integral M (\<lambda>x. f x - g x) (x - y)"
hoelzl@56993
   710
  unfolding diff_conv_add_uminus
hoelzl@56993
   711
  by (intro has_bochner_integral_add has_bochner_integral_minus)
hoelzl@56993
   712
hoelzl@56993
   713
lemma has_bochner_integral_setsum:
hoelzl@56993
   714
  "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
hoelzl@56993
   715
    has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
hoelzl@57036
   716
  by (induct I rule: infinite_finite_induct) auto
hoelzl@56993
   717
hoelzl@56993
   718
lemma has_bochner_integral_implies_finite_norm:
hoelzl@56993
   719
  "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
hoelzl@56993
   720
proof (elim has_bochner_integral.cases)
hoelzl@56993
   721
  fix s v
hoelzl@56993
   722
  assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and
hoelzl@56993
   723
    lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
hoelzl@56993
   724
  from order_tendstoD[OF lim_0, of "\<infinity>"]
hoelzl@56993
   725
  obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) < \<infinity>"
hoelzl@56993
   726
    by (metis (mono_tags, lifting) eventually_False_sequentially eventually_elim1
hoelzl@56993
   727
              less_ereal.simps(4) zero_ereal_def)
hoelzl@56993
   728
hoelzl@56993
   729
  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
hoelzl@56993
   730
    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   731
hoelzl@56993
   732
  def m \<equiv> "if space M = {} then 0 else Max ((\<lambda>x. norm (s i x))`space M)"
hoelzl@56993
   733
  have "finite (s i ` space M)"
hoelzl@56993
   734
    using s by (auto simp: simple_function_def simple_bochner_integrable.simps)
hoelzl@56993
   735
  then have "finite (norm ` s i ` space M)"
hoelzl@56993
   736
    by (rule finite_imageI)
hoelzl@56993
   737
  then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
hoelzl@56993
   738
    by (auto simp: m_def image_comp comp_def Max_ge_iff)
hoelzl@56993
   739
  then have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ereal m * indicator {x\<in>space M. s i x \<noteq> 0} x \<partial>M)"
hoelzl@56996
   740
    by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
hoelzl@56993
   741
  also have "\<dots> < \<infinity>"
hoelzl@56996
   742
    using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
hoelzl@56993
   743
  finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
hoelzl@56993
   744
hoelzl@56993
   745
  have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) + ereal (norm (s i x)) \<partial>M)"
hoelzl@56996
   746
    by (auto intro!: nn_integral_mono) (metis add_commute norm_triangle_sub)
hoelzl@56993
   747
  also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
hoelzl@56996
   748
    by (rule nn_integral_add) auto
hoelzl@56993
   749
  also have "\<dots> < \<infinity>"
hoelzl@56993
   750
    using s_fin f_s_fin by auto
hoelzl@56993
   751
  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
hoelzl@56993
   752
qed
hoelzl@56993
   753
hoelzl@56993
   754
lemma has_bochner_integral_norm_bound:
hoelzl@56993
   755
  assumes i: "has_bochner_integral M f x"
hoelzl@56993
   756
  shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
hoelzl@56993
   757
using assms proof
hoelzl@56993
   758
  fix s assume
hoelzl@56993
   759
    x: "(\<lambda>i. simple_bochner_integral M (s i)) ----> x" (is "?s ----> x") and
hoelzl@56993
   760
    s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and
hoelzl@56993
   761
    lim: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0" and
hoelzl@56993
   762
    f[measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   763
hoelzl@56993
   764
  have [measurable]: "\<And>i. s i \<in> borel_measurable M"
hoelzl@56993
   765
    using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function)
hoelzl@56993
   766
hoelzl@56993
   767
  show "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
hoelzl@56993
   768
  proof (rule LIMSEQ_le)
hoelzl@56993
   769
    show "(\<lambda>i. ereal (norm (?s i))) ----> norm x"
hoelzl@56993
   770
      using x by (intro tendsto_intros lim_ereal[THEN iffD2])
hoelzl@56993
   771
    show "\<exists>N. \<forall>n\<ge>N. norm (?s n) \<le> (\<integral>\<^sup>+x. norm (f x - s n x) \<partial>M) + (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
hoelzl@56993
   772
      (is "\<exists>N. \<forall>n\<ge>N. _ \<le> ?t n")
hoelzl@56993
   773
    proof (intro exI allI impI)
hoelzl@56993
   774
      fix n
hoelzl@56993
   775
      have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
hoelzl@56993
   776
        by (auto intro!: simple_bochner_integral_norm_bound)
hoelzl@56993
   777
      also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
hoelzl@56996
   778
        by (intro simple_bochner_integral_eq_nn_integral)
hoelzl@56993
   779
           (auto intro: s simple_bochner_integrable_compose2)
hoelzl@56993
   780
      also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s n x)) + norm (f x) \<partial>M)"
hoelzl@56996
   781
        by (auto intro!: nn_integral_mono)
hoelzl@56993
   782
           (metis add_commute norm_minus_commute norm_triangle_sub)
hoelzl@56993
   783
      also have "\<dots> = ?t n" 
hoelzl@56996
   784
        by (rule nn_integral_add) auto
hoelzl@56993
   785
      finally show "norm (?s n) \<le> ?t n" .
hoelzl@56993
   786
    qed
hoelzl@56993
   787
    have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
hoelzl@56993
   788
      using has_bochner_integral_implies_finite_norm[OF i]
hoelzl@56993
   789
      by (intro tendsto_add_ereal tendsto_const lim) auto
hoelzl@56993
   790
    then show "?t ----> \<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M"
hoelzl@56993
   791
      by simp
hoelzl@56993
   792
  qed
hoelzl@56993
   793
qed
hoelzl@56993
   794
hoelzl@56993
   795
lemma has_bochner_integral_eq:
hoelzl@56993
   796
  "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M f y \<Longrightarrow> x = y"
hoelzl@56993
   797
proof (elim has_bochner_integral.cases)
hoelzl@56993
   798
  assume f[measurable]: "f \<in> borel_measurable M"
hoelzl@56993
   799
hoelzl@56993
   800
  fix s t
hoelzl@56993
   801
  assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
hoelzl@56993
   802
  assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x - t i x) \<partial>M) ----> 0" (is "?T ----> 0")
hoelzl@56993
   803
  assume s: "\<And>i. simple_bochner_integrable M (s i)"
hoelzl@56993
   804
  assume t: "\<And>i. simple_bochner_integrable M (t i)"
hoelzl@56993
   805
hoelzl@56993
   806
  have [measurable]: "\<And>i. s i \<in> borel_measurable M" "\<And>i. t i \<in> borel_measurable M"
hoelzl@56993
   807
    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
hoelzl@56993
   808
hoelzl@56993
   809
  let ?s = "\<lambda>i. simple_bochner_integral M (s i)"
hoelzl@56993
   810
  let ?t = "\<lambda>i. simple_bochner_integral M (t i)"
hoelzl@56993
   811
  assume "?s ----> x" "?t ----> y"
hoelzl@56993
   812
  then have "(\<lambda>i. norm (?s i - ?t i)) ----> norm (x - y)"
hoelzl@56993
   813
    by (intro tendsto_intros)
hoelzl@56993
   814
  moreover
hoelzl@56993
   815
  have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
hoelzl@56993
   816
  proof (rule tendsto_sandwich)
hoelzl@56993
   817
    show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
hoelzl@56996
   818
      by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
hoelzl@56993
   819
hoelzl@56993
   820
    show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
hoelzl@56993
   821
      by (intro always_eventually allI simple_bochner_integral_bounded s t f)
hoelzl@56993
   822
    show "(\<lambda>i. ?S i + ?T i) ----> ereal 0"
hoelzl@56993
   823
      using tendsto_add_ereal[OF _ _ `?S ----> 0` `?T ----> 0`]
hoelzl@56993
   824
      by (simp add: zero_ereal_def[symmetric])
hoelzl@56993
   825
  qed
hoelzl@56993
   826
  then have "(\<lambda>i. norm (?s i - ?t i)) ----> 0"
hoelzl@56993
   827
    by simp
hoelzl@56993
   828
  ultimately have "norm (x - y) = 0"
hoelzl@56993
   829
    by (rule LIMSEQ_unique)
hoelzl@56993
   830
  then show "x = y" by simp
hoelzl@56993
   831
qed
hoelzl@56993
   832
hoelzl@56993
   833
lemma has_bochner_integralI_AE:
hoelzl@56993
   834
  assumes f: "has_bochner_integral M f x"
hoelzl@56993
   835
    and g: "g \<in> borel_measurable M"
hoelzl@56993
   836
    and ae: "AE x in M. f x = g x"
hoelzl@56993
   837
  shows "has_bochner_integral M g x"
hoelzl@56993
   838
  using f
hoelzl@56993
   839
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
hoelzl@56993
   840
  fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
hoelzl@56993
   841
  also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M)"
hoelzl@56993
   842
    using ae
hoelzl@56996
   843
    by (intro ext nn_integral_cong_AE, eventually_elim) simp
hoelzl@56993
   844
  finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
hoelzl@56993
   845
qed (auto intro: g)
hoelzl@56993
   846
hoelzl@56993
   847
lemma has_bochner_integral_eq_AE:
hoelzl@56993
   848
  assumes f: "has_bochner_integral M f x"
hoelzl@56993
   849
    and g: "has_bochner_integral M g y"
hoelzl@56993
   850
    and ae: "AE x in M. f x = g x"
hoelzl@56993
   851
  shows "x = y"
hoelzl@56993
   852
proof -
hoelzl@56993
   853
  from assms have "has_bochner_integral M g x"
hoelzl@56993
   854
    by (auto intro: has_bochner_integralI_AE)
hoelzl@56993
   855
  from this g show "x = y"
hoelzl@56993
   856
    by (rule has_bochner_integral_eq)
hoelzl@56993
   857
qed
hoelzl@56993
   858
hoelzl@57137
   859
lemma simple_bochner_integrable_restrict_space:
hoelzl@57137
   860
  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
hoelzl@57137
   861
  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
hoelzl@57137
   862
  shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
hoelzl@57137
   863
    simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
hoelzl@57137
   864
  by (simp add: simple_bochner_integrable.simps space_restrict_space
hoelzl@57137
   865
    simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
hoelzl@57137
   866
    indicator_eq_0_iff conj_ac)
hoelzl@57137
   867
hoelzl@57137
   868
lemma simple_bochner_integral_restrict_space:
hoelzl@57137
   869
  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
hoelzl@57137
   870
  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
hoelzl@57137
   871
  assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
hoelzl@57137
   872
  shows "simple_bochner_integral (restrict_space M \<Omega>) f =
hoelzl@57137
   873
    simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
hoelzl@57137
   874
proof -
hoelzl@57137
   875
  have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
hoelzl@57137
   876
    using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
hoelzl@57137
   877
    by (simp add: simple_bochner_integrable.simps simple_function_def)
hoelzl@57137
   878
  then show ?thesis
hoelzl@57137
   879
    by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
hoelzl@57137
   880
                   simple_bochner_integral_def Collect_restrict
hoelzl@57137
   881
             split: split_indicator split_indicator_asm
hoelzl@57137
   882
             intro!: setsum_mono_zero_cong_left arg_cong2[where f=measure])
hoelzl@57137
   883
qed
hoelzl@57137
   884
hoelzl@56993
   885
inductive integrable for M f where
hoelzl@56993
   886
  "has_bochner_integral M f x \<Longrightarrow> integrable M f"
hoelzl@56993
   887
hoelzl@56993
   888
definition lebesgue_integral ("integral\<^sup>L") where
hoelzl@56993
   889
  "integral\<^sup>L M f = (THE x. has_bochner_integral M f x)"
hoelzl@56993
   890
hoelzl@56993
   891
syntax
hoelzl@56993
   892
  "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110)
hoelzl@56993
   893
hoelzl@56993
   894
translations
hoelzl@56993
   895
  "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
hoelzl@56993
   896
hoelzl@56993
   897
lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
hoelzl@56993
   898
  by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
hoelzl@56993
   899
hoelzl@56993
   900
lemma has_bochner_integral_integrable:
hoelzl@56993
   901
  "integrable M f \<Longrightarrow> has_bochner_integral M f (integral\<^sup>L M f)"
hoelzl@56993
   902
  by (auto simp: has_bochner_integral_integral_eq integrable.simps)
hoelzl@56993
   903
hoelzl@56993
   904
lemma has_bochner_integral_iff:
hoelzl@56993
   905
  "has_bochner_integral M f x \<longleftrightarrow> integrable M f \<and> integral\<^sup>L M f = x"
hoelzl@56993
   906
  by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)
hoelzl@56993
   907
hoelzl@56993
   908
lemma simple_bochner_integrable_eq_integral:
hoelzl@56993
   909
  "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integral M f = integral\<^sup>L M f"
hoelzl@56993
   910
  using has_bochner_integral_simple_bochner_integrable[of M f]
hoelzl@56993
   911
  by (simp add: has_bochner_integral_integral_eq)
hoelzl@56993
   912
hoelzl@56993
   913
lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = (THE x. False)"
hoelzl@56993
   914
  unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
hoelzl@56993
   915
hoelzl@56993
   916
lemma integral_eq_cases:
hoelzl@56993
   917
  "integrable M f \<longleftrightarrow> integrable N g \<Longrightarrow>
hoelzl@56993
   918
    (integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow>
hoelzl@56993
   919
    integral\<^sup>L M f = integral\<^sup>L N g"
hoelzl@56993
   920
  by (metis not_integrable_integral_eq)
hoelzl@56993
   921
hoelzl@56993
   922
lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
hoelzl@56993
   923
  by (auto elim: integrable.cases has_bochner_integral.cases)
hoelzl@56993
   924
hoelzl@56993
   925
lemma integrable_cong:
hoelzl@56993
   926
  "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
hoelzl@56993
   927
  using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
hoelzl@56993
   928
hoelzl@56993
   929
lemma integrable_cong_AE:
hoelzl@56993
   930
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
hoelzl@56993
   931
    integrable M f \<longleftrightarrow> integrable M g"
hoelzl@56993
   932
  unfolding integrable.simps
hoelzl@56993
   933
  by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
hoelzl@56993
   934
hoelzl@56993
   935
lemma integral_cong:
hoelzl@56993
   936
  "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
hoelzl@56993
   937
  using assms by (simp cong: has_bochner_integral_cong add: lebesgue_integral_def)
hoelzl@56993
   938
hoelzl@56993
   939
lemma integral_cong_AE:
hoelzl@56993
   940
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
hoelzl@56993
   941
    integral\<^sup>L M f = integral\<^sup>L M g"
hoelzl@56993
   942
  unfolding lebesgue_integral_def
hoelzl@56993
   943
  by (intro has_bochner_integral_cong_AE arg_cong[where f=The] ext)
hoelzl@56993
   944
hoelzl@56993
   945
lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
hoelzl@57036
   946
  by (auto simp: integrable.simps)
hoelzl@56993
   947
hoelzl@56993
   948
lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
hoelzl@56993
   949
  by (metis has_bochner_integral_zero integrable.simps) 
hoelzl@56993
   950
hoelzl@56993
   951
lemma integrable_setsum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
hoelzl@56993
   952
  by (metis has_bochner_integral_setsum integrable.simps) 
hoelzl@56993
   953
hoelzl@56993
   954
lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
hoelzl@56993
   955
  integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
hoelzl@56993
   956
  by (metis has_bochner_integral_indicator integrable.simps) 
hoelzl@56993
   957
hoelzl@56993
   958
lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
hoelzl@56993
   959
  integrable M (indicator A :: 'a \<Rightarrow> real)"
hoelzl@56993
   960
  by (metis has_bochner_integral_real_indicator integrable.simps)
hoelzl@56993
   961
hoelzl@56993
   962
lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
hoelzl@56993
   963
  by (auto simp: integrable.simps intro: has_bochner_integral_diff)
hoelzl@56993
   964
  
hoelzl@56993
   965
lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
hoelzl@56993
   966
  by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
hoelzl@56993
   967
hoelzl@56993
   968
lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
hoelzl@56993
   969
  unfolding integrable.simps by fastforce
hoelzl@56993
   970
hoelzl@56993
   971
lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
hoelzl@56993
   972
  unfolding integrable.simps by fastforce
hoelzl@56993
   973
hoelzl@56993
   974
lemma integrable_mult_left[simp, intro]:
hoelzl@56993
   975
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
   976
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)"
hoelzl@56993
   977
  unfolding integrable.simps by fastforce
hoelzl@56993
   978
hoelzl@56993
   979
lemma integrable_mult_right[simp, intro]:
hoelzl@56993
   980
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
   981
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)"
hoelzl@56993
   982
  unfolding integrable.simps by fastforce
hoelzl@56993
   983
hoelzl@56993
   984
lemma integrable_divide_zero[simp, intro]:
hoelzl@56993
   985
  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
hoelzl@56993
   986
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
hoelzl@56993
   987
  unfolding integrable.simps by fastforce
hoelzl@56993
   988
hoelzl@56993
   989
lemma integrable_inner_left[simp, intro]:
hoelzl@56993
   990
  "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)"
hoelzl@56993
   991
  unfolding integrable.simps by fastforce
hoelzl@56993
   992
hoelzl@56993
   993
lemma integrable_inner_right[simp, intro]:
hoelzl@56993
   994
  "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)"
hoelzl@56993
   995
  unfolding integrable.simps by fastforce
hoelzl@56993
   996
hoelzl@56993
   997
lemmas integrable_minus[simp, intro] =
hoelzl@56993
   998
  integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
hoelzl@56993
   999
lemmas integrable_divide[simp, intro] =
hoelzl@56993
  1000
  integrable_bounded_linear[OF bounded_linear_divide]
hoelzl@56993
  1001
lemmas integrable_Re[simp, intro] =
hoelzl@56993
  1002
  integrable_bounded_linear[OF bounded_linear_Re]
hoelzl@56993
  1003
lemmas integrable_Im[simp, intro] =
hoelzl@56993
  1004
  integrable_bounded_linear[OF bounded_linear_Im]
hoelzl@56993
  1005
lemmas integrable_cnj[simp, intro] =
hoelzl@56993
  1006
  integrable_bounded_linear[OF bounded_linear_cnj]
hoelzl@56993
  1007
lemmas integrable_of_real[simp, intro] =
hoelzl@56993
  1008
  integrable_bounded_linear[OF bounded_linear_of_real]
hoelzl@56993
  1009
lemmas integrable_fst[simp, intro] =
hoelzl@56993
  1010
  integrable_bounded_linear[OF bounded_linear_fst]
hoelzl@56993
  1011
lemmas integrable_snd[simp, intro] =
hoelzl@56993
  1012
  integrable_bounded_linear[OF bounded_linear_snd]
hoelzl@56993
  1013
hoelzl@56993
  1014
lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
hoelzl@56993
  1015
  by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
hoelzl@56993
  1016
hoelzl@56993
  1017
lemma integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
hoelzl@56993
  1018
    integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g"
hoelzl@56993
  1019
  by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)
hoelzl@56993
  1020
hoelzl@56993
  1021
lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
hoelzl@56993
  1022
    integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
hoelzl@56993
  1023
  by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
hoelzl@56993
  1024
hoelzl@56993
  1025
lemma integral_setsum[simp]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
hoelzl@56993
  1026
  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
hoelzl@56993
  1027
  by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable)
hoelzl@56993
  1028
hoelzl@56993
  1029
lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
hoelzl@56993
  1030
    integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
hoelzl@56993
  1031
  by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
hoelzl@56993
  1032
hoelzl@56993
  1033
lemma integral_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
hoelzl@56993
  1034
  integral\<^sup>L M (\<lambda>x. indicator A x *\<^sub>R c) = measure M A *\<^sub>R c"
hoelzl@56993
  1035
  by (intro has_bochner_integral_integral_eq has_bochner_integral_indicator has_bochner_integral_integrable)
hoelzl@56993
  1036
hoelzl@56993
  1037
lemma integral_real_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
hoelzl@56993
  1038
  integral\<^sup>L M (indicator A :: 'a \<Rightarrow> real) = measure M A"
hoelzl@56993
  1039
  by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator has_bochner_integral_integrable)
hoelzl@56993
  1040
hoelzl@56993
  1041
lemma integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c"
hoelzl@56993
  1042
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
hoelzl@56993
  1043
hoelzl@56993
  1044
lemma integral_scaleR_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
hoelzl@56993
  1045
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_right)
hoelzl@56993
  1046
hoelzl@56993
  1047
lemma integral_mult_left[simp]:
hoelzl@56993
  1048
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
  1049
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
hoelzl@56993
  1050
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
hoelzl@56993
  1051
hoelzl@56993
  1052
lemma integral_mult_right[simp]:
hoelzl@56993
  1053
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
hoelzl@56993
  1054
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
hoelzl@56993
  1055
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
hoelzl@56993
  1056
hoelzl@56993
  1057
lemma integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c"
hoelzl@56993
  1058
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
hoelzl@56993
  1059
hoelzl@56993
  1060
lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f"
hoelzl@56993
  1061
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
hoelzl@56993
  1062
hoelzl@56993
  1063
lemma integral_divide_zero[simp]:
hoelzl@56993
  1064
  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
hoelzl@56993
  1065
  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
hoelzl@56993
  1066
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_divide_zero)
hoelzl@56993
  1067
hoelzl@56993
  1068
lemmas integral_minus[simp] =
hoelzl@56993
  1069
  integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
hoelzl@56993
  1070
lemmas integral_divide[simp] =
hoelzl@56993
  1071
  integral_bounded_linear[OF bounded_linear_divide]
hoelzl@56993
  1072
lemmas integral_Re[simp] =
hoelzl@56993
  1073
  integral_bounded_linear[OF bounded_linear_Re]
hoelzl@56993
  1074
lemmas integral_Im[simp] =
hoelzl@56993
  1075
  integral_bounded_linear[OF bounded_linear_Im]
hoelzl@56993
  1076
lemmas integral_cnj[simp] =
hoelzl@56993
  1077
  integral_bounded_linear[OF bounded_linear_cnj]
hoelzl@56993
  1078
lemmas integral_of_real[simp] =
hoelzl@56993
  1079
  integral_bounded_linear[OF bounded_linear_of_real]
hoelzl@56993
  1080
lemmas integral_fst[simp] =
hoelzl@56993
  1081
  integral_bounded_linear[OF bounded_linear_fst]
hoelzl@56993
  1082
lemmas integral_snd[simp] =
hoelzl@56993
  1083
  integral_bounded_linear[OF bounded_linear_snd]
hoelzl@56993
  1084
hoelzl@56993
  1085
lemma integral_norm_bound_ereal:
hoelzl@56993
  1086
  "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
hoelzl@56993
  1087
  by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
hoelzl@56993
  1088
hoelzl@56993
  1089
lemma integrableI_sequence:
hoelzl@56993
  1090
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1091
  assumes f[measurable]: "f \<in> borel_measurable M"
hoelzl@56993
  1092
  assumes s: "\<And>i. simple_bochner_integrable M (s i)"
hoelzl@56993
  1093
  assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) ----> 0" (is "?S ----> 0")
hoelzl@56993
  1094
  shows "integrable M f"
hoelzl@56993
  1095
proof -
hoelzl@56993
  1096
  let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
hoelzl@56993
  1097
hoelzl@56993
  1098
  have "\<exists>x. ?s ----> x"
hoelzl@56993
  1099
    unfolding convergent_eq_cauchy
hoelzl@56993
  1100
  proof (rule metric_CauchyI)
hoelzl@56993
  1101
    fix e :: real assume "0 < e"
hoelzl@56993
  1102
    then have "0 < ereal (e / 2)" by auto
hoelzl@56993
  1103
    from order_tendstoD(2)[OF lim this]
hoelzl@56993
  1104
    obtain M where M: "\<And>n. M \<le> n \<Longrightarrow> ?S n < e / 2"
hoelzl@56993
  1105
      by (auto simp: eventually_sequentially)
hoelzl@56993
  1106
    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (?s m) (?s n) < e"
hoelzl@56993
  1107
    proof (intro exI allI impI)
hoelzl@56993
  1108
      fix m n assume m: "M \<le> m" and n: "M \<le> n"
hoelzl@56993
  1109
      have "?S n \<noteq> \<infinity>"
hoelzl@56993
  1110
        using M[OF n] by auto
hoelzl@56993
  1111
      have "norm (?s n - ?s m) \<le> ?S n + ?S m"
hoelzl@56993
  1112
        by (intro simple_bochner_integral_bounded s f)
hoelzl@56993
  1113
      also have "\<dots> < ereal (e / 2) + e / 2"
hoelzl@56993
  1114
        using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]]
hoelzl@56996
  1115
        by (auto simp: nn_integral_nonneg)
hoelzl@56993
  1116
      also have "\<dots> = e" by simp
hoelzl@56993
  1117
      finally show "dist (?s n) (?s m) < e"
hoelzl@56993
  1118
        by (simp add: dist_norm)
hoelzl@56993
  1119
    qed
hoelzl@56993
  1120
  qed
hoelzl@56993
  1121
  then obtain x where "?s ----> x" ..
hoelzl@56993
  1122
  show ?thesis
hoelzl@56993
  1123
    by (rule, rule) fact+
hoelzl@56993
  1124
qed
hoelzl@56993
  1125
hoelzl@56996
  1126
lemma nn_integral_dominated_convergence_norm:
hoelzl@56993
  1127
  fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
hoelzl@56993
  1128
  assumes [measurable]:
hoelzl@56993
  1129
       "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
hoelzl@56993
  1130
    and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x"
hoelzl@56993
  1131
    and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
hoelzl@56993
  1132
    and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
hoelzl@56993
  1133
  shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> 0"
hoelzl@56993
  1134
proof -
hoelzl@56993
  1135
  have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
hoelzl@56993
  1136
    unfolding AE_all_countable by rule fact
hoelzl@56993
  1137
  with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
hoelzl@56993
  1138
  proof (eventually_elim, intro allI)
hoelzl@56993
  1139
    fix i x assume "(\<lambda>i. u i x) ----> u' x" "\<forall>j. norm (u j x) \<le> w x" "\<forall>j. norm (u j x) \<le> w x"
hoelzl@56993
  1140
    then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x"
hoelzl@56993
  1141
      by (auto intro: LIMSEQ_le_const2 tendsto_norm)
hoelzl@56993
  1142
    then have "norm (u' x) + norm (u i x) \<le> 2 * w x"
hoelzl@56993
  1143
      by simp
hoelzl@56993
  1144
    also have "norm (u' x - u i x) \<le> norm (u' x) + norm (u i x)"
hoelzl@56993
  1145
      by (rule norm_triangle_ineq4)
hoelzl@56993
  1146
    finally (xtrans) show "norm (u' x - u i x) \<le> 2 * w x" .
hoelzl@56993
  1147
  qed
hoelzl@56993
  1148
  
hoelzl@56993
  1149
  have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
hoelzl@56996
  1150
  proof (rule nn_integral_dominated_convergence)  
hoelzl@56993
  1151
    show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
hoelzl@56996
  1152
      by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
hoelzl@56993
  1153
    show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
hoelzl@56993
  1154
      using u' 
hoelzl@56993
  1155
    proof eventually_elim
hoelzl@56993
  1156
      fix x assume "(\<lambda>i. u i x) ----> u' x"
hoelzl@56993
  1157
      from tendsto_diff[OF tendsto_const[of "u' x"] this]
hoelzl@56993
  1158
      show "(\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
hoelzl@56993
  1159
        by (simp add: zero_ereal_def tendsto_norm_zero_iff)
hoelzl@56993
  1160
    qed
hoelzl@56993
  1161
  qed (insert bnd, auto)
hoelzl@56993
  1162
  then show ?thesis by simp
hoelzl@56993
  1163
qed
hoelzl@56993
  1164
hoelzl@56993
  1165
lemma integrableI_bounded:
hoelzl@56993
  1166
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1167
  assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
hoelzl@56993
  1168
  shows "integrable M f"
hoelzl@56993
  1169
proof -
hoelzl@56993
  1170
  from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
hoelzl@56993
  1171
    s: "\<And>i. simple_function M (s i)" and
hoelzl@56993
  1172
    pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x" and
hoelzl@56993
  1173
    bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
hoelzl@56993
  1174
    by (simp add: norm_conv_dist) metis
hoelzl@56993
  1175
  
hoelzl@56993
  1176
  show ?thesis
hoelzl@56993
  1177
  proof (rule integrableI_sequence)
hoelzl@56993
  1178
    { fix i
hoelzl@56993
  1179
      have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1180
        by (intro nn_integral_mono) (simp add: bound)
hoelzl@56993
  1181
      also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1182
        by (rule nn_integral_cmult) auto
hoelzl@56993
  1183
      finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
hoelzl@56993
  1184
        using fin by auto }
hoelzl@56993
  1185
    note fin_s = this
hoelzl@56993
  1186
hoelzl@56993
  1187
    show "\<And>i. simple_bochner_integrable M (s i)"
hoelzl@56993
  1188
      by (rule simple_bochner_integrableI_bounded) fact+
hoelzl@56993
  1189
hoelzl@56993
  1190
    show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
hoelzl@56996
  1191
    proof (rule nn_integral_dominated_convergence_norm)
hoelzl@56993
  1192
      show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
hoelzl@56993
  1193
        using bound by auto
hoelzl@56993
  1194
      show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
hoelzl@56993
  1195
        using s by (auto intro: borel_measurable_simple_function)
hoelzl@56993
  1196
      show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
hoelzl@56996
  1197
        using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
hoelzl@56993
  1198
      show "AE x in M. (\<lambda>i. s i x) ----> f x"
hoelzl@56993
  1199
        using pointwise by auto
hoelzl@56993
  1200
    qed fact
hoelzl@56993
  1201
  qed fact
hoelzl@56993
  1202
qed
hoelzl@56993
  1203
hoelzl@56993
  1204
lemma integrableI_nonneg:
hoelzl@56993
  1205
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1206
  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
hoelzl@56993
  1207
  shows "integrable M f"
hoelzl@56993
  1208
proof -
hoelzl@56993
  1209
  have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
hoelzl@56996
  1210
    using assms by (intro nn_integral_cong_AE) auto
hoelzl@56993
  1211
  then show ?thesis
hoelzl@56993
  1212
    using assms by (intro integrableI_bounded) auto
hoelzl@56993
  1213
qed
hoelzl@56993
  1214
hoelzl@56993
  1215
lemma integrable_iff_bounded:
hoelzl@56993
  1216
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1217
  shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
hoelzl@56993
  1218
  using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
hoelzl@56993
  1219
  unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
hoelzl@56993
  1220
hoelzl@56993
  1221
lemma integrable_bound:
hoelzl@56993
  1222
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1223
    and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
hoelzl@56993
  1224
  shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow>
hoelzl@56993
  1225
    integrable M g"
hoelzl@56993
  1226
  unfolding integrable_iff_bounded
hoelzl@56993
  1227
proof safe
hoelzl@56993
  1228
  assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@56993
  1229
  assume "AE x in M. norm (g x) \<le> norm (f x)"
hoelzl@56993
  1230
  then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1231
    by  (intro nn_integral_mono_AE) auto
hoelzl@56993
  1232
  also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
hoelzl@56993
  1233
  finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
hoelzl@56993
  1234
qed 
hoelzl@56993
  1235
hoelzl@56993
  1236
lemma integrable_abs[simp, intro]:
hoelzl@56993
  1237
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1238
  assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
hoelzl@56993
  1239
  using assms by (rule integrable_bound) auto
hoelzl@56993
  1240
hoelzl@56993
  1241
lemma integrable_norm[simp, intro]:
hoelzl@56993
  1242
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1243
  assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))"
hoelzl@56993
  1244
  using assms by (rule integrable_bound) auto
hoelzl@56993
  1245
  
hoelzl@56993
  1246
lemma integrable_norm_cancel:
hoelzl@56993
  1247
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1248
  assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
hoelzl@56993
  1249
  using assms by (rule integrable_bound) auto
hoelzl@56993
  1250
hoelzl@56993
  1251
lemma integrable_abs_cancel:
hoelzl@56993
  1252
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1253
  assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
hoelzl@56993
  1254
  using assms by (rule integrable_bound) auto
hoelzl@56993
  1255
hoelzl@56993
  1256
lemma integrable_max[simp, intro]:
hoelzl@56993
  1257
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1258
  assumes fg[measurable]: "integrable M f" "integrable M g"
hoelzl@56993
  1259
  shows "integrable M (\<lambda>x. max (f x) (g x))"
hoelzl@56993
  1260
  using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
hoelzl@56993
  1261
  by (rule integrable_bound) auto
hoelzl@56993
  1262
hoelzl@56993
  1263
lemma integrable_min[simp, intro]:
hoelzl@56993
  1264
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1265
  assumes fg[measurable]: "integrable M f" "integrable M g"
hoelzl@56993
  1266
  shows "integrable M (\<lambda>x. min (f x) (g x))"
hoelzl@56993
  1267
  using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
hoelzl@56993
  1268
  by (rule integrable_bound) auto
hoelzl@56993
  1269
hoelzl@56993
  1270
lemma integral_minus_iff[simp]:
hoelzl@56993
  1271
  "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
hoelzl@56993
  1272
  unfolding integrable_iff_bounded
hoelzl@56993
  1273
  by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
hoelzl@56993
  1274
hoelzl@56993
  1275
lemma integrable_indicator_iff:
hoelzl@56993
  1276
  "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
hoelzl@56996
  1277
  by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
hoelzl@56993
  1278
           cong: conj_cong)
hoelzl@56993
  1279
hoelzl@57137
  1280
lemma
hoelzl@56993
  1281
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
hoelzl@56993
  1282
  assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
hoelzl@56993
  1283
  assumes lim: "AE x in M. (\<lambda>i. s i x) ----> f x"
hoelzl@56993
  1284
  assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
hoelzl@57137
  1285
  shows integrable_dominated_convergence: "integrable M f"
hoelzl@57137
  1286
    and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
hoelzl@57137
  1287
    and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
hoelzl@56993
  1288
proof -
hoelzl@56993
  1289
  have "AE x in M. 0 \<le> w x"
hoelzl@56993
  1290
    using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
hoelzl@56993
  1291
  then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
hoelzl@56996
  1292
    by (intro nn_integral_cong_AE) auto
hoelzl@56993
  1293
  with `integrable M w` have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
hoelzl@56993
  1294
    unfolding integrable_iff_bounded by auto
hoelzl@56993
  1295
hoelzl@56993
  1296
  show int_s: "\<And>i. integrable M (s i)"
hoelzl@56993
  1297
    unfolding integrable_iff_bounded
hoelzl@56993
  1298
  proof
hoelzl@56993
  1299
    fix i 
hoelzl@56993
  1300
    have "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
hoelzl@56996
  1301
      using bound by (intro nn_integral_mono_AE) auto
hoelzl@56993
  1302
    with w show "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) < \<infinity>" by auto
hoelzl@56993
  1303
  qed fact
hoelzl@56993
  1304
hoelzl@56993
  1305
  have all_bound: "AE x in M. \<forall>i. norm (s i x) \<le> w x"
hoelzl@56993
  1306
    using bound unfolding AE_all_countable by auto
hoelzl@56993
  1307
hoelzl@56993
  1308
  show int_f: "integrable M f"
hoelzl@56993
  1309
    unfolding integrable_iff_bounded
hoelzl@56993
  1310
  proof
hoelzl@56993
  1311
    have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
hoelzl@56993
  1312
      using all_bound lim
hoelzl@56996
  1313
    proof (intro nn_integral_mono_AE, eventually_elim)
hoelzl@56993
  1314
      fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
hoelzl@56993
  1315
      then show "ereal (norm (f x)) \<le> ereal (w x)"
hoelzl@56993
  1316
        by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
hoelzl@56993
  1317
    qed
hoelzl@56993
  1318
    with w show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" by auto
hoelzl@56993
  1319
  qed fact
hoelzl@56993
  1320
hoelzl@56993
  1321
  have "(\<lambda>n. ereal (norm (integral\<^sup>L M (s n) - integral\<^sup>L M f))) ----> ereal 0" (is "?d ----> ereal 0")
hoelzl@56993
  1322
  proof (rule tendsto_sandwich)
hoelzl@56993
  1323
    show "eventually (\<lambda>n. ereal 0 \<le> ?d n) sequentially" "(\<lambda>_. ereal 0) ----> ereal 0" by auto
hoelzl@56993
  1324
    show "eventually (\<lambda>n. ?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)) sequentially"
hoelzl@56993
  1325
    proof (intro always_eventually allI)
hoelzl@56993
  1326
      fix n
hoelzl@56993
  1327
      have "?d n = norm (integral\<^sup>L M (\<lambda>x. s n x - f x))"
hoelzl@56993
  1328
        using int_f int_s by simp
hoelzl@56993
  1329
      also have "\<dots> \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)"
hoelzl@56993
  1330
        by (intro int_f int_s integrable_diff integral_norm_bound_ereal)
hoelzl@56993
  1331
      finally show "?d n \<le> (\<integral>\<^sup>+x. norm (s n x - f x) \<partial>M)" .
hoelzl@56993
  1332
    qed
hoelzl@56993
  1333
    show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
hoelzl@56993
  1334
      unfolding zero_ereal_def[symmetric]
hoelzl@56993
  1335
      apply (subst norm_minus_commute)
hoelzl@56996
  1336
    proof (rule nn_integral_dominated_convergence_norm[where w=w])
hoelzl@56993
  1337
      show "\<And>n. s n \<in> borel_measurable M"
hoelzl@56993
  1338
        using int_s unfolding integrable_iff_bounded by auto
hoelzl@56993
  1339
    qed fact+
hoelzl@56993
  1340
  qed
hoelzl@56993
  1341
  then have "(\<lambda>n. integral\<^sup>L M (s n) - integral\<^sup>L M f) ----> 0"
hoelzl@56993
  1342
    unfolding lim_ereal tendsto_norm_zero_iff .
hoelzl@56993
  1343
  from tendsto_add[OF this tendsto_const[of "integral\<^sup>L M f"]]
hoelzl@56993
  1344
  show "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"  by simp
hoelzl@56993
  1345
qed
hoelzl@56993
  1346
hoelzl@56993
  1347
lemma integrable_mult_left_iff:
hoelzl@56993
  1348
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1349
  shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
hoelzl@56993
  1350
  using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
hoelzl@56993
  1351
  by (cases "c = 0") auto
hoelzl@56993
  1352
hoelzl@56996
  1353
lemma nn_integral_eq_integral:
hoelzl@56993
  1354
  assumes f: "integrable M f"
hoelzl@56993
  1355
  assumes nonneg: "AE x in M. 0 \<le> f x" 
hoelzl@56993
  1356
  shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
hoelzl@56993
  1357
proof -
hoelzl@56993
  1358
  { fix f :: "'a \<Rightarrow> real" assume f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "integrable M f"
hoelzl@56993
  1359
    then have "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
hoelzl@56993
  1360
    proof (induct rule: borel_measurable_induct_real)
hoelzl@56993
  1361
      case (set A) then show ?case
hoelzl@56993
  1362
        by (simp add: integrable_indicator_iff ereal_indicator emeasure_eq_ereal_measure)
hoelzl@56993
  1363
    next
hoelzl@56993
  1364
      case (mult f c) then show ?case
hoelzl@56993
  1365
        unfolding times_ereal.simps(1)[symmetric]
hoelzl@56996
  1366
        by (subst nn_integral_cmult)
hoelzl@56993
  1367
           (auto simp add: integrable_mult_left_iff zero_ereal_def[symmetric])
hoelzl@56993
  1368
    next
hoelzl@56993
  1369
      case (add g f)
hoelzl@56993
  1370
      then have "integrable M f" "integrable M g"
hoelzl@56993
  1371
        by (auto intro!: integrable_bound[OF add(8)])
hoelzl@56993
  1372
      with add show ?case
hoelzl@56993
  1373
        unfolding plus_ereal.simps(1)[symmetric]
hoelzl@56996
  1374
        by (subst nn_integral_add) auto
hoelzl@56993
  1375
    next
hoelzl@56993
  1376
      case (seq s)
hoelzl@56993
  1377
      { fix i x assume "x \<in> space M" with seq(4) have "s i x \<le> f x"
hoelzl@56993
  1378
          by (intro LIMSEQ_le_const[OF seq(5)] exI[of _ i]) (auto simp: incseq_def le_fun_def) }
hoelzl@56993
  1379
      note s_le_f = this
hoelzl@56993
  1380
hoelzl@56993
  1381
      show ?case
hoelzl@56993
  1382
      proof (rule LIMSEQ_unique)
hoelzl@56993
  1383
        show "(\<lambda>i. ereal (integral\<^sup>L M (s i))) ----> ereal (integral\<^sup>L M f)"
hoelzl@56993
  1384
          unfolding lim_ereal
hoelzl@56993
  1385
        proof (rule integral_dominated_convergence[where w=f])
hoelzl@56993
  1386
          show "integrable M f" by fact
hoelzl@56993
  1387
          from s_le_f seq show "\<And>i. AE x in M. norm (s i x) \<le> f x"
hoelzl@56993
  1388
            by auto
hoelzl@56993
  1389
        qed (insert seq, auto)
hoelzl@56993
  1390
        have int_s: "\<And>i. integrable M (s i)"
hoelzl@56993
  1391
          using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
hoelzl@56993
  1392
        have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
hoelzl@56993
  1393
          using seq s_le_f f
hoelzl@56996
  1394
          by (intro nn_integral_dominated_convergence[where w=f])
hoelzl@56993
  1395
             (auto simp: integrable_iff_bounded)
hoelzl@56993
  1396
        also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
hoelzl@56993
  1397
          using seq int_s by simp
hoelzl@56993
  1398
        finally show "(\<lambda>i. \<integral>x. s i x \<partial>M) ----> \<integral>\<^sup>+x. f x \<partial>M"
hoelzl@56993
  1399
          by simp
hoelzl@56993
  1400
      qed
hoelzl@56993
  1401
    qed }
hoelzl@56993
  1402
  from this[of "\<lambda>x. max 0 (f x)"] assms have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = integral\<^sup>L M (\<lambda>x. max 0 (f x))"
hoelzl@56993
  1403
    by simp
hoelzl@56993
  1404
  also have "\<dots> = integral\<^sup>L M f"
hoelzl@56993
  1405
    using assms by (auto intro!: integral_cong_AE)
hoelzl@56993
  1406
  also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
hoelzl@56996
  1407
    using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
hoelzl@56993
  1408
  finally show ?thesis .
hoelzl@56993
  1409
qed
hoelzl@56993
  1410
hoelzl@57036
  1411
lemma
hoelzl@57036
  1412
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
hoelzl@57036
  1413
  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
hoelzl@57036
  1414
  and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
hoelzl@57036
  1415
  and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
hoelzl@57036
  1416
  shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
hoelzl@57036
  1417
    and sums_integral: "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is "?f sums ?x")
hoelzl@57036
  1418
    and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
hoelzl@57036
  1419
    and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
hoelzl@57036
  1420
proof -
hoelzl@57036
  1421
  have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
hoelzl@57036
  1422
  proof (rule integrableI_bounded)
hoelzl@57036
  1423
    have "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) = (\<integral>\<^sup>+ x. (\<Sum>i. ereal (norm (f i x))) \<partial>M)"
hoelzl@57036
  1424
      apply (intro nn_integral_cong_AE) 
hoelzl@57036
  1425
      using summable
hoelzl@57036
  1426
      apply eventually_elim
hoelzl@57036
  1427
      apply (simp add: suminf_ereal' suminf_nonneg)
hoelzl@57036
  1428
      done
hoelzl@57036
  1429
    also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
hoelzl@57036
  1430
      by (intro nn_integral_suminf) auto
hoelzl@57036
  1431
    also have "\<dots> = (\<Sum>i. ereal (\<integral>x. norm (f i x) \<partial>M))"
hoelzl@57036
  1432
      by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
hoelzl@57036
  1433
    finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
hoelzl@57036
  1434
      by (simp add: suminf_ereal' sums)
hoelzl@57036
  1435
  qed simp
hoelzl@57036
  1436
hoelzl@57036
  1437
  have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
hoelzl@57036
  1438
    using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
hoelzl@57036
  1439
hoelzl@57036
  1440
  have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
hoelzl@57036
  1441
    using summable
hoelzl@57036
  1442
  proof eventually_elim
hoelzl@57036
  1443
    fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
hoelzl@57036
  1444
    have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_setsum)
hoelzl@57036
  1445
    also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
hoelzl@57036
  1446
      using setsum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
hoelzl@57036
  1447
    finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
hoelzl@57036
  1448
  qed
hoelzl@57036
  1449
hoelzl@57137
  1450
  note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
hoelzl@57137
  1451
  note int = integral_dominated_convergence[OF _ _ 1 2 3]
hoelzl@57036
  1452
hoelzl@57036
  1453
  show "integrable M ?S"
hoelzl@57137
  1454
    by (rule ibl) measurable
hoelzl@57036
  1455
hoelzl@57036
  1456
  show "?f sums ?x" unfolding sums_def
hoelzl@57137
  1457
    using int by (simp add: integrable)
hoelzl@57036
  1458
  then show "?x = suminf ?f" "summable ?f"
hoelzl@57036
  1459
    unfolding sums_iff by auto
hoelzl@57036
  1460
qed
hoelzl@57036
  1461
hoelzl@56993
  1462
lemma integral_norm_bound:
hoelzl@56993
  1463
  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
hoelzl@56993
  1464
  shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
hoelzl@56996
  1465
  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
hoelzl@56993
  1466
  using integral_norm_bound_ereal[of M f] by simp
hoelzl@56993
  1467
  
hoelzl@56996
  1468
lemma integral_eq_nn_integral:
hoelzl@56993
  1469
  "integrable M f \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
hoelzl@56996
  1470
  by (subst nn_integral_eq_integral) auto
hoelzl@56993
  1471
  
hoelzl@56993
  1472
lemma integrableI_simple_bochner_integrable:
hoelzl@56993
  1473
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1474
  shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
hoelzl@56993
  1475
  by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
hoelzl@56993
  1476
     (auto simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps)
hoelzl@56993
  1477
hoelzl@56993
  1478
lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
hoelzl@56993
  1479
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1480
  assumes "integrable M f"
hoelzl@56993
  1481
  assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
hoelzl@56993
  1482
  assumes add: "\<And>f g. integrable M f \<Longrightarrow> P f \<Longrightarrow> integrable M g \<Longrightarrow> P g \<Longrightarrow> P (\<lambda>x. f x + g x)"
hoelzl@56993
  1483
  assumes lim: "\<And>f s. (\<And>i. integrable M (s i)) \<Longrightarrow> (\<And>i. P (s i)) \<Longrightarrow>
hoelzl@56993
  1484
   (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x) \<Longrightarrow>
hoelzl@56993
  1485
   (\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
hoelzl@56993
  1486
  shows "P f"
hoelzl@56993
  1487
proof -
hoelzl@56993
  1488
  from `integrable M f` have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
hoelzl@56993
  1489
    unfolding integrable_iff_bounded by auto
hoelzl@56993
  1490
  from borel_measurable_implies_sequence_metric[OF f(1)]
hoelzl@56993
  1491
  obtain s where s: "\<And>i. simple_function M (s i)" "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) ----> f x"
hoelzl@56993
  1492
    "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
hoelzl@56993
  1493
    unfolding norm_conv_dist by metis
hoelzl@56993
  1494
hoelzl@56993
  1495
  { fix f A 
hoelzl@56993
  1496
    have [simp]: "P (\<lambda>x. 0)"
hoelzl@56993
  1497
      using base[of "{}" undefined] by simp
hoelzl@56993
  1498
    have "(\<And>i::'b. i \<in> A \<Longrightarrow> integrable M (f i::'a \<Rightarrow> 'b)) \<Longrightarrow>
hoelzl@56993
  1499
    (\<And>i. i \<in> A \<Longrightarrow> P (f i)) \<Longrightarrow> P (\<lambda>x. \<Sum>i\<in>A. f i x)"
hoelzl@56993
  1500
    by (induct A rule: infinite_finite_induct) (auto intro!: add) }
hoelzl@56993
  1501
  note setsum = this
hoelzl@56993
  1502
hoelzl@56993
  1503
  def s' \<equiv> "\<lambda>i z. indicator (space M) z *\<^sub>R s i z"
hoelzl@56993
  1504
  then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x"
hoelzl@56993
  1505
    by simp
hoelzl@56993
  1506
hoelzl@56993
  1507
  have sf[measurable]: "\<And>i. simple_function M (s' i)"
hoelzl@56993
  1508
    unfolding s'_def using s(1)
hoelzl@56993
  1509
    by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
hoelzl@56993
  1510
hoelzl@56993
  1511
  { fix i 
hoelzl@56993
  1512
    have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
hoelzl@56993
  1513
        (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})"
hoelzl@56993
  1514
      by (auto simp add: s'_def split: split_indicator)
hoelzl@56993
  1515
    then have "\<And>z. s' i = (\<lambda>z. \<Sum>y\<in>s' i`space M - {0}. indicator {x\<in>space M. s' i x = y} z *\<^sub>R y)"
hoelzl@56993
  1516
      using sf by (auto simp: fun_eq_iff simple_function_def s'_def) }
hoelzl@56993
  1517
  note s'_eq = this
hoelzl@56993
  1518
hoelzl@56993
  1519
  show "P f"
hoelzl@56993
  1520
  proof (rule lim)
hoelzl@56993
  1521
    fix i
hoelzl@56993
  1522
hoelzl@56993
  1523
    have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1524
      using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
hoelzl@56993
  1525
    also have "\<dots> < \<infinity>"
hoelzl@56996
  1526
      using f by (subst nn_integral_cmult) auto
hoelzl@56993
  1527
    finally have sbi: "simple_bochner_integrable M (s' i)"
hoelzl@56993
  1528
      using sf by (intro simple_bochner_integrableI_bounded) auto
hoelzl@56993
  1529
    then show "integrable M (s' i)"
hoelzl@56993
  1530
      by (rule integrableI_simple_bochner_integrable)
hoelzl@56993
  1531
hoelzl@56993
  1532
    { fix x assume"x \<in> space M" "s' i x \<noteq> 0"
hoelzl@56993
  1533
      then have "emeasure M {y \<in> space M. s' i y = s' i x} \<le> emeasure M {y \<in> space M. s' i y \<noteq> 0}"
hoelzl@56993
  1534
        by (intro emeasure_mono) auto
hoelzl@56993
  1535
      also have "\<dots> < \<infinity>"
hoelzl@56993
  1536
        using sbi by (auto elim: simple_bochner_integrable.cases)
hoelzl@56993
  1537
      finally have "emeasure M {y \<in> space M. s' i y = s' i x} \<noteq> \<infinity>" by simp }
hoelzl@56993
  1538
    then show "P (s' i)"
hoelzl@56993
  1539
      by (subst s'_eq) (auto intro!: setsum base)
hoelzl@56993
  1540
hoelzl@56993
  1541
    fix x assume "x \<in> space M" with s show "(\<lambda>i. s' i x) ----> f x"
hoelzl@56993
  1542
      by (simp add: s'_eq_s)
hoelzl@56993
  1543
    show "norm (s' i x) \<le> 2 * norm (f x)"
hoelzl@56993
  1544
      using `x \<in> space M` s by (simp add: s'_eq_s)
hoelzl@56993
  1545
  qed fact
hoelzl@56993
  1546
qed
hoelzl@56993
  1547
hoelzl@56993
  1548
lemma integral_nonneg_AE:
hoelzl@56993
  1549
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1550
  assumes [measurable]: "integrable M f" "AE x in M. 0 \<le> f x"
hoelzl@56993
  1551
  shows "0 \<le> integral\<^sup>L M f"
hoelzl@56993
  1552
proof -
hoelzl@56993
  1553
  have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
hoelzl@57036
  1554
    by (subst integral_eq_nn_integral) (auto intro: real_of_ereal_pos nn_integral_nonneg assms)
hoelzl@56993
  1555
  also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
hoelzl@56993
  1556
    using assms(2) by (intro integral_cong_AE assms integrable_max) auto
hoelzl@56993
  1557
  finally show ?thesis
hoelzl@56993
  1558
    by simp
hoelzl@56993
  1559
qed
hoelzl@56993
  1560
hoelzl@56993
  1561
lemma integral_eq_zero_AE:
hoelzl@56993
  1562
  "f \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
hoelzl@56993
  1563
  using integral_cong_AE[of f M "\<lambda>_. 0"] by simp
hoelzl@56993
  1564
hoelzl@56993
  1565
lemma integral_nonneg_eq_0_iff_AE:
hoelzl@56993
  1566
  fixes f :: "_ \<Rightarrow> real"
hoelzl@56993
  1567
  assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
hoelzl@56993
  1568
  shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
hoelzl@56993
  1569
proof
hoelzl@56993
  1570
  assume "integral\<^sup>L M f = 0"
hoelzl@56996
  1571
  then have "integral\<^sup>N M f = 0"
hoelzl@56996
  1572
    using nn_integral_eq_integral[OF f nonneg] by simp
hoelzl@56993
  1573
  then have "AE x in M. ereal (f x) \<le> 0"
hoelzl@56996
  1574
    by (simp add: nn_integral_0_iff_AE)
hoelzl@56993
  1575
  with nonneg show "AE x in M. f x = 0"
hoelzl@56993
  1576
    by auto
hoelzl@56993
  1577
qed (auto simp add: integral_eq_zero_AE)
hoelzl@56993
  1578
hoelzl@56993
  1579
lemma integral_mono_AE:
hoelzl@56993
  1580
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1581
  assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
hoelzl@56993
  1582
  shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
hoelzl@56993
  1583
proof -
hoelzl@56993
  1584
  have "0 \<le> integral\<^sup>L M (\<lambda>x. g x - f x)"
hoelzl@56993
  1585
    using assms by (intro integral_nonneg_AE integrable_diff assms) auto
hoelzl@56993
  1586
  also have "\<dots> = integral\<^sup>L M g - integral\<^sup>L M f"
hoelzl@56993
  1587
    by (intro integral_diff assms)
hoelzl@56993
  1588
  finally show ?thesis by simp
hoelzl@56993
  1589
qed
hoelzl@56993
  1590
hoelzl@56993
  1591
lemma integral_mono:
hoelzl@56993
  1592
  fixes f :: "'a \<Rightarrow> real"
hoelzl@56993
  1593
  shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow> 
hoelzl@56993
  1594
    integral\<^sup>L M f \<le> integral\<^sup>L M g"
hoelzl@56993
  1595
  by (intro integral_mono_AE) auto
hoelzl@56993
  1596
hoelzl@57025
  1597
lemma (in finite_measure) integrable_measure: 
hoelzl@57025
  1598
  assumes I: "disjoint_family_on X I" "countable I"
hoelzl@57025
  1599
  shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
hoelzl@57025
  1600
proof -
hoelzl@57025
  1601
  have "(\<integral>\<^sup>+i. measure M (X i) \<partial>count_space I) = (\<integral>\<^sup>+i. measure M (if X i \<in> sets M then X i else {}) \<partial>count_space I)"
hoelzl@57025
  1602
    by (auto intro!: nn_integral_cong measure_notin_sets)
hoelzl@57025
  1603
  also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
hoelzl@57025
  1604
    using I unfolding emeasure_eq_measure[symmetric]
hoelzl@57025
  1605
    by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
hoelzl@57025
  1606
  finally show ?thesis
hoelzl@57025
  1607
    by (auto intro!: integrableI_bounded simp: measure_nonneg)
hoelzl@57025
  1608
qed
hoelzl@57025
  1609
hoelzl@57025
  1610
lemma integrableI_real_bounded:
hoelzl@57025
  1611
  assumes f: "f \<in> borel_measurable M" and ae: "AE x in M. 0 \<le> f x" and fin: "integral\<^sup>N M f < \<infinity>"
hoelzl@57025
  1612
  shows "integrable M f"
hoelzl@57025
  1613
proof (rule integrableI_bounded)
hoelzl@57025
  1614
  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ereal (f x) \<partial>M"
hoelzl@57025
  1615
    using ae by (auto intro: nn_integral_cong_AE)
hoelzl@57025
  1616
  also note fin
hoelzl@57025
  1617
  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
hoelzl@57025
  1618
qed fact
hoelzl@57025
  1619
hoelzl@57025
  1620
lemma integral_real_bounded:
hoelzl@57025
  1621
  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
hoelzl@57025
  1622
  shows "integral\<^sup>L M f \<le> r"
hoelzl@57025
  1623
proof -
hoelzl@57025
  1624
  have "integrable M f"
hoelzl@57025
  1625
    using assms by (intro integrableI_real_bounded) auto
hoelzl@57025
  1626
  from nn_integral_eq_integral[OF this] assms show ?thesis
hoelzl@57025
  1627
    by simp
hoelzl@57025
  1628
qed
hoelzl@57025
  1629
hoelzl@57137
  1630
subsection {* Restricted measure spaces *}
hoelzl@57137
  1631
hoelzl@57137
  1632
lemma integrable_restrict_space:
hoelzl@57137
  1633
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@57137
  1634
  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
hoelzl@57137
  1635
  shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
hoelzl@57137
  1636
  unfolding integrable_iff_bounded
hoelzl@57137
  1637
    borel_measurable_restrict_space_iff[OF \<Omega>]
hoelzl@57137
  1638
    nn_integral_restrict_space[OF \<Omega>]
hoelzl@57137
  1639
  by (simp add: ac_simps ereal_indicator times_ereal.simps(1)[symmetric] del: times_ereal.simps)
hoelzl@57137
  1640
hoelzl@57137
  1641
lemma integral_restrict_space:
hoelzl@57137
  1642
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@57137
  1643
  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
hoelzl@57137
  1644
  shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
hoelzl@57137
  1645
proof (rule integral_eq_cases)
hoelzl@57137
  1646
  assume "integrable (restrict_space M \<Omega>) f"
hoelzl@57137
  1647
  then show ?thesis
hoelzl@57137
  1648
  proof induct
hoelzl@57137
  1649
    case (base A c) then show ?case
hoelzl@57137
  1650
      by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
hoelzl@57137
  1651
                    emeasure_restrict_space Int_absorb1 measure_restrict_space)
hoelzl@57137
  1652
  next
hoelzl@57137
  1653
    case (add g f) then show ?case
hoelzl@57137
  1654
      by (simp add: scaleR_add_right integrable_restrict_space)
hoelzl@57137
  1655
  next
hoelzl@57137
  1656
    case (lim f s)
hoelzl@57137
  1657
    show ?case
hoelzl@57137
  1658
    proof (rule LIMSEQ_unique)
hoelzl@57137
  1659
      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> integral\<^sup>L (restrict_space M \<Omega>) f"
hoelzl@57137
  1660
        using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
hoelzl@57137
  1661
      
hoelzl@57137
  1662
      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
hoelzl@57137
  1663
        unfolding lim
hoelzl@57137
  1664
        using lim
hoelzl@57137
  1665
        by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
hoelzl@57137
  1666
           (auto simp add: space_restrict_space integrable_restrict_space
hoelzl@57137
  1667
                 simp del: norm_scaleR
hoelzl@57137
  1668
                 split: split_indicator)
hoelzl@57137
  1669
    qed
hoelzl@57137
  1670
  qed
hoelzl@57137
  1671
qed (simp add: integrable_restrict_space)
hoelzl@57137
  1672
hoelzl@56994
  1673
subsection {* Measure spaces with an associated density *}
hoelzl@56993
  1674
hoelzl@56993
  1675
lemma integrable_density:
hoelzl@56993
  1676
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
hoelzl@56993
  1677
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@56993
  1678
    and nn: "AE x in M. 0 \<le> g x"
hoelzl@56993
  1679
  shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
hoelzl@56993
  1680
  unfolding integrable_iff_bounded using nn
hoelzl@56996
  1681
  apply (simp add: nn_integral_density )
hoelzl@56996
  1682
  apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
hoelzl@56993
  1683
  apply auto
hoelzl@56993
  1684
  done
hoelzl@56993
  1685
hoelzl@56993
  1686
lemma integral_density:
hoelzl@56993
  1687
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
hoelzl@56993
  1688
  assumes f: "f \<in> borel_measurable M"
hoelzl@56993
  1689
    and g[measurable]: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
hoelzl@56993
  1690
  shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
hoelzl@56993
  1691
proof (rule integral_eq_cases)
hoelzl@56993
  1692
  assume "integrable (density M g) f"
hoelzl@56993
  1693
  then show ?thesis
hoelzl@56993
  1694
  proof induct
hoelzl@56993
  1695
    case (base A c)
hoelzl@56993
  1696
    then have [measurable]: "A \<in> sets M" by auto
hoelzl@56993
  1697
  
hoelzl@56993
  1698
    have int: "integrable M (\<lambda>x. g x * indicator A x)"
hoelzl@56993
  1699
      using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
hoelzl@56993
  1700
    then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ereal (g x * indicator A x) \<partial>M)"
hoelzl@56996
  1701
      using g by (subst nn_integral_eq_integral) auto
hoelzl@56993
  1702
    also have "\<dots> = (\<integral>\<^sup>+ x. ereal (g x) * indicator A x \<partial>M)"
hoelzl@56996
  1703
      by (intro nn_integral_cong) (auto split: split_indicator)
hoelzl@56993
  1704
    also have "\<dots> = emeasure (density M g) A"
hoelzl@56993
  1705
      by (rule emeasure_density[symmetric]) auto
hoelzl@56993
  1706
    also have "\<dots> = ereal (measure (density M g) A)"
hoelzl@56993
  1707
      using base by (auto intro: emeasure_eq_ereal_measure)
hoelzl@56993
  1708
    also have "\<dots> = integral\<^sup>L (density M g) (indicator A)"
hoelzl@56993
  1709
      using base by simp
hoelzl@56993
  1710
    finally show ?case
hoelzl@56993
  1711
      using base by (simp add: int)
hoelzl@56993
  1712
  next
hoelzl@56993
  1713
    case (add f h)
hoelzl@56993
  1714
    then have [measurable]: "f \<in> borel_measurable M" "h \<in> borel_measurable M"
hoelzl@56993
  1715
      by (auto dest!: borel_measurable_integrable)
hoelzl@56993
  1716
    from add g show ?case
hoelzl@56993
  1717
      by (simp add: scaleR_add_right integrable_density)
hoelzl@56993
  1718
  next
hoelzl@56993
  1719
    case (lim f s)
hoelzl@56993
  1720
    have [measurable]: "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M"
hoelzl@56993
  1721
      using lim(1,5)[THEN borel_measurable_integrable] by auto
hoelzl@56993
  1722
  
hoelzl@56993
  1723
    show ?case
hoelzl@56993
  1724
    proof (rule LIMSEQ_unique)
hoelzl@56993
  1725
      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
hoelzl@57137
  1726
      proof (rule integral_dominated_convergence)
hoelzl@56993
  1727
        show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
hoelzl@56993
  1728
          by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
hoelzl@56993
  1729
        show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x"
hoelzl@56993
  1730
          using lim(3) by (auto intro!: tendsto_scaleR AE_I2[of M])
hoelzl@56993
  1731
        show "\<And>i. AE x in M. norm (g x *\<^sub>R s i x) \<le> 2 * norm (g x *\<^sub>R f x)"
hoelzl@56993
  1732
          using lim(4) g by (auto intro!: AE_I2[of M] mult_left_mono simp: field_simps)
hoelzl@56993
  1733
      qed auto
hoelzl@56993
  1734
      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
hoelzl@56993
  1735
        unfolding lim(2)[symmetric]
hoelzl@57137
  1736
        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
hoelzl@57036
  1737
           (insert lim(3-5), auto)
hoelzl@56993
  1738
    qed
hoelzl@56993
  1739
  qed
hoelzl@56993
  1740
qed (simp add: f g integrable_density)
hoelzl@56993
  1741
hoelzl@56993
  1742
lemma
hoelzl@56993
  1743
  fixes g :: "'a \<Rightarrow> real"
hoelzl@56993
  1744
  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
hoelzl@56993
  1745
  shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
hoelzl@56993
  1746
    and integrable_real_density: "integrable (density M f) g \<longleftrightarrow> integrable M (\<lambda>x. f x * g x)"
hoelzl@56993
  1747
  using assms integral_density[of g M f] integrable_density[of g M f] by auto
hoelzl@56993
  1748
hoelzl@56993
  1749
lemma has_bochner_integral_density:
hoelzl@56993
  1750
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
hoelzl@56993
  1751
  shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
hoelzl@56993
  1752
    has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
hoelzl@56993
  1753
  by (simp add: has_bochner_integral_iff integrable_density integral_density)
hoelzl@56993
  1754
hoelzl@56993
  1755
subsection {* Distributions *}
hoelzl@56993
  1756
hoelzl@56993
  1757
lemma integrable_distr_eq:
hoelzl@56993
  1758
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1759
  assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
hoelzl@56993
  1760
  shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
hoelzl@56996
  1761
  unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
hoelzl@56993
  1762
hoelzl@56993
  1763
lemma integrable_distr:
hoelzl@56993
  1764
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1765
  shows "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
hoelzl@56993
  1766
  by (subst integrable_distr_eq[symmetric, where g=T])
hoelzl@56993
  1767
     (auto dest: borel_measurable_integrable)
hoelzl@56993
  1768
hoelzl@56993
  1769
lemma integral_distr:
hoelzl@56993
  1770
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1771
  assumes g[measurable]: "g \<in> measurable M N" and f: "f \<in> borel_measurable N"
hoelzl@56993
  1772
  shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\<lambda>x. f (g x))"
hoelzl@56993
  1773
proof (rule integral_eq_cases)
hoelzl@56993
  1774
  assume "integrable (distr M N g) f"
hoelzl@56993
  1775
  then show ?thesis
hoelzl@56993
  1776
  proof induct
hoelzl@56993
  1777
    case (base A c)
hoelzl@56993
  1778
    then have [measurable]: "A \<in> sets N" by auto
hoelzl@56993
  1779
    from base have int: "integrable (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c)"
hoelzl@56993
  1780
      by (intro integrable_indicator)
hoelzl@56993
  1781
  
hoelzl@56993
  1782
    have "integral\<^sup>L (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c) = measure (distr M N g) A *\<^sub>R c"
hoelzl@56993
  1783
      using base by (subst integral_indicator) auto
hoelzl@56993
  1784
    also have "\<dots> = measure M (g -` A \<inter> space M) *\<^sub>R c"
hoelzl@56993
  1785
      by (subst measure_distr) auto
hoelzl@56993
  1786
    also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator (g -` A \<inter> space M) a *\<^sub>R c)"
hoelzl@56993
  1787
      using base by (subst integral_indicator) (auto simp: emeasure_distr)
hoelzl@56993
  1788
    also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator A (g a) *\<^sub>R c)"
hoelzl@56993
  1789
      using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
hoelzl@56993
  1790
    finally show ?case .
hoelzl@56993
  1791
  next
hoelzl@56993
  1792
    case (add f h)
hoelzl@56993
  1793
    then have [measurable]: "f \<in> borel_measurable N" "h \<in> borel_measurable N"
hoelzl@56993
  1794
      by (auto dest!: borel_measurable_integrable)
hoelzl@56993
  1795
    from add g show ?case
hoelzl@56993
  1796
      by (simp add: scaleR_add_right integrable_distr_eq)
hoelzl@56993
  1797
  next
hoelzl@56993
  1798
    case (lim f s)
hoelzl@56993
  1799
    have [measurable]: "f \<in> borel_measurable N" "\<And>i. s i \<in> borel_measurable N"
hoelzl@56993
  1800
      using lim(1,5)[THEN borel_measurable_integrable] by auto
hoelzl@56993
  1801
  
hoelzl@56993
  1802
    show ?case
hoelzl@56993
  1803
    proof (rule LIMSEQ_unique)
hoelzl@56993
  1804
      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
hoelzl@57137
  1805
      proof (rule integral_dominated_convergence)
hoelzl@56993
  1806
        show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
hoelzl@57036
  1807
          using lim by (auto simp: integrable_distr_eq) 
hoelzl@56993
  1808
        show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
hoelzl@56993
  1809
          using lim(3) g[THEN measurable_space] by auto
hoelzl@56993
  1810
        show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
hoelzl@56993
  1811
          using lim(4) g[THEN measurable_space] by auto
hoelzl@56993
  1812
      qed auto
hoelzl@56993
  1813
      show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
hoelzl@56993
  1814
        unfolding lim(2)[symmetric]
hoelzl@57137
  1815
        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
hoelzl@57036
  1816
           (insert lim(3-5), auto)
hoelzl@56993
  1817
    qed
hoelzl@56993
  1818
  qed
hoelzl@56993
  1819
qed (simp add: f g integrable_distr_eq)
hoelzl@56993
  1820
hoelzl@56993
  1821
lemma has_bochner_integral_distr:
hoelzl@56993
  1822
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1823
  shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
hoelzl@56993
  1824
    has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
hoelzl@56993
  1825
  by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
hoelzl@56993
  1826
hoelzl@56994
  1827
subsection {* Lebesgue integration on @{const count_space} *}
hoelzl@56993
  1828
hoelzl@56993
  1829
lemma integrable_count_space:
hoelzl@56993
  1830
  fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
hoelzl@56993
  1831
  shows "finite X \<Longrightarrow> integrable (count_space X) f"
hoelzl@56996
  1832
  by (auto simp: nn_integral_count_space integrable_iff_bounded)
hoelzl@56993
  1833
hoelzl@56993
  1834
lemma measure_count_space[simp]:
hoelzl@56993
  1835
  "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
hoelzl@56993
  1836
  unfolding measure_def by (subst emeasure_count_space ) auto
hoelzl@56993
  1837
hoelzl@56993
  1838
lemma lebesgue_integral_count_space_finite_support:
hoelzl@56993
  1839
  assumes f: "finite {a\<in>A. f a \<noteq> 0}"
hoelzl@56993
  1840
  shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
hoelzl@56993
  1841
proof -
hoelzl@56993
  1842
  have eq: "\<And>x. x \<in> A \<Longrightarrow> (\<Sum>a | x = a \<and> a \<in> A \<and> f a \<noteq> 0. f a) = (\<Sum>x\<in>{x}. f x)"
hoelzl@56993
  1843
    by (intro setsum_mono_zero_cong_left) auto
hoelzl@56993
  1844
    
hoelzl@56993
  1845
  have "(\<integral>x. f x \<partial>count_space A) = (\<integral>x. (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. indicator {a} x *\<^sub>R f a) \<partial>count_space A)"
hoelzl@56993
  1846
    by (intro integral_cong refl) (simp add: f eq)
hoelzl@56993
  1847
  also have "\<dots> = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. measure (count_space A) {a} *\<^sub>R f a)"
hoelzl@56993
  1848
    by (subst integral_setsum) (auto intro!: setsum_cong)
hoelzl@56993
  1849
  finally show ?thesis
hoelzl@56993
  1850
    by auto
hoelzl@56993
  1851
qed
hoelzl@56993
  1852
hoelzl@56993
  1853
lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
hoelzl@56993
  1854
  by (subst lebesgue_integral_count_space_finite_support)
hoelzl@56993
  1855
     (auto intro!: setsum_mono_zero_cong_left)
hoelzl@56993
  1856
hoelzl@56994
  1857
subsection {* Point measure *}
hoelzl@56993
  1858
hoelzl@56993
  1859
lemma lebesgue_integral_point_measure_finite:
hoelzl@56993
  1860
  fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  1861
  shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
hoelzl@56993
  1862
    integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"
hoelzl@56993
  1863
  by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
hoelzl@56993
  1864
hoelzl@56993
  1865
lemma integrable_point_measure_finite:
hoelzl@56993
  1866
  fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and f :: "'a \<Rightarrow> real"
hoelzl@56993
  1867
  shows "finite A \<Longrightarrow> integrable (point_measure A f) g"
hoelzl@56993
  1868
  unfolding point_measure_def
hoelzl@56993
  1869
  apply (subst density_ereal_max_0)
hoelzl@56993
  1870
  apply (subst integrable_density)
hoelzl@56993
  1871
  apply (auto simp: AE_count_space integrable_count_space)
hoelzl@56993
  1872
  done
hoelzl@56993
  1873
hoelzl@56994
  1874
subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
hoelzl@56993
  1875
hoelzl@56993
  1876
lemma real_lebesgue_integral_def:
hoelzl@56993
  1877
  assumes f: "integrable M f"
hoelzl@56993
  1878
  shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
hoelzl@56993
  1879
proof -
hoelzl@56993
  1880
  have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
hoelzl@56993
  1881
    by (auto intro!: arg_cong[where f="integral\<^sup>L M"])
hoelzl@56993
  1882
  also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
hoelzl@56993
  1883
    by (intro integral_diff integrable_max integrable_minus integrable_zero f)
hoelzl@56993
  1884
  also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
hoelzl@57036
  1885
    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
hoelzl@56993
  1886
  also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
hoelzl@57036
  1887
    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
hoelzl@56993
  1888
  also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
hoelzl@56993
  1889
    by (auto simp: max_def)
hoelzl@56993
  1890
  also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
hoelzl@56993
  1891
    by (auto simp: max_def)
hoelzl@56993
  1892
  finally show ?thesis
hoelzl@56996
  1893
    unfolding nn_integral_max_0 .
hoelzl@56993
  1894
qed
hoelzl@56993
  1895
hoelzl@56993
  1896
lemma real_integrable_def:
hoelzl@56993
  1897
  "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
hoelzl@56993
  1898
    (\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
hoelzl@56993
  1899
  unfolding integrable_iff_bounded
hoelzl@56993
  1900
proof (safe del: notI)
hoelzl@56993
  1901
  assume *: "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
hoelzl@56993
  1902
  have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1903
    by (intro nn_integral_mono) auto
hoelzl@56993
  1904
  also note *
hoelzl@56993
  1905
  finally show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
hoelzl@56993
  1906
    by simp
hoelzl@56993
  1907
  have "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
hoelzl@56996
  1908
    by (intro nn_integral_mono) auto
hoelzl@56993
  1909
  also note *
hoelzl@56993
  1910
  finally show "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
hoelzl@56993
  1911
    by simp
hoelzl@56993
  1912
next
hoelzl@56993
  1913
  assume [measurable]: "f \<in> borel_measurable M"
hoelzl@56993
  1914
  assume fin: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
hoelzl@56993
  1915
  have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) + max 0 (ereal (- f x)) \<partial>M)"
hoelzl@56996
  1916
    by (intro nn_integral_cong) (auto simp: max_def)
hoelzl@56993
  1917
  also have"\<dots> = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (ereal (- f x)) \<partial>M)"
hoelzl@56996
  1918
    by (intro nn_integral_add) auto
hoelzl@56993
  1919
  also have "\<dots> < \<infinity>"
hoelzl@56996
  1920
    using fin by (auto simp: nn_integral_max_0)
hoelzl@56993
  1921
  finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
hoelzl@56993
  1922
qed
hoelzl@56993
  1923
hoelzl@56993
  1924
lemma integrableD[dest]:
hoelzl@56993
  1925
  assumes "integrable M f"
hoelzl@56993
  1926
  shows "f \<in> borel_measurable M" "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
hoelzl@56993
  1927
  using assms unfolding real_integrable_def by auto
hoelzl@56993
  1928
hoelzl@56993
  1929
lemma integrableE:
hoelzl@56993
  1930
  assumes "integrable M f"
hoelzl@56993
  1931
  obtains r q where
hoelzl@56993
  1932
    "(\<integral>\<^sup>+x. ereal (f x)\<partial>M) = ereal r"
hoelzl@56993
  1933
    "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M) = ereal q"
hoelzl@56993
  1934
    "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
hoelzl@56993
  1935
  using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
hoelzl@56996
  1936
  using nn_integral_nonneg[of M "\<lambda>x. ereal (f x)"]
hoelzl@56996
  1937
  using nn_integral_nonneg[of M "\<lambda>x. ereal (-f x)"]
hoelzl@56993
  1938
  by (cases rule: ereal2_cases[of "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ereal (f x)\<partial>M)"]) auto
hoelzl@56993
  1939
hoelzl@56993
  1940
lemma integral_monotone_convergence_nonneg:
hoelzl@56993
  1941
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
hoelzl@56993
  1942
  assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
hoelzl@56993
  1943
    and pos: "\<And>i. AE x in M. 0 \<le> f i x"
hoelzl@56993
  1944
    and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
hoelzl@56993
  1945
    and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
hoelzl@56993
  1946
    and u: "u \<in> borel_measurable M"
hoelzl@56993
  1947
  shows "integrable M u"
hoelzl@56993
  1948
  and "integral\<^sup>L M u = x"
hoelzl@56993
  1949
proof -
hoelzl@56993
  1950
  have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ereal (f n x) \<partial>M))"
hoelzl@56996
  1951
  proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
hoelzl@56993
  1952
    fix i
hoelzl@56993
  1953
    from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
hoelzl@56993
  1954
      by eventually_elim (auto simp: mono_def)
hoelzl@56993
  1955
    show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
hoelzl@56993
  1956
      using i by auto
hoelzl@56993
  1957
  next
hoelzl@56993
  1958
    show "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ereal (f i x)) \<partial>M"
hoelzl@56996
  1959
      apply (rule nn_integral_cong_AE)
hoelzl@56993
  1960
      using lim mono
hoelzl@56993
  1961
      by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
hoelzl@56993
  1962
  qed
hoelzl@56993
  1963
  also have "\<dots> = ereal x"
hoelzl@56996
  1964
    using mono i unfolding nn_integral_eq_integral[OF i pos]
hoelzl@56993
  1965
    by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
hoelzl@56993
  1966
  finally have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = ereal x" .
hoelzl@56993
  1967
  moreover have "(\<integral>\<^sup>+ x. ereal (- u x) \<partial>M) = 0"
hoelzl@56996
  1968
  proof (subst nn_integral_0_iff_AE)
hoelzl@56993
  1969
    show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
hoelzl@56993
  1970
      using u by auto
hoelzl@56993
  1971
    from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
hoelzl@56993
  1972
    proof eventually_elim
hoelzl@56993
  1973
      fix x assume "mono (\<lambda>n. f n x)" "0 \<le> f 0 x" "(\<lambda>i. f i x) ----> u x"
hoelzl@56993
  1974
      then show "ereal (- u x) \<le> 0"
hoelzl@56993
  1975
        using incseq_le[of "\<lambda>n. f n x" "u x" 0] by (simp add: mono_def incseq_def)
hoelzl@56993
  1976
    qed
hoelzl@56993
  1977
  qed
hoelzl@56993
  1978
  ultimately show "integrable M u" "integral\<^sup>L M u = x"
hoelzl@56993
  1979
    by (auto simp: real_integrable_def real_lebesgue_integral_def u)
hoelzl@56993
  1980
qed
hoelzl@56993
  1981
hoelzl@56993
  1982
lemma
hoelzl@56993
  1983
  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
hoelzl@56993
  1984
  assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
hoelzl@56993
  1985
  and lim: "AE x in M. (\<lambda>i. f i x) ----> u x"
hoelzl@56993
  1986
  and ilim: "(\<lambda>i. integral\<^sup>L M (f i)) ----> x"
hoelzl@56993
  1987
  and u: "u \<in> borel_measurable M"
hoelzl@56993
  1988
  shows integrable_monotone_convergence: "integrable M u"
hoelzl@56993
  1989
    and integral_monotone_convergence: "integral\<^sup>L M u = x"
hoelzl@56993
  1990
    and has_bochner_integral_monotone_convergence: "has_bochner_integral M u x"
hoelzl@56993
  1991
proof -
hoelzl@56993
  1992
  have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
hoelzl@56993
  1993
    using f by auto
hoelzl@56993
  1994
  have 2: "AE x in M. mono (\<lambda>n. f n x - f 0 x)"
hoelzl@56993
  1995
    using mono by (auto simp: mono_def le_fun_def)
hoelzl@56993
  1996
  have 3: "\<And>n. AE x in M. 0 \<le> f n x - f 0 x"
hoelzl@56993
  1997
    using mono by (auto simp: field_simps mono_def le_fun_def)
hoelzl@56993
  1998
  have 4: "AE x in M. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
hoelzl@56993
  1999
    using lim by (auto intro!: tendsto_diff)
hoelzl@56993
  2000
  have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^sup>L M (f 0)"
hoelzl@56993
  2001
    using f ilim by (auto intro!: tendsto_diff)
hoelzl@56993
  2002
  have 6: "(\<lambda>x. u x - f 0 x) \<in> borel_measurable M"
hoelzl@56993
  2003
    using f[of 0] u by auto
hoelzl@56993
  2004
  note diff = integral_monotone_convergence_nonneg[OF 1 2 3 4 5 6]
hoelzl@56993
  2005
  have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
hoelzl@56993
  2006
    using diff(1) f by (rule integrable_add)
hoelzl@56993
  2007
  with diff(2) f show "integrable M u" "integral\<^sup>L M u = x"
hoelzl@56993
  2008
    by auto
hoelzl@56993
  2009
  then show "has_bochner_integral M u x"
hoelzl@56993
  2010
    by (metis has_bochner_integral_integrable)
hoelzl@56993
  2011
qed
hoelzl@56993
  2012
hoelzl@56993
  2013
lemma integral_norm_eq_0_iff:
hoelzl@56993
  2014
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@56993
  2015
  assumes f[measurable]: "integrable M f"
hoelzl@56993
  2016
  shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"