Theory Bochner_Integration

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

section ‹Bochner Integration for Vector-Valued Functions›

theory Bochner_Integration
  imports Finite_Product_Measure
begin

text ‹

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

›

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))  (xspace M. (λi. F i x)  f x) 
    (i. xspace M. dist (F i x) z  2 * dist (f x) z)"
proof -
  obtain D :: "'b set" where "countable D" and D: "X. open X  X  {}  dD. 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 d  D D[of UNIV] countable D 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 =
    {xspace M. dist (f x) (e n) < 1 / (Suc m)  1 / (Suc m)  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  (nN. B m n)}" for N x
  define F where [abs_def]: "F N x =
    (if (mN. x  (nN. B m n))  (nN. x  B (m N x) n)
     then e (LEAST n. x  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 "mN. x  (nN. B m n)"
    then have "m N x  {m::nat. m  N  x  (nN. B m n)}"
      unfolding m_def by (intro Max_in) auto
    then have "m N x  N" "nN. 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: "mN. x  (nN. 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 f x  z 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 xspace M f x  z have "x  (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 1 / Suc n < e
          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{xA. g x  B x}. f x)"
  and sum_indicator_mult[simp]: "(x  A. indicator (B x) (g x) * f x) = (x{xA. 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  borel_measurable M" "x. 0  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. yU' i`space M. y * indicator {xspace 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. yU' i`space M. y * indicator {xspace 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 + 
                   (yF. y * indicat_real {x  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 *R x = p *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 {yspace 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 (λ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 {xspace M. p (f x) (g x)  0} 
      emeasure M ({xspace M. f x  0}  {xspace M. g x  0})"
    by (intro emeasure_mono) (auto simp: p_0)
  also have "  emeasure M {xspace M. f x  0} + emeasure M {xspace 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: "(+x. f x M) < " and nn: "x. 0  f x"
  shows "emeasure M {xspace M. f x  0}  "
proof cases
  from f have meas[measurable]: "f  borel_measurable M"
    by (rule borel_measurable_simple_function)

  assume non_empty: "xspace 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 {xspace M. 0  f x} =
    (+x. m * indicator {xspace M. 0  f x} x M)"
    using f by (intro nn_integral_cmult_indicator[symmetric]) auto
  also have "  (+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  < 
  finally show ?thesis
    using m by (auto simp: ennreal_mult_less_top)
next
  assume "¬ (xspace M. f x  0)"
  with nn have *: "{xspace 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: "(+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

definitiontag important› simple_bochner_integral :: "'a measure  ('a  'b::real_vector)  'b" where
  "simple_bochner_integral M f = (yf`space M. measure M {xspace M. f x = y} *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 = (yg ` space M. measure M {xspace M. g x = y} *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. xspace 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 =
    (yf`space M. (zg`space M.
      if xspace M. y = f x  z = g x then measure M {xspace M. g x = z} else 0) *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. xspace M. f y = f x  z = g x} =
        {z. xspace M. f y = f x  z = g x}"
      by auto
    have eq:"{x  space M. f x = f y} =
        (i{z. xspace M. f y = f x  z = g x}. {x  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. xspace 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} =
      (zg ` space M. if xspace M. f y = f x  z = g x then measure M {x  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 " = (yf`space M. (zg`space M.
      if xspace M. y = f x  z = g x then measure M {xspace M. g x = z} *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) =
    (y(λx. (f x, g x)) ` space M. measure M {x  space M. (f x, g x) = y} *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 =
    (y(λx. (f x, g x)) ` space M. measure M {x  space M. (f x, g x) = y} *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 =
    (y(λx. (f x, g x)) ` space M. measure M {x  space M. (f x, g x) = y} *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)) =
    (yg ` space M. measure M {x  space M. g x = y} *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) 
    (yf ` space M. norm (measure M {x  space M. f x = y} *R y))"
    unfolding simple_bochner_integral_def by (rule norm_sum)
  also have " = (yf ` space M. measure M {x  space M. f x = y} *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 = (+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 ((λx. ennreal (f x)) -` {ennreal (f y)}  space M)" by simp }
  with f have "simple_bochner_integral M f = (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 " = (+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)) 
    (+ x. norm (f x - s x) M) + (+ x. norm (f x - t x) 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 " = (+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 "  (+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)  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 
    (i. simple_bochner_integrable M (s i)) 
    (λi. +x. norm (f x - s i x) M)  0 
    (λi. simple_bochner_integral M (s i))  x 
    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  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 Asets M] 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 (λ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. + x. norm (f x - sf i x) M)  0"
  assume g_sg: "(λi. + 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. + 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  (+ x. (norm (f x - sf i x)) M) + + 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  (+ 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. + 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. + 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 * (+ 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  (+ 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 *R c) (x *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 *R f x) (c *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 (λx. indicator A x *R c) (measure M A *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 (λ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 (λx. iI. f i x) (iI. x i)"
  by (induct I rule: infinite_finite_induct) auto

proposition has_bochner_integral_implies_finite_norm:
  "has_bochner_integral M f x  (+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. + x. ennreal (norm (f x - s i x)) M)  0"
  from order_tendstoD[OF lim_0, of ""]
  obtain i where f_s_fin: "(+ 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 "(+x. norm (s i x) M)  (+x. ennreal m * indicator {xspace 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: 0  m simple_bochner_integrable.simps ennreal_mult_less_top less_top)
  finally have s_fin: "(+x. norm (s i x) M) < " .

  have "(+ x. norm (f x) M)  (+ 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 " = (+x. norm (f x - s i x) M) + (+x. norm (s i x) M)"
    by (rule nn_integral_add) auto
  also have " < "
    using s_fin f_s_fin by auto
  finally show "(+ x. ennreal (norm (f x)) M) < " .
qed

proposition has_bochner_integral_norm_bound:
  assumes i: "has_bochner_integral M f x"
  shows "norm x  (+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. + 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  (+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. nN. norm (?s n)  (+x. norm (f x - s n x) M) + (+x. norm (f x) M)"
      (is "N. nN. _  ?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 " = (+x. norm (s n x) M)"
        by (intro simple_bochner_integral_eq_nn_integral)
           (auto intro: s simple_bochner_integrable_compose2)
      also have "  (+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 + (+ 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  + 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. + x. norm (f x - s i x) M)  0" (is "?S  0")
  assume "(λi. + 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 ?S  0 ?T  0] 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. + x. ennreal (norm (f x - s i x)) M)  0"
  also have "(λi. + x. ennreal (norm (f x - s i x)) M) = (λi. + x. ennreal (norm (g x - s i x)) M)"
    using ae
    by (intro ext nn_integral_cong_AE, eventually_elim) simp
  finally show "(λi. + 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 Ω: "Ω  space M  sets M"
  shows "simple_bochner_integrable (restrict_space M Ω) f 
    simple_bochner_integrable M (λx. indicator Ω x *R f x)"
  by (simp add: simple_bochner_integrable.simps space_restrict_space
    simple_function_restrict_space[OF Ω] emeasure_restrict_space[OF Ω] Collect_restrict
    indicator_eq_0_iff conj_left_commute)

lemma simple_bochner_integral_restrict_space:
  fixes f :: "_  'b::real_normed_vector"
  assumes Ω: "Ω  space M  sets M"
  assumes f: "simple_bochner_integrable (restrict_space M Ω) f"
  shows "simple_bochner_integral (restrict_space M Ω) f =
    simple_bochner_integral M (λx. indicator Ω x *R f x)"
proof -
  have "finite ((λx. indicator Ω x *R f x)`space M)"
    using f simple_bochner_integrable_restrict_space[OF Ω, 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 Ω(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

definitiontag important› lebesgue_integral ("integralL") where
  "integralL 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" ("((2 _./ _)/ _)" [60,61] 110)

translations
  " x. f M" == "CONST lebesgue_integral M (λx. f)"

syntax
  "_ascii_lebesgue_integral" :: "pttrn  'a measure  real  real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)

translations
  "LINT x|M. f" == "CONST lebesgue_integral M (λx. f)"

lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x  integralL 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 (integralL 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  integralL 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 = integralL 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  integralL 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  integrable N g  integralL M f = integralL N g) 
    integralL M f = integralL 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  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)  integralL M f = integralL 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 
    integralL M f = integralL 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. iI. f i x)"
  by (metis has_bochner_integral_sum integrable.simps)

lemma integrable_indicator[simp, intro]: "A  sets M  emeasure M A <  
  integrable M (λx. indicator A x *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 *R c)"
  unfolding integrable.simps by fastforce

lemma integrable_scaleR_right[simp, intro]: "(c  0  integrable M f)  integrable M (λx. c *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]: "integralL 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 
    integralL M (λx. f x + g x) = integralL M f + integralL 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 
    integralL M (λx. f x - g x) = integralL M f - integralL 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)) 
  integralL M (λx. iI. f i x) = (iI. integralL 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)) 
  integralL M (λx. iI. f i x) = (iI. integralL M (f i))"
  unfolding simp_implies_def by (rule integral_sum)

lemma integral_bounded_linear: "bounded_linear T  integrable M f 
    integralL M (λx. T (f x)) = T (integralL 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 "integralL M (λx. T (f x)) = T (integralL 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 *R c M) = integralL M f *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 *R f x M) = c *R integralL 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) = integralL 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 * integralL 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) = integralL 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 * integralL 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) = integralL 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  integralL 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 "integralL M (λx. f x / c) = integralL M f / c"
  by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp

lemma integral_minus[simp]: "integralL M (λx. - f x) = - integralL 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]: "integralL M (λx. complex_of_real (f x)) = of_real (integralL M f)"
  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp

lemma integral_cnj[simp]: "integralL M (λx. cnj (f x)) = cnj (integralL 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 (integralL M f)  (+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. +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. mM. nM. 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<e by (simp flip: ennreal_plus)
      finally show "dist (?s n) (?s m) < e"
        using 0<e 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: "(+x. w x M) < "
    and u': "AE x in M. (λi. u i x)  u' x"
  shows "(λi. (+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. (+x. norm (u' x - u i x) M))  (+x. 0 M)"
  proof (rule nn_integral_dominated_convergence)
    show "(+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: "(+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
      have "(+x. norm (s i x) M)  (+x. ennreal (2 * norm (f x)) M)"
        by (intro nn_integral_mono) (simp add: bound)
      also have " = 2 * (+x. ennreal (norm (f x)) M)"
        by (simp add: ennreal_mult nn_integral_cmult)
      also have " < top"
        using fin by (simp add: ennreal_mult_less_top)
      finally have "(+x. norm (s i x) M) < "
        by simp }
    note fin_s = this

    show "i. simple_bochner_integrable M (s i)"
      by (rule simple_bochner_integrableI_bounded) fact+

    show "(λi. + x. ennreal (norm (f x - s i x)) M)  0"
    proof (rule nn_integral_dominated_convergence_norm)
      show "j. AE x in M. norm (s j x)  2 * norm (f x)"
        using bound by auto
      show "i. s i  borel_measurable M" "(λx. 2 * norm (f x))  borel_measurable M"
        using s by (auto intro: borel_measurable_simple_function)
      show "(+ x. ennreal (2 * norm (f x)) M) < "
        using fin by (simp add: nn_integral_cmult ennreal_mult ennreal_mult_less_top)
      show "AE x in M. (λi. s i x)  f x"
        using pointwise by auto
    qed fact
  qed fact
qed

lemma integrableI_bounded_set:
  fixes f :: "'a  'b::{banach, second_countable_topology}"
  assumes [measurable]: "A  sets M" "f  borel_measurable M"
  assumes finite: "emeasure M A < "
    and bnd: "AE x in M. x  A  norm (f x)  B"
    and null: "AE x in M. x  A  f x = 0"
  shows "integrable M f"
proof (rule integrableI_bounded)
  { fix x :: 'b have "norm x  B  0  B"
      using norm_ge_zero[of x] by arith }
  with bnd null have "(+ x. ennreal (norm (f x)) M)  (+ x. ennreal (max 0 B) * indicator A x M)"
    by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
  also have " < "
    using finite by (subst nn_integral_cmult_indicator) (auto simp: ennreal_mult_less_top)
  finally show "(+ x. ennreal (norm (f x)) M) < " .
qed simp

lemma integrableI_bounded_set_indicator:
  fixes f :: "'a  'b</