src/HOL/Analysis/Set_Integral.thy
author paulson <lp15@cam.ac.uk>
Wed, 28 Sep 2016 17:01:01 +0100
changeset 63952 354808e9f44b
parent 63941 f353674c2528
child 63958 02de4a58e210
permissions -rw-r--r--
new material connected with HOL Light measure theory, plus more rationalisation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63627
6ddb43c6b711 rename HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl
parents: 63626
diff changeset
     1
(*  Title:      HOL/Analysis/Set_Integral.thy
63329
6b26c378ab35 Probability: tuned headers; cleanup Radon_Nikodym
hoelzl
parents: 63092
diff changeset
     2
    Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     3
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     4
Notation and useful facts for working with integrals over a set.
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     5
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     6
TODO: keep all these? Need unicode translations as well.
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     7
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     8
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     9
theory Set_Integral
63941
f353674c2528 move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
hoelzl
parents: 63886
diff changeset
    10
  imports Bochner_Integration
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    11
begin
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    12
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
    13
(*
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    14
    Notation
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    15
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    16
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    17
abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    18
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    19
abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    20
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    21
abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    22
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    23
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    24
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
59358
7fd531cc0172 more line breaks in integral notation
Andreas Lochbihler
parents: 59092
diff changeset
    25
("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    26
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    27
translations
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    28
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    29
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    30
abbreviation
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    31
  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    32
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    33
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    34
  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
59358
7fd531cc0172 more line breaks in integral notation
Andreas Lochbihler
parents: 59092
diff changeset
    35
("AE _\<in>_ in _./ _" [0,0,0,10] 10)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    36
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    37
translations
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    38
  "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    39
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    40
(*
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    41
    Notation for integration wrt lebesgue measure on the reals:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    42
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    43
      LBINT x. f
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    44
      LBINT x : A. f
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    45
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    46
    TODO: keep all these? Need unicode.
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    47
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    48
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    49
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    50
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
59358
7fd531cc0172 more line breaks in integral notation
Andreas Lochbihler
parents: 59092
diff changeset
    51
("(2LBINT _./ _)" [0,60] 60)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    52
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    53
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    54
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
59358
7fd531cc0172 more line breaks in integral notation
Andreas Lochbihler
parents: 59092
diff changeset
    55
("(3LBINT _:_./ _)" [0,60,61] 60)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    56
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
    57
(*
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
    58
    Basic properties
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    59
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    60
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    61
(*
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61880
diff changeset
    62
lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    63
  by (auto simp add: indicator_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    64
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    65
62083
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    66
lemma set_borel_measurable_sets:
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    67
  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    68
  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    69
  shows "f -` B \<inter> X \<in> sets M"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    70
proof -
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    71
  have "f \<in> borel_measurable (restrict_space M X)"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    72
    using assms by (subst borel_measurable_restrict_space_iff) auto
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    73
  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    74
    by (rule measurable_sets) fact
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    75
  with \<open>X \<in> sets M\<close> show ?thesis
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    76
    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    77
qed
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61969
diff changeset
    78
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    79
lemma set_lebesgue_integral_cong:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    80
  assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    81
  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
    82
  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    83
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    84
lemma set_lebesgue_integral_cong_AE:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    85
  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    86
  assumes "AE x \<in> A in M. f x = g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    87
  shows "LINT x:A|M. f x = LINT x:A|M. g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    88
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    89
  have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    90
    using assms by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    91
  thus ?thesis by (intro integral_cong_AE) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    92
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    93
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    94
lemma set_integrable_cong_AE:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    95
    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
    96
    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    97
    set_integrable M A f = set_integrable M A g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    98
  by (rule integrable_cong_AE) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    99
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   100
lemma set_integrable_subset:
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   101
  fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   102
  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   103
  shows "set_integrable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   104
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   105
  have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   106
    by (rule integrable_mult_indicator) fact+
61808
fc1556774cfe isabelle update_cartouches -c -t;
wenzelm
parents: 60615
diff changeset
   107
  with \<open>B \<subseteq> A\<close> show ?thesis
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   108
    by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   109
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   110
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   111
(* TODO: integral_cmul_indicator should be named set_integral_const *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   112
(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   113
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   114
lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   115
  by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   116
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   117
lemma set_integral_mult_right [simp]:
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   118
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   119
  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   120
  by (subst integral_mult_right_zero[symmetric]) auto
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   121
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   122
lemma set_integral_mult_left [simp]:
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   123
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   124
  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   125
  by (subst integral_mult_left_zero[symmetric]) auto
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   126
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   127
lemma set_integral_divide_zero [simp]:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59358
diff changeset
   128
  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   129
  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   130
  by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   131
     (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   132
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   133
lemma set_integrable_scaleR_right [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   134
  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   135
  unfolding scaleR_left_commute by (rule integrable_scaleR_right)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   136
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   137
lemma set_integrable_scaleR_left [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   138
  fixes a :: "_ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   139
  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   140
  using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   141
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   142
lemma set_integrable_mult_right [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   143
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   144
  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   145
  using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   146
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   147
lemma set_integrable_mult_left [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   148
  fixes a :: "'a::{real_normed_field, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   149
  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   150
  using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   151
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   152
lemma set_integrable_divide [simp, intro]:
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59358
diff changeset
   153
  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   154
  assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   155
  shows "set_integrable M A (\<lambda>t. f t / a)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   156
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   157
  have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   158
    using assms by (rule integrable_divide_zero)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   159
  also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   160
    by (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   161
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   162
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   163
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   164
lemma set_integral_add [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   165
  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   166
  assumes "set_integrable M A f" "set_integrable M A g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   167
  shows "set_integrable M A (\<lambda>x. f x + g x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   168
    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   169
  using assms by (simp_all add: scaleR_add_right)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   170
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   171
lemma set_integral_diff [simp, intro]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   172
  assumes "set_integrable M A f" "set_integrable M A g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   173
  shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   174
    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   175
  using assms by (simp_all add: scaleR_diff_right)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   176
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   177
(* question: why do we have this for negation, but multiplication by a constant
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   178
   requires an integrability assumption? *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   179
lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   180
  by (subst integral_minus[symmetric]) simp_all
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   181
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   182
lemma set_integral_complex_of_real:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   183
  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   184
  by (subst integral_complex_of_real[symmetric])
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   185
     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   186
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   187
lemma set_integral_mono:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   188
  fixes f g :: "_ \<Rightarrow> real"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   189
  assumes "set_integrable M A f" "set_integrable M A g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   190
    "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   191
  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   192
using assms by (auto intro: integral_mono split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   193
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   194
lemma set_integral_mono_AE:
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   195
  fixes f g :: "_ \<Rightarrow> real"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   196
  assumes "set_integrable M A f" "set_integrable M A g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   197
    "AE x \<in> A in M. f x \<le> g x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   198
  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   199
using assms by (auto intro: integral_mono_AE split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   200
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   201
lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   202
  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   203
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   204
lemma set_integrable_abs_iff:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   205
  fixes f :: "_ \<Rightarrow> real"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   206
  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   207
  by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   208
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   209
lemma set_integrable_abs_iff':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   210
  fixes f :: "_ \<Rightarrow> real"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   211
  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   212
    set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   213
by (intro set_integrable_abs_iff) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   214
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   215
lemma set_integrable_discrete_difference:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   216
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   217
  assumes "countable X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   218
  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   219
  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   220
  shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   221
proof (rule integrable_discrete_difference[where X=X])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   222
  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   223
    using diff by (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   224
qed fact+
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   225
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   226
lemma set_integral_discrete_difference:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   227
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   228
  assumes "countable X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   229
  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   230
  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   231
  shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   232
proof (rule integral_discrete_difference[where X=X])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   233
  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   234
    using diff by (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   235
qed fact+
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   236
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   237
lemma set_integrable_Un:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   238
  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   239
  assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   240
    and [measurable]: "A \<in> sets M" "B \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   241
  shows "set_integrable M (A \<union> B) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   242
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   243
  have "set_integrable M (A - B) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   244
    using f_A by (rule set_integrable_subset) auto
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   245
  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   246
    by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   247
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   248
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   249
lemma set_integrable_UN:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   250
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   251
  assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   252
    "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   253
  shows "set_integrable M (\<Union>i\<in>I. A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   254
using assms by (induct I) (auto intro!: set_integrable_Un)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   255
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   256
lemma set_integral_Un:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   257
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   258
  assumes "A \<inter> B = {}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   259
  and "set_integrable M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   260
  and "set_integrable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   261
  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   262
by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   263
      scaleR_add_left assms)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   264
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   265
lemma set_integral_cong_set:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   266
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   267
  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   268
    and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   269
  shows "LINT x:B|M. f x = LINT x:A|M. f x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   270
proof (rule integral_cong_AE)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   271
  show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   272
    using ae by (auto simp: subset_eq split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   273
qed fact+
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   274
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   275
lemma set_borel_measurable_subset:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   276
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   277
  assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   278
  shows "set_borel_measurable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   279
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   280
  have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   281
    by measurable
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   282
  also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
61808
fc1556774cfe isabelle update_cartouches -c -t;
wenzelm
parents: 60615
diff changeset
   283
    using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   284
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   285
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   286
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   287
lemma set_integral_Un_AE:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   288
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   289
  assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   290
  and "set_integrable M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   291
  and "set_integrable M B f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   292
  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   293
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   294
  have f: "set_integrable M (A \<union> B) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   295
    by (intro set_integrable_Un assms)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   296
  then have f': "set_borel_measurable M (A \<union> B) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   297
    by (rule borel_measurable_integrable)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   298
  have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   299
  proof (rule set_integral_cong_set)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   300
    show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   301
      using ae by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   302
    show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   303
      using f' by (rule set_borel_measurable_subset) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   304
  qed fact
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   305
  also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   306
    by (auto intro!: set_integral_Un set_integrable_subset[OF f])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   307
  also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   308
    using ae
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   309
    by (intro arg_cong2[where f="op+"] set_integral_cong_set)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   310
       (auto intro!: set_borel_measurable_subset[OF f'])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   311
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   312
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   313
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   314
lemma set_integral_finite_Union:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   315
  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   316
  assumes "finite I" "disjoint_family_on A I"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   317
    and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   318
  shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   319
  using assms
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   320
  apply induct
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   321
  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   322
by (subst set_integral_Un, auto intro: set_integrable_UN)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   323
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   324
(* TODO: find a better name? *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   325
lemma pos_integrable_to_top:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   326
  fixes l::real
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   327
  assumes "\<And>i. A i \<in> sets M" "mono A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   328
  assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   329
  and intgbl: "\<And>i::nat. set_integrable M (A i) f"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   330
  and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   331
  shows "set_integrable M (\<Union>i. A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   332
  apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   333
  apply (rule intgbl)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   334
  prefer 3 apply (rule lim)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   335
  apply (rule AE_I2)
61808
fc1556774cfe isabelle update_cartouches -c -t;
wenzelm
parents: 60615
diff changeset
   336
  using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   337
proof (rule AE_I2)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   338
  { fix x assume "x \<in> space M"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   339
    show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   340
    proof cases
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   341
      assume "\<exists>i. x \<in> A i"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   342
      then guess i ..
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   343
      then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
61808
fc1556774cfe isabelle update_cartouches -c -t;
wenzelm
parents: 60615
diff changeset
   344
        using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   345
      show ?thesis
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   346
        apply (intro Lim_eventually)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   347
        using *
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   348
        apply eventually_elim
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   349
        apply (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   350
        done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   351
    qed auto }
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   352
  then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
62624
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62083
diff changeset
   353
    apply (rule borel_measurable_LIMSEQ_real)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   354
    apply assumption
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   355
    apply (intro borel_measurable_integrable intgbl)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   356
    done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   357
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   358
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   359
(* Proof from Royden Real Analysis, p. 91. *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   360
lemma lebesgue_integral_countable_add:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   361
  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   362
  assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   363
    and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   364
    and intgbl: "set_integrable M (\<Union>i. A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   365
  shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   366
proof (subst integral_suminf[symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   367
  show int_A: "\<And>i. set_integrable M (A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   368
    using intgbl by (rule set_integrable_subset) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   369
  { fix x assume "x \<in> space M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   370
    have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   371
      by (intro sums_scaleR_left indicator_sums) fact }
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   372
  note sums = this
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   373
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   374
  have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   375
    using int_A[THEN integrable_norm] by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   376
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   377
  show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   378
    using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   379
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   380
  show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   381
  proof (rule summableI_nonneg_bounded)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   382
    fix n
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   383
    show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   384
      using norm_f by (auto intro!: integral_nonneg_AE)
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   385
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   386
    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   387
      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   388
      by (simp add: abs_mult)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   389
    also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   390
      using norm_f
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   391
      by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   392
    also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   393
      using intgbl[THEN integrable_norm]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   394
      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   395
         (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   396
    finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   397
      set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   398
      by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   399
  qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   400
  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
63886
685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents: 63627
diff changeset
   401
    apply (rule Bochner_Integration.integral_cong[OF refl])
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   402
    apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   403
    using sums_unique[OF indicator_sums[OF disj]]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   404
    apply auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   405
    done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   406
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   407
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   408
lemma set_integral_cont_up:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   409
  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   410
  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   411
  and intgbl: "set_integrable M (\<Union>i. A i) f"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   412
  shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   413
proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   414
  have int_A: "\<And>i. set_integrable M (A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   415
    using intgbl by (rule set_integrable_subset) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   416
  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   417
    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   418
    using intgbl integrable_norm[OF intgbl] by auto
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   419
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   420
  { fix x i assume "x \<in> A i"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   421
    with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   422
      by (intro filterlim_cong refl)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   423
         (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   424
  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   425
    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   426
qed (auto split: split_indicator)
60615
e5fa1d5d3952 Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   427
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   428
(* Can the int0 hypothesis be dropped? *)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   429
lemma set_integral_cont_down:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   430
  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   431
  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   432
  and int0: "set_integrable M (A 0) f"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   433
  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   434
proof (rule integral_dominated_convergence)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   435
  have int_A: "\<And>i. set_integrable M (A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   436
    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   437
  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   438
    using int0[THEN integrable_norm] by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   439
  have "set_integrable M (\<Inter>i. A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   440
    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   441
  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   442
    by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   443
  show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   444
    using A by (auto split: split_indicator simp: decseq_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   445
  { fix x i assume "x \<in> space M" "x \<notin> A i"
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   446
    with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   447
      by (intro filterlim_cong refl)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   448
         (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
61969
e01015e49041 more symbols;
wenzelm
parents: 61945
diff changeset
   449
  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   450
    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   451
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   452
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   453
lemma set_integral_at_point:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   454
  fixes a :: real
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   455
  assumes "set_integrable M {a} f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   456
  and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   457
  shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   458
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   459
  have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   460
    by (intro set_lebesgue_integral_cong) simp_all
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   461
  then show ?thesis using assms by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   462
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   463
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   464
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   465
abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   466
  "complex_integrable M f \<equiv> integrable M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   467
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   468
abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   469
  "integral\<^sup>C M f == integral\<^sup>L M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   470
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   471
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   472
  "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   473
 ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   474
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   475
translations
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   476
  "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   477
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   478
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   479
  "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   480
  ("(3CLINT _|_. _)" [0,110,60] 60)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   481
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   482
translations
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   483
  "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   484
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   485
lemma complex_integrable_cnj [simp]:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   486
  "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   487
proof
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   488
  assume "complex_integrable M (\<lambda>x. cnj (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   489
  then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   490
    by (rule integrable_cnj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   491
  then show "complex_integrable M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   492
    by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   493
qed simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   494
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   495
lemma complex_of_real_integrable_eq:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   496
  "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   497
proof
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   498
  assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   499
  then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   500
    by (rule integrable_Re)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   501
  then show "integrable M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   502
    by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   503
qed simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   504
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   505
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   506
abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   507
  "complex_set_integrable M A f \<equiv> set_integrable M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   508
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   509
abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   510
  "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   511
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   512
syntax
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   513
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   514
("(4CLINT _:_|_. _)" [0,60,110,61] 60)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   515
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   516
translations
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   517
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   518
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   519
lemma set_borel_measurable_continuous:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   520
  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   521
  assumes "S \<in> sets borel" "continuous_on S f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   522
  shows "set_borel_measurable borel S f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   523
proof -
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   524
  have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   525
    by (intro assms borel_measurable_continuous_on_if continuous_on_const)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   526
  also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   527
    by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   528
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   529
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   530
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   531
lemma set_measurable_continuous_on_ivl:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   532
  assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   533
  shows "set_borel_measurable borel {a..b} f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   534
  by (rule set_borel_measurable_continuous[OF _ assms]) simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   535
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   536
end
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   537