Theory Additional_Lemmas_for_Integrals

(*
 Title:Additional_Lemmas_for_Integrals.thy
 Author: Tetsuya Sato
 Author: Yasuhiko Minamide
*)

theory Additional_Lemmas_for_Integrals
  imports"HOL-Probability.Probability"
begin

section ‹Lemmas for Integrals›

subsection ‹Lemmas on Nonnegative Integrals›

(*
 The below lemma is for integrals on intervals of type {.. a}.
 It is a modification of Equivalence_Lebesgue_Henstock_Integration.nn_integral_FTC_atLeast,
 which is for integrals on intervals of type {a ..}. The proof is also borrowed from it.
*)

lemma nn_integral_FTC_atGreatest:
  fixes f :: "real ⇒ real"
  assumes f_borel: "f ∈ borel_measurable borel"
  assumes f: "⋀x. x ≤ a ⟹ DERIV F x :> f x"
  assumes nonneg: "⋀x. x ≤ a ⟹ 0 ≤ f x"
  assumes lim: "(F ⤏ T) at_bot"
  shows "(∫⇧+x. ennreal (f x) * indicator {..a} x ∂lborel) = F a - T"
proof-
  let ?f ="λ(i :: nat) (x :: real). ennreal (f x) * indicator {(a - real i)..a} x"
  let ?fR ="λx. ennreal (f x) * indicator {.. a} x"

  have F_mono: "x ≤ a ⟹ y ≤ x ⟹ F y ≤ F x"for x y
    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of y x F]) (auto intro: order_trans)
  hence F_le_T: "x ≤ a ⟹ T ≤ F x"for x
    by (intro tendsto_upperbound[OF lim]) (auto simp: eventually_at_bot_linorder)
  have "(SUP i. ?f i x) = ?fR x"for x
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
    obtain n where"a - x < real n"
      using reals_Archimedean2[of"a - x"] ..
    hence "eventually (λn. ?f n x = ?fR x) sequentially"
      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
    thus"(λn. ?f n x) ⇢ ?fR x"
      by (rule tendsto_eventually)
  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
  hence "integral⇧N lborel ?fR = (∫⇧+ x. (SUP i. ?f i x) ∂lborel)"
    by auto
  also have "… = (SUP i. (∫⇧+ x. ?f i x ∂lborel))"
  proof (rule nn_integral_monotone_convergence_SUP)
    show "incseq ?f"
      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
    show "⋀i. (?f i) ∈ borel_measurable lborel"
      using f_borel by auto
  qed
  also have "… = (SUP i. ennreal (F a - F (a - real i)))"
    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
  also have "… = F a - T"
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
    show "incseq (λi. ennreal (F a - F (a - real i)))"
      by (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
    have P: "LIM x sequentially. a - real x :> at_bot"
    proof(subst filterlim_at_bot_lt[where c = 0],safe)
      fix Z :: real assume "Z < 0"
      show "∀⇩F x in sequentially. a - real x ≤ Z"
      proof (rule eventually_sequentiallyI[where c ="nat ⌊(a - Z)⌋ + 1"])
        fix x assume "nat ⌊a - Z⌋ + 1 ≤ x"
        show "a - real x ≤ Z"
          using ‹nat ⌊a - Z⌋ + 1 ≤ x› by linarith
      qed
    qed
    have "(λx. F (a - real x)) ⇢ T"
      by(intro filterlim_compose[OF lim P])
    thus"(λi. ennreal (F a - F (a - real i))) ⇢ ennreal (F a - T)"
      by (auto simp: F_mono F_le_T tendsto_diff)
  qed
  finally show ?thesis by auto
qed

lemma nn_integral_split_null_intersection:
  assumes [measurable]: "f ∈ borel_measurable M"
    "B ∈ sets M" "C ∈ sets M"
    "B ∩ C ∈ null_sets M"
  shows "(∫⇧+x ∈ B ∪ C. f x ∂M) = (∫⇧+x ∈ B. f x ∂M) + (∫⇧+x ∈ C. f x ∂M)"
proof-
  let ?D ="B ∩ C"
  have eq1: "(∫⇧+x ∈ B. f x ∂M) = (∫⇧+x ∈ (B - ?D). f x ∂M)"
  proof(rule nn_integral_null_delta)
    have "sym_diff B (B - ?D) = ?D"by auto
    thus"sym_diff B (B - ?D)∈ null_sets M"using assms by auto
  qed(auto)
  have "B ∪ C = (B - ?D) ∪ C"by auto
  hence "(∫⇧+x ∈ B ∪ C. f x ∂M) = (∫⇧+x ∈ (B - ?D) ∪ C. f x ∂M)"
    by auto
  also have "... =(∫⇧+x ∈ (B - ?D). f x ∂M) + (∫⇧+x ∈ C. f x ∂M)"
    by(rule nn_integral_disjoint_pair,auto)
  thus ?thesis using eq1 calculation by auto
qed

lemma nn_integral_split_null_intersection2:
  assumes [measurable]: "f ∈ borel_measurable M"
    "B ∈ sets M" "C ∈ sets M"
    "B ∩ C ∈ null_sets M"
    "A = B ∪ C"
  shows "(∫⇧+x ∈ A. f x ∂M) = (∫⇧+x ∈ B. f x ∂M) + (∫⇧+x ∈ C. f x ∂M)"
  by (auto simp: assms(4) assms(5) nn_integral_split_null_intersection)

lemma nn_integral_interval_lessThan_atMost:
  fixes m :: "real"
  assumes "f ∈ borel_measurable lborel"
  shows "(∫⇧+ x∈ {..m}. f x ∂lborel) = (∫⇧+ x ∈ {..<m}. f x ∂lborel)"
proof(rule nn_integral_null_delta)
  have "sym_diff {..m} {..<m} = {m}"by auto
  also have "... ∈ null_sets lborel"
    by auto
  finally show "sym_diff {..m} {..<m} ∈ null_sets lborel".
qed(auto)

lemma nn_integral_interval_greaterThan_atLeast:
  fixes m :: "real"
  assumes "f ∈ borel_measurable lborel"
  shows "(∫⇧+ x∈ {m..}. f x ∂lborel) = (∫⇧+ x ∈ {m<..}. f x ∂lborel)"
proof(rule nn_integral_null_delta)
  have "sym_diff {m..} {m<..} = {m}"by auto
  also have "... ∈ null_sets lborel"
    by auto
  finally show "sym_diff {m..} {m<..} ∈ null_sets lborel".
qed(auto)

lemma nn_set_integral_lborel_split:
  fixes m :: "real"
  assumes [measurable]: "f ∈ borel_measurable lborel"
  shows "(∫⇧+ x∈UNIV. f x ∂lborel) = (∫⇧+ x ∈ {..m}. f x ∂lborel) + (∫⇧+ x ∈ {m..}. f x ∂lborel)"
proof(rule nn_integral_split_null_intersection2)
  have "{..m} ∩ {m..} = {m}"by auto
  thus"{..m} ∩ {m..} ∈ null_sets lborel"by auto
qed(auto)

lemma nn_set_integral_lborel_split_AtMost:
  fixes m n :: "real"
  assumes [measurable]: "f ∈ borel_measurable lborel"
    and "n ≤ m"
  shows "(∫⇧+ x∈{..m}. f x ∂lborel) = (∫⇧+ x ∈ {..n}. f x ∂lborel) + (∫⇧+ x ∈ {n..m}. f x ∂lborel)"
proof(rule nn_integral_split_null_intersection2)
  show "{..m} = {..n} ∪ {n..m}"using assms(2) by auto
qed(auto simp add: assms(2))

lemma nn_set_integral_lborel_split_AtLeast:
  fixes m n :: "real"
  assumes [measurable]: "f ∈ borel_measurable lborel"
    and "n ≤ m"
  shows "(∫⇧+ x∈{n..}. f x ∂lborel) = (∫⇧+ x ∈ {n..m}. f x ∂lborel) + (∫⇧+ x ∈ {m..}. f x ∂lborel)"
proof(rule nn_integral_split_null_intersection2)
  show "{n..} = {n..m} ∪ {m..}"using assms(2) by auto
qed(auto simp add: assms(2))

lemma nn_set_integral_lborel_split_AtMostAtLeast:
  fixes l m n :: "real"
  assumes [measurable]: "f ∈ borel_measurable lborel"
    and "l ≤ m"
    and "m ≤ n"
  shows "(∫⇧+ x∈{l..n}. f x ∂lborel) = (∫⇧+ x ∈ {l..m}. f x ∂lborel) + (∫⇧+ x ∈ {m..n}. f x ∂lborel)"
proof(rule nn_integral_split_null_intersection2, auto simp: assms(2,3))
  show "⋀x. l ≤ x ⟹ x ≤ m ⟹ x ≤ n"using assms(2,3) by auto
  show "⋀x. m ≤ x ⟹ x ≤ n ⟹ l ≤ x"using assms(2,3) by auto
qed

lemma nn_integral_lborel_split:
  fixes m :: "real"
  assumes [measurable]: "f ∈ borel_measurable lborel"
  shows "(∫⇧+ x. f x ∂lborel) = (∫⇧+ x ∈ {..m}. f x ∂lborel) + (∫⇧+ x ∈ {m..}. f x ∂lborel)"
  using nn_set_integral_lborel_split by force

subsection ‹Lemmas on Bochner Integrals›

lemma integral_split_indicator[simp]:
  assumes "Ω ∈ sets M" "(f :: _⇒ real) ∈ borel_measurable M" "integrable M f"
  shows "(∫ x. f x ∂M) = (∫ x ∈ Ω. f x ∂M) + (∫ x ∈ space M - Ω. f x ∂M)"
proof -
  have "(Ω ∪ (space M - Ω)) = space M"
    using assms(1) sets.sets_into_space by blast
  hence "(∫ x. f x ∂M) = (∫ x∈ (Ω ∪ (space M - Ω)). f x ∂M)"
    by (auto simp: assms(3) set_integral_space)
  also have "... =(∫ x ∈ Ω. f x ∂M) + (∫ x ∈ space M - Ω. f x ∂M)"
  proof(rule set_integral_Un)
    have P: "set_integrable M (space M) f"unfolding set_integrable_def
      using integrable_mult_indicator assms by blast
    thus"set_integrable M Ω f"using set_integrable_subset assms sets.sets_into_space by metis
    have "(space M - Ω) ∈ sets M"
      using assms by auto
    thus"set_integrable M (space M - Ω) f"using P set_integrable_subset sets.sets_into_space by metis
  qed(auto)
  finally show "(∫ x. f x ∂M) = (∫ x ∈ Ω. f x ∂M) + (∫ x ∈ space M - Ω. f x ∂M)".
qed

lemma integral_drop_negative_part:
  assumes "(f :: _⇒real) ∈ borel_measurable M"
    and "integrable M f"
  shows "(∫ x. f x ∂M) ≤ (∫x∈{x ∈ space M. 0 < f x}. f x ∂M)"
proof-
  let ?A ="{x ∈ space M. 0 < f x}"
  have PM: "?A ∈ sets M"
    using assms(1) assms(2) borel_measurable_le by auto
  have splitP: "(∫ x. f x ∂M) = (∫ x ∈?A. f x ∂M) + (∫ x ∈ space M - ?A. f x ∂M)"
    using assms by auto
  have negpart: "∀ x∈ space M.(indicator (space M - ?A) x)* (f x) ≤ 0"
  proof
    fix x assume A: "x ∈ space M"
    show "indicat_real (space M - ?A) x *(f x) ≤ 0"
    proof(cases)
      assume "x ∈ ?A"
      hence "indicat_real (space M - ?A) x = 0"by auto
      thus ?thesis by auto
    next assume A1: "x ∉ ?A"
      hence "x ∈ space M - ?A"using A by auto
      hence "indicat_real (space M - ?A) x = 1"by auto moreover
      have "f x ≤ 0"using A1 A by auto
      thus ?thesis
        by (auto simp: calculation)
    qed
  qed
  have "(∫ x ∈ space M - ?A. f x ∂M) ≤ (∫ x ∈ space M - ?A. (λ x.0)x ∂M)"
  proof(rule set_integral_mono)
    show "set_integrable M (space M - ?A) f"
      unfolding set_integrable_def
      using assms integrable_mult_indicator sets.compl_sets PM by blast
    show "set_integrable M (space M - ?A) (λx. 0)"
      unfolding set_integrable_def
      by auto
    show "⋀x. x ∈ space M - ?A ⟹ f x ≤ 0"
      using negpart by auto
  qed
  also have "... ≤ 0"
    by auto
  finally have ineq0: "(∫ x ∈ space M - ?A. f x ∂M) ≤ 0".
  show "(∫ x. f x ∂M) ≤ (∫ x ∈?A. f x ∂M)"
    using splitP ineq0 by auto
qed

lemma integral_drop_negative_part2:
  assumes "(f :: _⇒real) ∈ borel_measurable M"
    and "integrable M f"
    and "A ∈ sets M"
    and "{x ∈ space M. 0 < f x} ⊆ A"
    and "A ⊆ {x ∈ space M. 0 ≤ f x}"
  shows "(∫ x. f x ∂M) ≤ (∫x ∈ A. f x ∂M)"
proof-
  have meas: "A - {x ∈ space M. 0 < f x} ∈ sets M"
    using assms by measurable
  have meas2: "{x ∈ space M. 0 < f x} ∈ sets M"
    using assms by measurable
  have eq0: "∀ x ∈ (A - {x ∈ space M. 0 < f x}). f x = 0"
  proof
    fix x assume A: "x ∈ (A - {x ∈ space M. 0 < f x})"
    show "f x = 0"
      using assms A by auto
  qed
  have "(∫x∈(A - {x ∈ space M. 0 < f x}). f x ∂M) = (∫x∈(A - {x ∈ space M. 0 < f x}). (λ x. 0) x ∂M)"
  proof(rule eq0 set_lebesgue_integral_cong)
    show "A - {x ∈ space M. 0 < f x} ∈ sets M"
      using meas by auto
    show "∀x. x ∈ A - {x ∈ space M. 0 < f x} ⟶ f x = 0"
      using eq0 by blast
  qed
  hence eq1: "(∫x∈(A - {x ∈ space M. 0 < f x}). f x ∂M) = 0"
    by auto
  have ineq1: "(∫ x. f x ∂M) ≤ (∫x∈{x ∈ space M. 0 < f x}. f x ∂M)"
    by(auto intro!: integral_drop_negative_part simp: assms)
  also have "... = (∫x∈{x ∈ space M. 0 < f x}. f x ∂M) + (∫x∈(A - {x ∈ space M. 0 < f x}). f x ∂M)"
    using eq1 by auto
  also have "... = (∫x∈({x ∈ space M. 0 < f x}∪(A - {x ∈ space M. 0 < f x})). f x ∂M)"
  proof(rule set_integral_Un[THEN sym])
    show "{x ∈ space M. 0 < f x} ∩ (A - {x ∈ space M. 0 < f x}) = {}"
      by auto
    have t: "set_integrable M (space M) f"
      unfolding set_integrable_def assms
      using assms(2) integrable_mult_indicator by blast
    show "set_integrable M {x ∈ space M. 0 < f x} f"
      using set_integrable_subset t meas2 by blast
    show "set_integrable M (A - {x ∈ space M. 0 < f x}) f"
      using set_integrable_subset[OF t meas] meas sets.sets_into_space by blast
  qed
  also have "... = (∫x∈A. f x ∂M)"
    by (auto simp: Un_absorb2 Un_commute assms(4))
  finally show "(∫ x. f x ∂M) ≤ (∫x∈A. f x ∂M)".
qed

lemma set_integral_indicator:
	fixes M :: "'a measure" and c :: "real"
	assumes "B ∈ sets M"
	  and "emeasure M B < ⊤"
	shows "(∫ x∈ B. c ∂M) = c * measure M B"
proof-
	have "(∫ x∈ B. c ∂M) = (∫ x. c * indicator B x ∂M)"
		by (auto simp: set_lebesgue_integral_def)
	also have "... = c *(∫ x. indicator B x ∂M)"
		using integral_mult_right_zero by blast
	also have "... = c * measure M B"
	proof-
	  have "(∫ x. indicator B x ∂M) = measure M B"
	  proof(rule has_bochner_integral_integral_eq,rule has_bochner_integral_real_indicator)
	    show "B ∈ sets M"using assms(1) by auto
	    show "emeasure M B < ∞"using assms(2) by auto
	  qed
	  thus ?thesis by auto
	qed
	finally show "(∫ x∈ B. c ∂M) = c * measure M B".
qed

end