Quelle Bochner_Integration.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Bochner_Integration.thy
    Author:     Johannes Hölzl, TU München
*)

section \<open>Bochner Integration for Vector-Valued Functions\<close>

theory Bochner_Integration
  imports Finite_Product_Measure
begin

text \<open>

In the following development of the Bochner integral we use second countable topologies instead
of separable spaces. A second countable topology is also separable.

\<close>

proposition borel_measurable_implies_sequence_metric:
  fixes f :: "'a \ 'b :: {metric_space, second_countable_topology}"
  assumes [measurable]: "f \ borel_measurable M"
  shows "\F. (\i. simple_function M (F i)) \ (\x\space M. (\i. F i x) \ f x) \
    (\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
proof -
  obtain D :: "'b set" where "countable D" and D: "\X. open X \ X \ {} \ \d\D. d \ X"
    by (erule countable_dense_setE)

  define e where "e = from_nat_into D"
  { fix n x
    obtain d where "d \ D" and d: "d \ ball x (1 / Suc n)"
      using D[of "ball x (1 / Suc n)"] by auto
    from \<open>d \<in> D\<close> D[of UNIV] \<open>countable D\<close> obtain i where "d = e i"
      unfolding e_def by (auto dest: from_nat_into_surj)
    with d have "\i. dist x (e i) < 1 / Suc n"
      by auto }
  note e = this

  define A where [abs_def]: "A m n =
    {x\<in>space M. dist (f x) (e n) < 1 / (Suc m) \<and> 1 / (Suc m) \<le> dist (f x) z}" for m n
  define B where [abs_def]: "B m = disjointed (A m)" for m

  define m where [abs_def]: "m N x = Max {m. m \ N \ x \ (\n\N. B m n)}" for N x
  define F where [abs_def]: "F N x =
    (if (\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)) \<and> (\<exists>n\<le>N. x \<in> B (m N x) n)
     then e (LEAST n. x \<in> B (m N x) n) else z)" for N x

  have B_imp_A[intro, simp]: "\x m n. x \ B m n \ x \ A m n"
    using disjointed_subset[of "A m" for m] unfolding B_def by auto

  { fix m
    have "\n. A m n \ sets M"
      by (auto simp: A_def)
    then have "\n. B m n \ sets M"
      using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) }
  note this[measurable]

  { fix N i x assume "\m\N. x \ (\n\N. B m n)"
    then have "m N x \ {m::nat. m \ N \ x \ (\n\N. B m n)}"
      unfolding m_def by (intro Max_in) auto
    then have "m N x \ N" "\n\N. x \ B (m N x) n"
      by auto }
  note m = this

  { fix j N i x assume "j \ N" "i \ N" "x \ B j i"
    then have "j \ m N x"
      unfolding m_def by (intro Max_ge) auto }
  note m_upper = this

  show ?thesis
    unfolding simple_function_def
  proof (safe intro!: exI[of _ F])
    have [measurable]: "\i. F i \ borel_measurable M"
      unfolding F_def m_def by measurable
    show "\x i. F i -` {x} \ space M \ sets M"
      by measurable

    { fix i
      { fix n x assume "x \ B (m i x) n"
        then have "(LEAST n. x \ B (m i x) n) \ n"
          by (intro Least_le)
        also assume "n \ i"
        finally have "(LEAST n. x \ B (m i x) n) \ i" . }
      then have "F i ` space M \ {z} \ e ` {.. i}"
        by (auto simp: F_def)
      then show "finite (F i ` space M)"
        by (rule finite_subset) auto }

    { fix N i n x assume "i \ N" "n \ N" "x \ B i n"
      then have 1: "\m\N. x \ (\n\N. B m n)" by auto
      from m[OF this] obtain n where n: "m N x \ N" "n \ N" "x \ B (m N x) n" by auto
      moreover
      define L where "L = (LEAST n. x \ B (m N x) n)"
      have "dist (f x) (e L) < 1 / Suc (m N x)"
      proof -
        have "x \ B (m N x) L"
          using n(3) unfolding L_def by (rule LeastI)
        then have "x \ A (m N x) L"
          by auto
        then show ?thesis
          unfolding A_def by simp
      qed
      ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)"
        by (auto simp: F_def L_def) }
    note * = this

    fix x assume "x \ space M"
    show "(\i. F i x) \ f x"
    proof (cases "f x = z")
      case True
      then have "\i n. x \ A i n"
        unfolding A_def by auto
      then show ?thesis
        by (metis B_imp_A F_def LIMSEQ_def True dist_self)
    next
      case False
      show ?thesis
      proof (rule tendstoI)
        fix e :: real assume "0 < e"
        with \<open>f x \<noteq> z\<close> obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z"
          by (metis dist_nz order_less_trans neq_iff nat_approx_posE)
        with \<open>x\<in>space M\<close> \<open>f x \<noteq> z\<close> have "x \<in> (\<Union>i. B n i)"
          unfolding A_def B_def UN_disjointed_eq using e by auto
        then obtain i where i: "x \ B n i" by auto

        show "eventually (\i. dist (F i x) (f x) < e) sequentially"
          using eventually_ge_at_top[of "max n i"]
        proof eventually_elim
          fix j assume j: "max n i \ j"
          with i have "dist (f x) (F j x) < 1 / Suc (m j x)"
            by (intro *[OF _ _ i]) auto
          also have "\ \ 1 / Suc n"
            using j m_upper[OF _ _ i]
            by (auto simp: field_simps)
          also note \<open>1 / Suc n < e\<close>
          finally show "dist (F j x) (f x) < e"
            by (simp add: less_imp_le dist_commute)
        qed
      qed
    qed
    fix i
    { fix n m assume "x \ A n m"
      then have "dist (e m) (f x) + dist (f x) z \ 2 * dist (f x) z"
        unfolding A_def by (auto simp: dist_commute)
      also have "dist (e m) z \ dist (e m) (f x) + dist (f x) z"
        by (rule dist_triangle)
      finally (xtrans) have "dist (e m) z \ 2 * dist (f x) z" . }
    then show "dist (F i x) z \ 2 * dist (f x) z"
      unfolding F_def
      by (smt (verit, ccfv_threshold) LeastI2 B_imp_A dist_eq_0_iff zero_le_dist)
  qed
qed

lemma
  fixes f :: "'a \ 'b::semiring_1" assumes "finite A"
  shows sum_mult_indicator[simp]: "(\x \ A. f x * indicator (B x) (g x)) = (\x\{x\A. g x \ B x}. f x)"
  and sum_indicator_mult[simp]: "(\x \ A. indicator (B x) (g x) * f x) = (\x\{x\A. g x \ B x}. f x)"
  unfolding indicator_def
  using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)

lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
  fixes P :: "('a \ real) \ bool"
  assumes u: "u \ borel_measurable M" "\x. 0 \ u x"
  assumes set: "\A. A \ sets M \ P (indicator A)"
  assumes mult: "\u c. 0 \ c \ u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ P (\x. c * u x)"
  assumes add: "\u v. u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ v \ borel_measurable M \ (\x. 0 \ v x) \ (\x. x \ space M \ u x = 0 \ v x = 0) \ P v \ P (\x. v x + u x)"
  assumes seq: "\U. (\i. U i \ borel_measurable M) \ (\i x. 0 \ U i x) \ (\i. P (U i)) \ incseq U \ (\x. x \ space M \ (\i. U i x) \ u x) \ P u"
  shows "P u"
proof -
  have "(\x. ennreal (u x)) \ borel_measurable M" using u by auto
  from borel_measurable_implies_simple_function_sequence'[OF this]
  obtain U where U: "\i. simple_function M (U i)" "incseq U" "\i x. U i x < top" and
    sup: "\x. (SUP i. U i x) = ennreal (u x)"
    by blast

  define U' where [abs_def]: "U' i x = indicator (space M) x * enn2real (U i x)" for i x
  then have U'_sf[measurable]: "\i. simple_function M (U' i)"
    using U by (auto intro!: simple_function_compose1[where g=enn2real])

  show "P u"
  proof (rule seq)
    show U': "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x" for i
      using U'_sf by (auto simp: U'_def borel_measurable_simple_function)
    show "incseq U'"
      using U(2,3)
      by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)

    fix x assume x: "x \ space M"
    have "(\i. U i x) \ (SUP i. U i x)"
      using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def)
    moreover have "(\i. U i x) = (\i. ennreal (U' i x))"
      using x U(3) by (auto simp: fun_eq_iff U'_def image_iff eq_commute)
    moreover have "(SUP i. U i x) = ennreal (u x)"
      using sup u(2) by (simp add: max_def)
    ultimately show "(\i. U' i x) \ u x"
      using u U' by simp
  next
    fix i
    have "U' i ` space M \ enn2real ` (U i ` space M)" "finite (U i ` space M)"
      unfolding U'_def using U(1) by (auto dest: simple_functionD)
    then have fin: "finite (U' i ` space M)"
      by (metis finite_subset finite_imageI)
    moreover have "\z. {y. U' i z = y \ y \ U' i ` space M \ z \ space M} = (if z \ space M then {U' i z} else {})"
      by auto
    ultimately have U': "(\z. \y\U' i`space M. y * indicator {x\space M. U' i x = y} z) = U' i"
      by (simp add: U'_def fun_eq_iff)
    have "\x. x \ U' i ` space M \ 0 \ x"
      by (auto simp: U'_def)
    with fin have "P (\z. \y\U' i`space M. y * indicator {x\space M. U' i x = y} z)"
    proof induct
      case empty from set[of "{}"] show ?case
        by (simp add: indicator_def[abs_def])
    next
      case (insert x F)
      from insert.prems have nonneg: "x \ 0" "\y. y \ F \ y \ 0"
        by simp_all
      hence *: "P (\xa. x * indicat_real {x' \ space M. U' i x' = x} xa)"
        by (intro mult set) auto
      have "P (\z. x * indicat_real {x' \ space M. U' i x' = x} z +
                   (\<Sum>y\<in>F. y * indicat_real {x \<in> space M. U' i x = y} z))"
        using insert(1-3)
        by (intro add * sum_nonneg mult_nonneg_nonneg)
           (auto simp: nonneg indicator_def of_bool_def sum_nonneg_eq_0_iff)
      thus ?case
        using insert.hyps by (subst sum.insert) auto
    qed
    with U' show "P (U' i)" by simp
  qed
qed

lemma scaleR_cong_right:
  fixes x :: "'a :: real_vector"
  shows "(x \ 0 \ r = p) \ r *\<^sub>R x = p *\<^sub>R x"
  by auto

inductive simple_bochner_integrable :: "'a measure \ ('a \ 'b::real_vector) \ bool" for M f where
  "simple_function M f \ emeasure M {y\space M. f y \ 0} \ \ \
    simple_bochner_integrable M f"

lemma simple_bochner_integrable_compose2:
  assumes p_0: "p 0 0 = 0"
  shows "simple_bochner_integrable M f \ simple_bochner_integrable M g \
    simple_bochner_integrable M (\<lambda>x. p (f x) (g x))"
proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI)
  assume sf: "simple_function M f" "simple_function M g"
  then show "simple_function M (\x. p (f x) (g x))"
    by (rule simple_function_compose2)

  from sf have [measurable]:
      "f \ measurable M (count_space UNIV)"
      "g \ measurable M (count_space UNIV)"
    by (auto intro: measurable_simple_function)

  assume fin: "emeasure M {y \ space M. f y \ 0} \ \" "emeasure M {y \ space M. g y \ 0} \ \"

  have "emeasure M {x\space M. p (f x) (g x) \ 0} \
      emeasure M ({x\<in>space M. f x \<noteq> 0} \<union> {x\<in>space M. g x \<noteq> 0})"
    by (intro emeasure_mono) (auto simp: p_0)
  also have "\ \ emeasure M {x\space M. f x \ 0} + emeasure M {x\space M. g x \ 0}"
    by (intro emeasure_subadditive) auto
  finally show "emeasure M {y \ space M. p (f y) (g y) \ 0} \ \"
    using fin by (auto simp: top_unique)
qed

lemma simple_function_finite_support:
  assumes f: "simple_function M f" and fin: "(\\<^sup>+x. f x \M) < \" and nn: "\x. 0 \ f x"
  shows "emeasure M {x\space M. f x \ 0} \ \"
proof cases
  from f have meas[measurable]: "f \ borel_measurable M"
    by (rule borel_measurable_simple_function)

  assume non_empty: "\x\space M. f x \ 0"

  define m where "m = Min (f`space M - {0})"
  have "m \ f`space M - {0}"
    unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def)
  then have m: "0 < m"
    using nn by (auto simp: less_le)

  from m have "m * emeasure M {x\space M. 0 \ f x} =
    (\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
  also have "\ \ (\\<^sup>+x. f x \M)"
    using AE_space
  proof (intro nn_integral_mono_AE, eventually_elim)
    fix x assume "x \ space M"
    with nn show "m * indicator {x \ space M. 0 \ f x} x \ f x"
      using f by (auto split: split_indicator simp: simple_function_def m_def)
  qed
  also note \<open>\<dots> < \<infinity>\<close>
  finally show ?thesis
    using m by (auto simp: ennreal_mult_less_top)
next
  assume "\ (\x\space M. f x \ 0)"
  with nn have *: "{x\space M. f x \ 0} = {}"
    by auto
  show ?thesis unfolding * by simp
qed

lemma simple_bochner_integrableI_bounded:
  assumes f: "simple_function M f" and fin: "(\\<^sup>+x. norm (f x) \M) < \"
  shows "simple_bochner_integrable M f"
proof
  have "emeasure M {y \ space M. ennreal (norm (f y)) \ 0} \ \"
    using simple_function_finite_support simple_function_compose1 f fin by force
  then show "emeasure M {y \ space M. f y \ 0} \ \" by simp
qed fact

definition\<^marker>\<open>tag important\<close> simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
  "simple_bochner_integral M f = (\y\f`space M. measure M {x\space M. f x = y} *\<^sub>R y)"

proposition simple_bochner_integral_partition:
  assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
  assumes sub: "\x y. x \ space M \ y \ space M \ g x = g y \ f x = f y"
  assumes v: "\x. x \ space M \ f x = v (g x)"
  shows "simple_bochner_integral M f = (\y\g ` space M. measure M {x\space M. g x = y} *\<^sub>R v y)"
    (is "_ = ?r")
proof -
  from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
    by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)

  from f have [measurable]: "f \ measurable M (count_space UNIV)"
    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)

  from g have [measurable]: "g \ measurable M (count_space UNIV)"
    by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases)

  { fix y assume "y \ space M"
    then have "f ` space M \ {i. \x\space M. i = f x \ g y = g x} = {v (g y)}"
      by (auto cong: sub simp: v[symmetric]) }
  note eq = this

  have "simple_bochner_integral M f =
    (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M.
      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)"
    unfolding simple_bochner_integral_def
  proof (safe intro!: sum.cong scaleR_cong_right)
    fix y assume y: "y \ space M" "f y \ 0"
    have [simp]: "g ` space M \ {z. \x\space M. f y = f x \ z = g x} =
        {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
      by auto
    have eq:"{x \ space M. f x = f y} =
        (\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i})"
      by (auto simp: eq_commute cong: sub rev_conj_cong)
    have "finite (g`space M)" by simp
    then have "finite {z. \x\space M. f y = f x \ z = g x}"
      by (rule rev_finite_subset) auto
    moreover
    { fix x assume "x \ space M" "f x = f y"
      then have "x \ space M" "f x \ 0"
        using y by auto
      then have "emeasure M {y \ space M. g y = g x} \ emeasure M {y \ space M. f y \ 0}"
        by (auto intro!: emeasure_mono cong: sub)
      then have "emeasure M {xa \ space M. g xa = g x} < \"
        using f by (auto simp: simple_bochner_integrable.simps less_top) }
    ultimately
    show "measure M {x \ space M. f x = f y} =
      (\<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)"
      apply (simp add: sum.If_cases eq)
      apply (subst measure_finite_Union[symmetric])
      apply (auto simp: disjoint_family_on_def less_top)
      done
  qed
  also have "\ = (\y\f`space M. (\z\g`space M.
      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))"
    by (auto intro!: sum.cong simp: scaleR_sum_left)
  also have "\ = ?r"
    by (subst sum.swap)
       (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
  finally show "simple_bochner_integral M f = ?r" .
qed

lemma simple_bochner_integral_add:
  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
  shows "simple_bochner_integral M (\x. f x + g x) =
    simple_bochner_integral M f + simple_bochner_integral M g"
proof -
  from f g have "simple_bochner_integral M (\x. f x + g x) =
    (\<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))"
    by (intro simple_bochner_integral_partition)
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
  moreover from f g have "simple_bochner_integral M f =
    (\<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)"
    by (intro simple_bochner_integral_partition)
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
  moreover from f g have "simple_bochner_integral M g =
    (\<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)"
    by (intro simple_bochner_integral_partition)
       (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
  ultimately show ?thesis
    by (simp add: sum.distrib[symmetric] scaleR_add_right)
qed

lemma simple_bochner_integral_linear:
  assumes "linear f"
  assumes g: "simple_bochner_integrable M g"
  shows "simple_bochner_integral M (\x. f (g x)) = f (simple_bochner_integral M g)"
proof -
  interpret linear f by fact
  from g have "simple_bochner_integral M (\x. f (g x)) =
    (\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)"
    by (intro simple_bochner_integral_partition)
       (auto simp: simple_bochner_integrable_compose2[where p="\x y. f x"]
             elim: simple_bochner_integrable.cases)
  also have "\ = f (simple_bochner_integral M g)"
    by (simp add: simple_bochner_integral_def sum scale)
  finally show ?thesis .
qed

lemma simple_bochner_integral_minus:
  assumes f: "simple_bochner_integrable M f"
  shows "simple_bochner_integral M (\x. - f x) = - simple_bochner_integral M f"
proof -
  from linear_uminus f show ?thesis
    by (rule simple_bochner_integral_linear)
qed

lemma simple_bochner_integral_diff:
  assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g"
  shows "simple_bochner_integral M (\x. f x - g x) =
    simple_bochner_integral M f - simple_bochner_integral M g"
  unfolding diff_conv_add_uminus using f g
  by (subst simple_bochner_integral_add)
     (auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="\x y. - y"])

lemma simple_bochner_integral_norm_bound:
  assumes f: "simple_bochner_integrable M f"
  shows "norm (simple_bochner_integral M f) \ simple_bochner_integral M (\x. norm (f x))"
proof -
  have "norm (simple_bochner_integral M f) \
    (\<Sum>y\<in>f ` space M. norm (measure M {x \<in> space M. f x = y} *\<^sub>R y))"
    unfolding simple_bochner_integral_def by (rule norm_sum)
  also have "\ = (\y\f ` space M. measure M {x \ space M. f x = y} *\<^sub>R norm y)"
    by simp
  also have "\ = simple_bochner_integral M (\x. norm (f x))"
    using f
    by (intro simple_bochner_integral_partition[symmetric])
       (auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases)
  finally show ?thesis .
qed

lemma simple_bochner_integral_nonneg[simp]:
  fixes f :: "'a \ real"
  shows "(\x. 0 \ f x) \ 0 \ simple_bochner_integral M f"
  by (force simp: simple_bochner_integral_def intro: sum_nonneg)

lemma simple_bochner_integral_eq_nn_integral:
  assumes f: "simple_bochner_integrable M f" "\x. 0 \ f x"
  shows "simple_bochner_integral M f = (\\<^sup>+x. f x \M)"
proof -
  have ennreal_cong_mult: "(x \ 0 \ y = z) \ ennreal x * y = ennreal x * z" for x y z
      by fastforce

  have [measurable]: "f \ borel_measurable M"
    by (meson borel_measurable_simple_function f(1) simple_bochner_integrable.cases)

  { fix y assume y: "y \ space M" "f y \ 0"
    have "ennreal (measure M {x \ space M. f x = f y}) = emeasure M {x \ space M. f x = f y}"
    proof (rule emeasure_eq_ennreal_measure[symmetric])
      have "emeasure M {x \ space M. f x = f y} \ emeasure M {x \ space M. f x \ 0}"
        using y by (intro emeasure_mono) auto
      with f show "emeasure M {x \ space M. f x = f y} \ top"
        by (auto simp: simple_bochner_integrable.simps top_unique)
    qed
    moreover have "{x \ space M. f x = f y} = (\x. ennreal (f x)) -` {ennreal (f y)} \ space M"
      using f by auto
    ultimately have "ennreal (measure M {x \ space M. f x = f y}) =
          emeasure M ((\<lambda>x. ennreal (f x)) -` {ennreal (f y)} \<inter> space M)" by simp }
  with f have "simple_bochner_integral M f = (\\<^sup>Sx. f x \M)"
    unfolding simple_integral_def
    by (subst simple_bochner_integral_partition[OF f(1), where g="\x. ennreal (f x)" and v=enn2real])
       (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
             intro!: sum.cong ennreal_cong_mult
             simp: ac_simps ennreal_mult
             simp flip: sum_ennreal)
  also have "\ = (\\<^sup>+x. f x \M)"
    using f
    by (metis nn_integral_eq_simple_integral simple_bochner_integrable.cases simple_function_compose1)
  finally show ?thesis .
qed

lemma simple_bochner_integral_bounded:
  fixes f :: "'a \ 'b::{real_normed_vector, second_countable_topology}"
  assumes f[measurable]: "f \ borel_measurable M"
  assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
  shows "ennreal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \
    (\<integral>\<^sup>+ x. norm (f x - s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x - t x) \<partial>M)"
    (is "ennreal (norm (?s - ?t)) \ ?S + ?T")
proof -
  have [measurable]: "s \ borel_measurable M" "t \ borel_measurable M"
    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)

  have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\x. s x - t x))"
    using s t by (subst simple_bochner_integral_diff) auto
  also have "\ \ simple_bochner_integral M (\x. norm (s x - t x))"
    using simple_bochner_integrable_compose2[of "(-)" M "s" "t"] s t
    by (auto intro!: simple_bochner_integral_norm_bound)
  also have "\ = (\\<^sup>+x. norm (s x - t x) \M)"
    using simple_bochner_integrable_compose2[of "\x y. norm (x - y)" M "s" "t"] s t
    by (auto intro!: simple_bochner_integral_eq_nn_integral)
  also have "\ \ (\\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \M)"
  proof -
    have "\x. x \ space M \
         norm (s x - t x) \<le> norm (f x - s x) + norm (f x - t x)"
      by (metis dual_order.refl norm_diff_triangle_le norm_minus_commute)
    then show ?thesis
      by (metis (mono_tags, lifting) ennreal_leI ennreal_plus nn_integral_mono norm_ge_zero)
  qed
  also have "\ = ?S + ?T"
   by (rule nn_integral_add) auto
  finally show ?thesis .
qed

inductive has_bochner_integral :: "'a measure \ ('a \ 'b) \ 'b::{real_normed_vector, second_countable_topology} \ bool"
  for M f x where
  "f \ borel_measurable M \
    (\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow>
    (\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0 \<Longrightarrow>
    (\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x \<Longrightarrow>
    has_bochner_integral M f x"

lemma has_bochner_integral_cong:
  assumes "M = N" "\x. x \ space N \ f x = g x" "x = y"
  shows "has_bochner_integral M f x \ has_bochner_integral N g y"
  unfolding has_bochner_integral.simps assms(1,3)
  using assms(2) by (simp cong: measurable_cong_simp nn_integral_cong_simp)

lemma has_bochner_integral_cong_AE:
  "f \ borel_measurable M \ g \ borel_measurable M \ (AE x in M. f x = g x) \
    has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
  unfolding has_bochner_integral.simps
  by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\x. x \ 0"]
            nn_integral_cong_AE)
     auto

lemma borel_measurable_has_bochner_integral:
  "has_bochner_integral M f x \ f \ borel_measurable M"
  by (rule has_bochner_integral.cases)

lemma borel_measurable_has_bochner_integral'[measurable_dest]:
  "has_bochner_integral M f x \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N"
  using borel_measurable_has_bochner_integral[measurable] by measurable

lemma has_bochner_integral_simple_bochner_integrable:
  "simple_bochner_integrable M f \ has_bochner_integral M f (simple_bochner_integral M f)"
  by (rule has_bochner_integral.intros[where s="\_. f"])
     (auto intro: borel_measurable_simple_function
           elim: simple_bochner_integrable.cases
           simp flip: zero_ennreal_def)

lemma has_bochner_integral_real_indicator:
  assumes [measurable]: "A \ sets M" and A: "emeasure M A < \"
  shows "has_bochner_integral M (indicator A) (measure M A)"
proof -
  have sbi: "simple_bochner_integrable M (indicator A::'a \ real)"
  proof
    have "{y \ space M. (indicator A y::real) \ 0} = A"
      using sets.sets_into_space[OF \<open>A\<in>sets M\<close>] by (auto split: split_indicator)
    then show "emeasure M {y \ space M. (indicator A y::real) \ 0} \ \"
      using A by auto
  qed (rule simple_function_indicator assms)+
  moreover have "simple_bochner_integral M (indicator A) = measure M A"
    using simple_bochner_integral_eq_nn_integral[OF sbi] A
    by (simp add: ennreal_indicator emeasure_eq_ennreal_measure)
  ultimately show ?thesis
    by (metis has_bochner_integral_simple_bochner_integrable)
qed

lemma has_bochner_integral_add[intro]:
  "has_bochner_integral M f x \ has_bochner_integral M g y \
    has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
  fix sf sg
  assume f_sf: "(\i. \\<^sup>+ x. norm (f x - sf i x) \M) \ 0"
  assume g_sg: "(\i. \\<^sup>+ x. norm (g x - sg i x) \M) \ 0"

  assume sf: "\i. simple_bochner_integrable M (sf i)"
    and sg: "\i. simple_bochner_integrable M (sg i)"
  then have [measurable]: "\i. sf i \ borel_measurable M" "\i. sg i \ borel_measurable M"
    by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
  assume [measurable]: "f \ borel_measurable M" "g \ borel_measurable M"

  show "\i. simple_bochner_integrable M (\x. sf i x + sg i x)"
    using sf sg by (simp add: simple_bochner_integrable_compose2)

  show "(\i. \\<^sup>+ x. (norm (f x + g x - (sf i x + sg i x))) \M) \ 0"
    (is "?f \ 0")
  proof (rule tendsto_sandwich)
    show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) \ 0"
      by auto
    show "eventually (\i. ?f i \ (\\<^sup>+ x. (norm (f x - sf i x)) \M) + \\<^sup>+ x. (norm (g x - sg i x)) \M) sequentially"
      (is "eventually (\i. ?f i \ ?g i) sequentially")
    proof (intro always_eventually allI)
      fix i have "?f i \ (\\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \M)"
        by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
                 simp flip: ennreal_plus)
      also have "\ = ?g i"
        by (intro nn_integral_add) auto
      finally show "?f i \ ?g i" .
    qed
    show "?g \ 0"
      using tendsto_add[OF f_sf g_sg] by simp
  qed
qed (auto simp: simple_bochner_integral_add tendsto_add)

lemma has_bochner_integral_bounded_linear:
  assumes "bounded_linear T"
  shows "has_bochner_integral M f x \ has_bochner_integral M (\x. T (f x)) (T x)"
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
  interpret T: bounded_linear T by fact
  have [measurable]: "T \ borel_measurable borel"
    by (intro borel_measurable_continuous_onI T.continuous_on continuous_on_id)
  assume [measurable]: "f \ borel_measurable M"
  then show "(\x. T (f x)) \ borel_measurable M"
    by auto

  fix s assume f_s: "(\i. \\<^sup>+ x. norm (f x - s i x) \M) \ 0"
  assume s: "\i. simple_bochner_integrable M (s i)"
  then show "\i. simple_bochner_integrable M (\x. T (s i x))"
    by (auto intro: simple_bochner_integrable_compose2 T.zero)

  have [measurable]: "\i. s i \ borel_measurable M"
    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)

  obtain K where K: "K > 0" "\x i. norm (T (f x) - T (s i x)) \ norm (f x - s i x) * K"
    using T.pos_bounded by (auto simp: T.diff[symmetric])

  show "(\i. \\<^sup>+ x. norm (T (f x) - T (s i x)) \M) \ 0"
    (is "?f \ 0")
  proof (rule tendsto_sandwich)
    show "eventually (\n. 0 \ ?f n) sequentially" "(\_. 0) \ 0"
      by auto

    show "eventually (\i. ?f i \ K * (\\<^sup>+ x. norm (f x - s i x) \M)) sequentially"
      (is "eventually (\i. ?f i \ ?g i) sequentially")
    proof (intro always_eventually allI)
      fix i have "?f i \ (\\<^sup>+ x. ennreal K * norm (f x - s i x) \M)"
        using K by (intro nn_integral_mono) (auto simp: ac_simps ennreal_mult[symmetric])
      also have "\ = ?g i"
        using K by (intro nn_integral_cmult) auto
      finally show "?f i \ ?g i" .
    qed
    show "?g \ 0"
      using ennreal_tendsto_cmult[OF _ f_s] by simp
  qed

  assume "(\i. simple_bochner_integral M (s i)) \ x"
  with s show "(\i. simple_bochner_integral M (\x. T (s i x))) \ T x"
    by (auto intro!: T.tendsto simp: simple_bochner_integral_linear T.linear_axioms)
qed

lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\x. 0) 0"
  by (auto intro!: has_bochner_integral.intros[where s="\_ _. 0"]
           simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps
                 simple_bochner_integral_def image_constant_conv)

lemma has_bochner_integral_scaleR_left[intro]:
  "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x *\<^sub>R c) (x *\<^sub>R c)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])

lemma has_bochner_integral_scaleR_right[intro]:
  "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c *\<^sub>R f x) (c *\<^sub>R x)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])

lemma has_bochner_integral_mult_left[intro]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x * c) (x * c)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])

lemma has_bochner_integral_mult_right[intro]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c * f x) (c * x)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])

lemmas has_bochner_integral_divide =
  has_bochner_integral_bounded_linear[OF bounded_linear_divide]

lemma has_bochner_integral_divide_zero[intro]:
  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x / c) (x / c)"
  using has_bochner_integral_divide by (cases "c = 0") auto

lemma has_bochner_integral_inner_left[intro]:
  "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x \ c) (x \ c)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])

lemma has_bochner_integral_inner_right[intro]:
  "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. c \ f x) (c \ x)"
  by (cases "c = 0") (auto simp: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])

lemmas has_bochner_integral_minus =
  has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
lemmas has_bochner_integral_Re =
  has_bochner_integral_bounded_linear[OF bounded_linear_Re]
lemmas has_bochner_integral_Im =
  has_bochner_integral_bounded_linear[OF bounded_linear_Im]
lemmas has_bochner_integral_cnj =
  has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
lemmas has_bochner_integral_of_real =
  has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
lemmas has_bochner_integral_fst =
  has_bochner_integral_bounded_linear[OF bounded_linear_fst]
lemmas has_bochner_integral_snd =
  has_bochner_integral_bounded_linear[OF bounded_linear_snd]

lemma has_bochner_integral_indicator:
  "A \ sets M \ emeasure M A < \ \
    has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)"
  by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)

lemma has_bochner_integral_diff:
  "has_bochner_integral M f x \ has_bochner_integral M g y \
    has_bochner_integral M (\<lambda>x. f x - g x) (x - y)"
  unfolding diff_conv_add_uminus
  by (intro has_bochner_integral_add has_bochner_integral_minus)

lemma has_bochner_integral_sum:
  "(\i. i \ I \ has_bochner_integral M (f i) (x i)) \
    has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
  by (induct I rule: infinite_finite_induct) auto

proposition has_bochner_integral_implies_finite_norm:
  "has_bochner_integral M f x \ (\\<^sup>+x. norm (f x) \M) < \"
proof (elim has_bochner_integral.cases)
  fix s v
  assume [measurable]: "f \ borel_measurable M" and s: "\i. simple_bochner_integrable M (s i)" and
    lim_0: "(\i. \\<^sup>+ x. ennreal (norm (f x - s i x)) \M) \ 0"
  from order_tendstoD[OF lim_0, of "\"]
  obtain i where f_s_fin: "(\\<^sup>+ x. ennreal (norm (f x - s i x)) \M) < \"
    by (auto simp: eventually_sequentially)

  have [measurable]: "\i. s i \ borel_measurable M"
    using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)

  define m where "m = (if space M = {} then 0 else Max ((\x. norm (s i x))`space M))"
  have "finite (s i ` space M)"
    using s by (auto simp: simple_function_def simple_bochner_integrable.simps)
  then have "finite (norm ` s i ` space M)"
    by (rule finite_imageI)
  then have "\x. x \ space M \ norm (s i x) \ m" "0 \ m"
    by (auto simp: m_def image_comp comp_def Max_ge_iff)
  then have "(\\<^sup>+x. norm (s i x) \M) \ (\\<^sup>+x. ennreal m * indicator {x\space M. s i x \ 0} x \M)"
    by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
  also have "\ < \"
    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)
  finally have s_fin: "(\\<^sup>+x. norm (s i x) \M) < \" .

  have "(\\<^sup>+ x. norm (f x) \M) \ (\\<^sup>+ x. ennreal (norm (f x - s i x)) + ennreal (norm (s i x)) \M)"
    by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
       (metis add.commute norm_triangle_sub)
  also have "\ = (\\<^sup>+x. norm (f x - s i x) \M) + (\\<^sup>+x. norm (s i x) \M)"
    by (rule nn_integral_add) auto
  also have "\ < \"
    using s_fin f_s_fin by auto
  finally show "(\\<^sup>+ x. ennreal (norm (f x)) \M) < \" .
qed

proposition has_bochner_integral_norm_bound:
  assumes i: "has_bochner_integral M f x"
  shows "norm x \ (\\<^sup>+x. norm (f x) \M)"
using assms proof
  fix s assume
    x: "(\i. simple_bochner_integral M (s i)) \ x" (is "?s \ x") and
    s[simp]: "\i. simple_bochner_integrable M (s i)" and
    lim: "(\i. \\<^sup>+ x. ennreal (norm (f x - s i x)) \M) \ 0" and
    f[measurable]: "f \ borel_measurable M"

  have [measurable]: "\i. s i \ borel_measurable M"
    using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function)

  show "norm x \ (\\<^sup>+x. norm (f x) \M)"
  proof (rule LIMSEQ_le)
    show "(\i. ennreal (norm (?s i))) \ norm x"
      using x by (auto simp: tendsto_ennreal_iff intro: tendsto_intros)
    show "\N. \n\N. norm (?s n) \ (\\<^sup>+x. norm (f x - s n x) \M) + (\\<^sup>+x. norm (f x) \M)"
      (is "\N. \n\N. _ \ ?t n")
    proof (intro exI allI impI)
      fix n
      have "ennreal (norm (?s n)) \ simple_bochner_integral M (\x. norm (s n x))"
        by (auto intro!: simple_bochner_integral_norm_bound)
      also have "\ = (\\<^sup>+x. norm (s n x) \M)"
        by (intro simple_bochner_integral_eq_nn_integral)
           (auto intro: s simple_bochner_integrable_compose2)
      also have "\ \ (\\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \M)"
        by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
           (metis add.commute norm_minus_commute norm_triangle_sub)
      also have "\ = ?t n"
        by (rule nn_integral_add) auto
      finally show "norm (?s n) \ ?t n" .
    qed
    have "?t \ 0 + (\\<^sup>+ x. ennreal (norm (f x)) \M)"
      using has_bochner_integral_implies_finite_norm[OF i]
      by (intro tendsto_add tendsto_const lim)
    then show "?t \ \\<^sup>+ x. ennreal (norm (f x)) \M"
      by simp
  qed
qed

lemma has_bochner_integral_eq:
  "has_bochner_integral M f x \ has_bochner_integral M f y \ x = y"
proof (elim has_bochner_integral.cases)
  assume f[measurable]: "f \ borel_measurable M"

  fix s t
  assume "(\i. \\<^sup>+ x. norm (f x - s i x) \M) \ 0" (is "?S \ 0")
  assume "(\i. \\<^sup>+ x. norm (f x - t i x) \M) \ 0" (is "?T \ 0")
  assume s: "\i. simple_bochner_integrable M (s i)"
  assume t: "\i. simple_bochner_integrable M (t i)"

  have [measurable]: "\i. s i \ borel_measurable M" "\i. t i \ borel_measurable M"
    using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)

  let ?s = "\i. simple_bochner_integral M (s i)"
  let ?t = "\i. simple_bochner_integral M (t i)"
  assume "?s \ x" "?t \ y"
  then have "(\i. norm (?s i - ?t i)) \ norm (x - y)"
    by (intro tendsto_intros)
  moreover
  have "(\i. ennreal (norm (?s i - ?t i))) \ ennreal 0"
  proof (rule tendsto_sandwich)
    show "eventually (\i. 0 \ ennreal (norm (?s i - ?t i))) sequentially" "(\_. 0) \ ennreal 0"
      by auto

    show "eventually (\i. norm (?s i - ?t i) \ ?S i + ?T i) sequentially"
      by (intro always_eventually allI simple_bochner_integral_bounded s t f)
    show "(\i. ?S i + ?T i) \ ennreal 0"
      using tendsto_add[OF \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>] by simp
  qed
  then have "(\i. norm (?s i - ?t i)) \ 0"
    by (simp flip: ennreal_0)
  ultimately have "norm (x - y) = 0"
    by (rule LIMSEQ_unique)
  then show "x = y" by simp
qed

lemma has_bochner_integralI_AE:
  assumes f: "has_bochner_integral M f x"
    and g: "g \ borel_measurable M"
    and ae: "AE x in M. f x = g x"
  shows "has_bochner_integral M g x"
  using f
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
  fix s assume "(\i. \\<^sup>+ x. ennreal (norm (f x - s i x)) \M) \ 0"
  also have "(\i. \\<^sup>+ x. ennreal (norm (f x - s i x)) \M) = (\i. \\<^sup>+ x. ennreal (norm (g x - s i x)) \M)"
    using ae
    by (intro ext nn_integral_cong_AE, eventually_elim) simp
  finally show "(\i. \\<^sup>+ x. ennreal (norm (g x - s i x)) \M) \ 0" .
qed (auto intro: g)

lemma has_bochner_integral_eq_AE:
  assumes "has_bochner_integral M f x" and "has_bochner_integral M g y"
    and "AE x in M. f x = g x"
  shows "x = y"
  by (meson assms has_bochner_integral.simps has_bochner_integral_cong_AE has_bochner_integral_eq)

lemma simple_bochner_integrable_restrict_space:
  fixes f :: "_ \ 'b::real_normed_vector"
  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
  shows "simple_bochner_integrable (restrict_space M \) f \
    simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  by (simp add: simple_bochner_integrable.simps space_restrict_space
    simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
    indicator_eq_0_iff conj_left_commute)

lemma simple_bochner_integral_restrict_space:
  fixes f :: "_ \ 'b::real_normed_vector"
  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
  assumes f: "simple_bochner_integrable (restrict_space M \) f"
  shows "simple_bochner_integral (restrict_space M \) f =
    simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
proof -
  have "finite ((\x. indicator \ x *\<^sub>R f x)`space M)"
    using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
    by (simp add: simple_bochner_integrable.simps simple_function_def)
  then show ?thesis
    by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
                   simple_bochner_integral_def Collect_restrict
             split: split_indicator split_indicator_asm
             intro!: sum.mono_neutral_cong_left arg_cong2[where f=measure])
qed

context
  notes [[inductive_internals]]
begin

inductive integrable for M f where
  "has_bochner_integral M f x \ integrable M f"

end

definition\<^marker>\<open>tag important\<close> lebesgue_integral (\<open>integral\<^sup>L\<close>) where
  "integral\<^sup>L M f = (if \x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"

syntax
  "_lebesgue_integral" :: "pttrn \ real \ 'a measure \ real"
    (\<open>(\<open>indent=1 notation=\<open>binder integral\<close>\<close>\<integral>(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
syntax_consts
  "_lebesgue_integral" == lebesgue_integral
translations
  "\ x. f \M" == "CONST lebesgue_integral M (\x. f)"

syntax
  "_ascii_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real"
    (\<open>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
syntax_consts
  "_ascii_lebesgue_integral" == lebesgue_integral
translations
  "LINT x|M. f" == "CONST lebesgue_integral M (\x. f)"

lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \ integral\<^sup>L M f = x"
  by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)

lemma has_bochner_integral_integrable:
  "integrable M f \ has_bochner_integral M f (integral\<^sup>L M f)"
  by (auto simp: has_bochner_integral_integral_eq integrable.simps)

lemma has_bochner_integral_iff:
  "has_bochner_integral M f x \ integrable M f \ integral\<^sup>L M f = x"
  by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)

lemma simple_bochner_integrable_eq_integral:
  "simple_bochner_integrable M f \ simple_bochner_integral M f = integral\<^sup>L M f"
  using has_bochner_integral_simple_bochner_integrable[of M f]
  by (simp add: has_bochner_integral_integral_eq)

lemma not_integrable_integral_eq: "\ integrable M f \ integral\<^sup>L M f = 0"
  unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])

lemma integral_eq_cases:
  "integrable M f \ integrable N g \
    (integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow>
    integral\<^sup>L M f = integral\<^sup>L N g"
  by (metis not_integrable_integral_eq)

lemma borel_measurable_integrable[measurable_dest]: "integrable M f \ f \ borel_measurable M"
  by (auto elim: integrable.cases has_bochner_integral.cases)

lemma borel_measurable_integrable'[measurable_dest]:
  "integrable M f \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N"
  using borel_measurable_integrable[measurable] by measurable

lemma integrable_cong:
  "M = N \ (\x. x \ space N \ f x = g x) \ integrable M f \ integrable N g"
  by (simp cong: has_bochner_integral_cong add: integrable.simps)

lemma integrable_cong_AE:
  "f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \
    integrable M f \<longleftrightarrow> integrable M g"
  unfolding integrable.simps
  by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)

lemma integrable_cong_AE_imp:
  "integrable M g \ f \ borel_measurable M \ (AE x in M. g x = f x) \ integrable M f"
  using integrable_cong_AE[of f M g] by (auto simp: eq_commute)

lemma integral_cong:
  "M = N \ (\x. x \ space N \ f x = g x) \ integral\<^sup>L M f = integral\<^sup>L N g"
  by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def)

lemma integral_cong_AE:
  "f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \
    integral\<^sup>L M f = integral\<^sup>L M g"
  unfolding lebesgue_integral_def
  by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)

lemma integrable_add[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x + g x)"
  by (auto simp: integrable.simps)

lemma integrable_zero[simp, intro]: "integrable M (\x. 0)"
  by (metis has_bochner_integral_zero integrable.simps)

lemma integrable_sum[simp, intro]: "(\i. i \ I \ integrable M (f i)) \ integrable M (\x. \i\I. f i x)"
  by (metis has_bochner_integral_sum integrable.simps)

lemma integrable_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \
  integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
  by (metis has_bochner_integral_indicator integrable.simps)

lemma integrable_real_indicator[simp, intro]: "A \ sets M \ emeasure M A < \ \
  integrable M (indicator A :: 'a \ real)"
  by (metis has_bochner_integral_real_indicator integrable.simps)

lemma integrable_diff[simp, intro]: "integrable M f \ integrable M g \ integrable M (\x. f x - g x)"
  by (auto simp: integrable.simps intro: has_bochner_integral_diff)

lemma integrable_bounded_linear: "bounded_linear T \ integrable M f \ integrable M (\x. T (f x))"
  by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)

lemma integrable_scaleR_left[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. f x *\<^sub>R c)"
  unfolding integrable.simps by fastforce

lemma integrable_scaleR_right[simp, intro]: "(c \ 0 \ integrable M f) \ integrable M (\x. c *\<^sub>R f x)"
  unfolding integrable.simps by fastforce

lemma integrable_mult_left[simp, intro]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ integrable M f) \ integrable M (\x. f x * c)"
  unfolding integrable.simps by fastforce

lemma integrable_mult_right[simp, intro]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ integrable M f) \ integrable M (\x. c * f x)"
  unfolding integrable.simps by fastforce

lemma integrable_divide_zero[simp, intro]:
  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  shows "(c \ 0 \ integrable M f) \ integrable M (\x. f x / c)"
  unfolding integrable.simps by fastforce

lemma integrable_inner_left[simp, intro]:
  "(c \ 0 \ integrable M f) \ integrable M (\x. f x \ c)"
  unfolding integrable.simps by fastforce

lemma integrable_inner_right[simp, intro]:
  "(c \ 0 \ integrable M f) \ integrable M (\x. c \ f x)"
  unfolding integrable.simps by fastforce

lemmas integrable_minus[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
lemmas integrable_divide[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_divide]
lemmas integrable_Re[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_Re]
lemmas integrable_Im[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_Im]
lemmas integrable_cnj[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_cnj]
lemmas integrable_of_real[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_of_real]
lemmas integrable_fst[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_fst]
lemmas integrable_snd[simp, intro] =
  integrable_bounded_linear[OF bounded_linear_snd]

lemma integral_zero[simp]: "integral\<^sup>L M (\x. 0) = 0"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)

lemma integral_add[simp]: "integrable M f \ integrable M g \
    integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)

lemma integral_diff[simp]: "integrable M f \ integrable M g \
    integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)

lemma integral_sum: "(\i. i \ I \ integrable M (f i)) \
  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_sum has_bochner_integral_integrable)

lemma integral_sum'[simp]: "(\i. i \ I =simp=> integrable M (f i)) \
  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
  unfolding simp_implies_def by (rule integral_sum)

lemma integral_bounded_linear: "bounded_linear T \ integrable M f \
    integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
  by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)

lemma integral_bounded_linear':
  assumes T: "bounded_linear T" and T': "bounded_linear T'"
  assumes *: "\ (\x. T x = 0) \ (\x. T' (T x) = x)"
  shows "integral\<^sup>L M (\x. T (f x)) = T (integral\<^sup>L M f)"
proof cases
  assume "(\x. T x = 0)" then show ?thesis
    by simp
next
  assume **: "\ (\x. T x = 0)"
  show ?thesis
  proof cases
    assume "integrable M f" with T show ?thesis
      by (rule integral_bounded_linear)
  next
    assume not: "\ integrable M f"
    moreover have "\ integrable M (\x. T (f x))"
      by (metis (full_types) "*" "**" T' integrable_bounded_linear integrable_cong not)
    ultimately show ?thesis
      using T by (simp add: not_integrable_integral_eq linear_simps)
  qed
qed

lemma integral_scaleR_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x *\<^sub>R c \M) = integral\<^sup>L M f *\<^sub>R c"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)

lemma integral_scaleR_right[simp]: "(\ x. c *\<^sub>R f x \M) = c *\<^sub>R integral\<^sup>L M f"
  by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp

lemma integral_mult_left[simp]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ integrable M f) \ (\ x. f x * c \M) = integral\<^sup>L M f * c"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)

lemma integral_mult_right[simp]:
  fixes c :: "_::{real_normed_algebra,second_countable_topology}"
  shows "(c \ 0 \ integrable M f) \ (\ x. c * f x \M) = c * integral\<^sup>L M f"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)

lemma integral_mult_left_zero[simp]:
  fixes c :: "_::{real_normed_field,second_countable_topology}"
  shows "(\ x. f x * c \M) = integral\<^sup>L M f * c"
  by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp

lemma integral_mult_right_zero[simp]:
  fixes c :: "_::{real_normed_field,second_countable_topology}"
  shows "(\ x. c * f x \M) = c * integral\<^sup>L M f"
  by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp

lemma integral_inner_left[simp]: "(c \ 0 \ integrable M f) \ (\ x. f x \ c \M) = integral\<^sup>L M f \ c"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)

lemma integral_inner_right[simp]: "(c \ 0 \ integrable M f) \ (\ x. c \ f x \M) = c \ integral\<^sup>L M f"
  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)

lemma integral_divide_zero[simp]:
  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
  shows "integral\<^sup>L M (\x. f x / c) = integral\<^sup>L M f / c"
  by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp

lemma integral_minus[simp]: "integral\<^sup>L M (\x. - f x) = - integral\<^sup>L M f"
  by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp

lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp

lemma integral_cnj[simp]: "integral\<^sup>L M (\x. cnj (f x)) = cnj (integral\<^sup>L M f)"
  by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp

lemmas integral_divide[simp] =
  integral_bounded_linear[OF bounded_linear_divide]
lemmas integral_Re[simp] =
  integral_bounded_linear[OF bounded_linear_Re]
lemmas integral_Im[simp] =
  integral_bounded_linear[OF bounded_linear_Im]
lemmas integral_of_real[simp] =
  integral_bounded_linear[OF bounded_linear_of_real]
lemmas integral_fst[simp] =
  integral_bounded_linear[OF bounded_linear_fst]
lemmas integral_snd[simp] =
  integral_bounded_linear[OF bounded_linear_snd]

lemma integral_norm_bound_ennreal:
  "integrable M f \ norm (integral\<^sup>L M f) \ (\\<^sup>+x. norm (f x) \M)"
  by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)

lemma integrableI_sequence:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes f[measurable]: "f \ borel_measurable M"
  assumes s: "\i. simple_bochner_integrable M (s i)"
  assumes lim: "(\i. \\<^sup>+x. norm (f x - s i x) \M) \ 0" (is "?S \ 0")
  shows "integrable M f"
proof -
  let ?s = "\n. simple_bochner_integral M (s n)"

  have "\x. ?s \ x"
    unfolding convergent_eq_Cauchy
  proof (rule metric_CauchyI)
    fix e :: real assume "0 < e"
    then have "0 < ennreal (e / 2)" by auto
    from order_tendstoD(2)[OF lim this]
    obtain M where M: "\n. M \ n \ ?S n < e / 2"
      by (auto simp: eventually_sequentially)
    show "\M. \m\M. \n\M. dist (?s m) (?s n) < e"
    proof (intro exI allI impI)
      fix m n assume m: "M \ m" and n: "M \ n"
      have "?S n \ \"
        using M[OF n] by auto
      have "norm (?s n - ?s m) \ ?S n + ?S m"
        by (intro simple_bochner_integral_bounded s f)
      also have "\ < ennreal (e / 2) + e / 2"
        by (intro add_strict_mono M n m)
      also have "\ = e" using \0 by (simp flip: ennreal_plus)
      finally show "dist (?s n) (?s m) < e"
        using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
    qed
  qed
  then obtain x where "?s \ x" ..
  show ?thesis
    by (rule, rule) fact+
qed

proposition nn_integral_dominated_convergence_norm:
  fixes u' :: "_ \ _::{real_normed_vector, second_countable_topology}"
  assumes [measurable]:
       "\i. u i \ borel_measurable M" "u' \ borel_measurable M" "w \ borel_measurable M"
    and bound: "\j. AE x in M. norm (u j x) \ w x"
    and w: "(\\<^sup>+x. w x \M) < \"
    and u': "AE x in M. (\i. u i x) \ u' x"
  shows "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) \ 0"
proof -
  have "AE x in M. \j. norm (u j x) \ w x"
    unfolding AE_all_countable by rule fact
  with u' have bnd: "AE x in M. \j. norm (u' x - u j x) \ 2 * w x"
  proof (eventually_elim, intro allI)
    fix i x assume "(\i. u i x) \ u' x" "\j. norm (u j x) \ w x" "\j. norm (u j x) \ w x"
    then have "norm (u' x) \ w x" "norm (u i x) \ w x"
      by (auto intro: LIMSEQ_le_const2 tendsto_norm)
    then have "norm (u' x) + norm (u i x) \ 2 * w x"
      by simp
    also have "norm (u' x - u i x) \ norm (u' x) + norm (u i x)"
      by (rule norm_triangle_ineq4)
    finally (xtrans) show "norm (u' x - u i x) \ 2 * w x" .
  qed
  have w_nonneg: "AE x in M. 0 \ w x"
    using bound[of 0] by (auto intro: order_trans[OF norm_ge_zero])

  have "(\i. (\\<^sup>+x. norm (u' x - u i x) \M)) \ (\\<^sup>+x. 0 \M)"
  proof (rule nn_integral_dominated_convergence)
    show "(\\<^sup>+x. 2 * w x \M) < \"
      by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) (insert w_nonneg, auto simp: ennreal_mult )
    show "AE x in M. (\i. ennreal (norm (u' x - u i x))) \ 0"
      using u'
    proof eventually_elim
      fix x assume "(\i. u i x) \ u' x"
      from tendsto_diff[OF tendsto_const[of "u' x"] this]
      show "(\i. ennreal (norm (u' x - u i x))) \ 0"
        by (simp add: tendsto_norm_zero_iff flip: ennreal_0)
    qed
  qed (use bnd w_nonneg in auto)
  then show ?thesis by simp
qed

proposition integrableI_bounded:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes f[measurable]: "f \ borel_measurable M" and fin: "(\\<^sup>+x. norm (f x) \M) < \"
  shows "integrable M f"
proof -
  from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
    s: "\i. simple_function M (s i)" and
    pointwise: "\x. x \ space M \ (\i. s i x) \ f x" and
    bound: "\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)"
    by simp metis

  show ?thesis
  proof (rule integrableI_sequence)
    { fix i
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.39Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.