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