author  hoelzl 
Tue, 20 May 2014 19:24:39 +0200  
changeset 57025  e7fd64f82876 
parent 56996  891e992e510f 
child 57036  22568fb89165 
permissions  rwrr 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1 
(* Title: HOL/Probability/Bochner_Integration.thy 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

2 
Author: Johannes Hölzl, TU München 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

3 
*) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

4 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

5 
header {* Bochner Integration for VectorValued Functions *} 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

6 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

7 
theory Bochner_Integration 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

8 
imports Finite_Product_Measure 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

9 
begin 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

10 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

11 
text {* 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

12 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

13 
In the following development of the Bochner integral we use second countable topologies instead 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

14 
of separable spaces. A second countable topology is also separable. 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

15 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

16 
*} 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

17 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

18 
lemma borel_measurable_implies_sequence_metric: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

19 
fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

20 
assumes [measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

21 
shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) > f x) \<and> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

22 
(\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

23 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

24 
obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

25 
by (erule countable_dense_setE) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

26 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

27 
def e \<equiv> "from_nat_into D" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

28 
{ fix n x 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

29 
obtain d where "d \<in> D" and d: "d \<in> ball x (1 / Suc n)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

30 
using D[of "ball x (1 / Suc n)"] by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

31 
from `d \<in> D` D[of UNIV] `countable D` obtain i where "d = e i" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

32 
unfolding e_def by (auto dest: from_nat_into_surj) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

33 
with d have "\<exists>i. dist x (e i) < 1 / Suc n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

34 
by auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

35 
note e = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

36 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

37 
def A \<equiv> "\<lambda>m n. {x\<in>space M. dist (f x) (e n) < 1 / (Suc m) \<and> 1 / (Suc m) \<le> dist (f x) z}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

38 
def B \<equiv> "\<lambda>m. disjointed (A m)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

39 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

40 
def m \<equiv> "\<lambda>N x. Max {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

41 
def F \<equiv> "\<lambda>N::nat. \<lambda>x. if (\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)) \<and> (\<exists>n\<le>N. x \<in> B (m N x) n) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

42 
then e (LEAST n. x \<in> B (m N x) n) else z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

43 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

44 
have B_imp_A[intro, simp]: "\<And>x m n. x \<in> B m n \<Longrightarrow> x \<in> A m n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

45 
using disjointed_subset[of "A m" for m] unfolding B_def by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

46 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

47 
{ fix m 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

48 
have "\<And>n. A m n \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

49 
by (auto simp: A_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

50 
then have "\<And>n. B m n \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

51 
using sets.range_disjointed_sets[of "A m" M] by (auto simp: B_def) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

52 
note this[measurable] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

53 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

54 
{ fix N i x assume "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

55 
then have "m N x \<in> {m::nat. m \<le> N \<and> x \<in> (\<Union>n\<le>N. B m n)}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

56 
unfolding m_def by (intro Max_in) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

57 
then have "m N x \<le> N" "\<exists>n\<le>N. x \<in> B (m N x) n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

58 
by auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

59 
note m = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

60 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

61 
{ fix j N i x assume "j \<le> N" "i \<le> N" "x \<in> B j i" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

62 
then have "j \<le> m N x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

63 
unfolding m_def by (intro Max_ge) auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

64 
note m_upper = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

65 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

66 
show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

67 
unfolding simple_function_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

68 
proof (safe intro!: exI[of _ F]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

69 
have [measurable]: "\<And>i. F i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

70 
unfolding F_def m_def by measurable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

71 
show "\<And>x i. F i ` {x} \<inter> space M \<in> sets M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

72 
by measurable 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

73 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

74 
{ fix i 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

75 
{ fix n x assume "x \<in> B (m i x) n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

76 
then have "(LEAST n. x \<in> B (m i x) n) \<le> n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

77 
by (intro Least_le) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

78 
also assume "n \<le> i" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

79 
finally have "(LEAST n. x \<in> B (m i x) n) \<le> i" . } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

80 
then have "F i ` space M \<subseteq> {z} \<union> e ` {.. i}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

81 
by (auto simp: F_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

82 
then show "finite (F i ` space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

83 
by (rule finite_subset) auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

84 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

85 
{ fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

86 
then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

87 
from m[OF this] obtain n where n: "m N x \<le> N" "n \<le> N" "x \<in> B (m N x) n" by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

88 
moreover 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

89 
def L \<equiv> "LEAST n. x \<in> B (m N x) n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

90 
have "dist (f x) (e L) < 1 / Suc (m N x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

91 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

92 
have "x \<in> B (m N x) L" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

93 
using n(3) unfolding L_def by (rule LeastI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

94 
then have "x \<in> A (m N x) L" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

95 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

96 
then show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

97 
unfolding A_def by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

98 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

99 
ultimately have "dist (f x) (F N x) < 1 / Suc (m N x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

100 
by (auto simp add: F_def L_def) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

101 
note * = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

102 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

103 
fix x assume "x \<in> space M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

104 
show "(\<lambda>i. F i x) > f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

105 
proof cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

106 
assume "f x = z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

107 
then have "\<And>i n. x \<notin> A i n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

108 
unfolding A_def by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

109 
then have "\<And>i. F i x = z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

110 
by (auto simp: F_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

111 
then show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

112 
using `f x = z` by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

113 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

114 
assume "f x \<noteq> z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

115 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

116 
show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

117 
proof (rule tendstoI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

118 
fix e :: real assume "0 < e" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

119 
with `f x \<noteq> z` obtain n where "1 / Suc n < e" "1 / Suc n < dist (f x) z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

120 
by (metis dist_nz order_less_trans neq_iff nat_approx_posE) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

121 
with `x\<in>space M` `f x \<noteq> z` have "x \<in> (\<Union>i. B n i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

122 
unfolding A_def B_def UN_disjointed_eq using e by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

123 
then obtain i where i: "x \<in> B n i" by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

124 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

125 
show "eventually (\<lambda>i. dist (F i x) (f x) < e) sequentially" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

126 
using eventually_ge_at_top[of "max n i"] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

127 
proof eventually_elim 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

128 
fix j assume j: "max n i \<le> j" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

129 
with i have "dist (f x) (F j x) < 1 / Suc (m j x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

130 
by (intro *[OF _ _ i]) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

131 
also have "\<dots> \<le> 1 / Suc n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

132 
using j m_upper[OF _ _ i] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

133 
by (auto simp: field_simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

134 
also note `1 / Suc n < e` 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

135 
finally show "dist (F j x) (f x) < e" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

136 
by (simp add: less_imp_le dist_commute) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

137 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

138 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

139 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

140 
fix i 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

141 
{ fix n m assume "x \<in> A n m" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

142 
then have "dist (e m) (f x) + dist (f x) z \<le> 2 * dist (f x) z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

143 
unfolding A_def by (auto simp: dist_commute) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

144 
also have "dist (e m) z \<le> dist (e m) (f x) + dist (f x) z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

145 
by (rule dist_triangle) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

146 
finally (xtrans) have "dist (e m) z \<le> 2 * dist (f x) z" . } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

147 
then show "dist (F i x) z \<le> 2 * dist (f x) z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

148 
unfolding F_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

149 
apply auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

150 
apply (rule LeastI2) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

151 
apply auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

152 
done 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

153 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

154 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

155 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

156 
lemma real_indicator: "real (indicator A x :: ereal) = indicator A x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

157 
unfolding indicator_def by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

158 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

159 
lemma split_indicator_asm: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

160 
"P (indicator S x) \<longleftrightarrow> \<not> ((x \<in> S \<and> \<not> P 1) \<or> (x \<notin> S \<and> \<not> P 0))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

161 
unfolding indicator_def by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

162 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

163 
lemma 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

164 
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

165 
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

166 
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

167 
unfolding indicator_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

168 
using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

169 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

170 
lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

171 
fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

172 
assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

173 
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

174 
assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

175 
assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

176 
assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. U i x) > u x) \<Longrightarrow> P u" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

177 
shows "P u" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

178 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

179 
have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M" using u by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

180 
from borel_measurable_implies_simple_function_sequence'[OF this] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

181 
obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

182 
sup: "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

183 
by blast 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

184 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

185 
def U' \<equiv> "\<lambda>i x. indicator (space M) x * real (U i x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

186 
then have U'_sf[measurable]: "\<And>i. simple_function M (U' i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

187 
using U by (auto intro!: simple_function_compose1[where g=real]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

188 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

189 
show "P u" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

190 
proof (rule seq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

191 
fix i show "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

192 
using U nn by (auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

193 
intro: borel_measurable_simple_function 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

194 
intro!: borel_measurable_real_of_ereal real_of_ereal_pos borel_measurable_times 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

195 
simp: U'_def zero_le_mult_iff) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

196 
show "incseq U'" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

197 
using U(2,3) nn 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

198 
by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

199 
intro!: real_of_ereal_positive_mono) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

200 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

201 
fix x assume x: "x \<in> space M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

202 
have "(\<lambda>i. U i x) > (SUP i. U i x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

203 
using U(2) by (intro LIMSEQ_SUP) (auto simp: incseq_def le_fun_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

204 
moreover have "(\<lambda>i. U i x) = (\<lambda>i. ereal (U' i x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

205 
using x nn U(3) by (auto simp: fun_eq_iff U'_def ereal_real image_iff eq_commute) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

206 
moreover have "(SUP i. U i x) = ereal (u x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

207 
using sup u(2) by (simp add: max_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

208 
ultimately show "(\<lambda>i. U' i x) > u x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

209 
by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

210 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

211 
fix i 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

212 
have "U' i ` space M \<subseteq> real ` (U i ` space M)" "finite (U i ` space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

213 
unfolding U'_def using U(1) by (auto dest: simple_functionD) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

214 
then have fin: "finite (U' i ` space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

215 
by (metis finite_subset finite_imageI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

216 
moreover have "\<And>z. {y. U' i z = y \<and> y \<in> U' i ` space M \<and> z \<in> space M} = (if z \<in> space M then {U' i z} else {})" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

217 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

218 
ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

219 
by (simp add: U'_def fun_eq_iff) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

220 
have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

221 
using nn by (auto simp: U'_def real_of_ereal_pos) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

222 
with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

223 
proof induct 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

224 
case empty from set[of "{}"] show ?case 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

225 
by (simp add: indicator_def[abs_def]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

226 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

227 
case (insert x F) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

228 
then show ?case 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

229 
by (auto intro!: add mult set setsum_nonneg split: split_indicator split_indicator_asm 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

230 
simp del: setsum_mult_indicator simp: setsum_nonneg_eq_0_iff ) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

231 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

232 
with U' show "P (U' i)" by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

233 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

234 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

235 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

236 
lemma scaleR_cong_right: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

237 
fixes x :: "'a :: real_vector" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

238 
shows "(x \<noteq> 0 \<Longrightarrow> r = p) \<Longrightarrow> r *\<^sub>R x = p *\<^sub>R x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

239 
by (cases "x = 0") auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

240 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

241 
inductive simple_bochner_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" for M f where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

242 
"simple_function M f \<Longrightarrow> emeasure M {y\<in>space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

243 
simple_bochner_integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

244 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

245 
lemma simple_bochner_integrable_compose2: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

246 
assumes p_0: "p 0 0 = 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

247 
shows "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integrable M g \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

248 
simple_bochner_integrable M (\<lambda>x. p (f x) (g x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

249 
proof (safe intro!: simple_bochner_integrable.intros elim!: simple_bochner_integrable.cases del: notI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

250 
assume sf: "simple_function M f" "simple_function M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

251 
then show "simple_function M (\<lambda>x. p (f x) (g x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

252 
by (rule simple_function_compose2) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

253 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

254 
from sf have [measurable]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

255 
"f \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

256 
"g \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

257 
by (auto intro: measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

258 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

259 
assume fin: "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" "emeasure M {y \<in> space M. g y \<noteq> 0} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

260 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

261 
have "emeasure M {x\<in>space M. p (f x) (g x) \<noteq> 0} \<le> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

262 
emeasure M ({x\<in>space M. f x \<noteq> 0} \<union> {x\<in>space M. g x \<noteq> 0})" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

263 
by (intro emeasure_mono) (auto simp: p_0) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

264 
also have "\<dots> \<le> emeasure M {x\<in>space M. f x \<noteq> 0} + emeasure M {x\<in>space M. g x \<noteq> 0}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

265 
by (intro emeasure_subadditive) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

266 
finally show "emeasure M {y \<in> space M. p (f y) (g y) \<noteq> 0} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

267 
using fin by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

268 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

269 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

270 
lemma simple_function_finite_support: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

271 
assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and nn: "\<And>x. 0 \<le> f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

272 
shows "emeasure M {x\<in>space M. f x \<noteq> 0} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

273 
proof cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

274 
from f have meas[measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

275 
by (rule borel_measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

276 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

277 
assume non_empty: "\<exists>x\<in>space M. f x \<noteq> 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

278 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

279 
def m \<equiv> "Min (f`space M  {0})" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

280 
have "m \<in> f`space M  {0}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

281 
unfolding m_def using f non_empty by (intro Min_in) (auto simp: simple_function_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

282 
then have m: "0 < m" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

283 
using nn by (auto simp: less_le) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

284 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

285 
from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

286 
(\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)" 
56996  287 
using f by (intro nn_integral_cmult_indicator[symmetric]) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

288 
also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

289 
using AE_space 
56996  290 
proof (intro nn_integral_mono_AE, eventually_elim) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

291 
fix x assume "x \<in> space M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

292 
with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

293 
using f by (auto split: split_indicator simp: simple_function_def m_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

294 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

295 
also note `\<dots> < \<infinity>` 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

296 
finally show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

297 
using m by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

298 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

299 
assume "\<not> (\<exists>x\<in>space M. f x \<noteq> 0)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

300 
with nn have *: "{x\<in>space M. f x \<noteq> 0} = {}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

301 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

302 
show ?thesis unfolding * by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

303 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

304 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

305 
lemma simple_bochner_integrableI_bounded: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

306 
assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

307 
shows "simple_bochner_integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

308 
proof 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

309 
have "emeasure M {y \<in> space M. ereal (norm (f y)) \<noteq> 0} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

310 
proof (rule simple_function_finite_support) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

311 
show "simple_function M (\<lambda>x. ereal (norm (f x)))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

312 
using f by (rule simple_function_compose1) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

313 
show "(\<integral>\<^sup>+ y. ereal (norm (f y)) \<partial>M) < \<infinity>" by fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

314 
qed simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

315 
then show "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

316 
qed fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

317 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

318 
definition simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

319 
"simple_bochner_integral M f = (\<Sum>y\<in>f`space M. measure M {x\<in>space M. f x = y} *\<^sub>R y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

320 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

321 
lemma simple_bochner_integral_partition: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

322 
assumes f: "simple_bochner_integrable M f" and g: "simple_function M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

323 
assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

324 
assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

325 
shows "simple_bochner_integral M f = (\<Sum>y\<in>g ` space M. measure M {x\<in>space M. g x = y} *\<^sub>R v y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

326 
(is "_ = ?r") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

327 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

328 
from f g have [simp]: "finite (f`space M)" "finite (g`space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

329 
by (auto simp: simple_function_def elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

330 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

331 
from f have [measurable]: "f \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

332 
by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

333 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

334 
from g have [measurable]: "g \<in> measurable M (count_space UNIV)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

335 
by (auto intro: measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

336 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

337 
{ fix y assume "y \<in> space M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

338 
then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

339 
by (auto cong: sub simp: v[symmetric]) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

340 
note eq = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

341 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

342 
have "simple_bochner_integral M f = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

343 
(\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

344 
if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} else 0) *\<^sub>R y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

345 
unfolding simple_bochner_integral_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

346 
proof (safe intro!: setsum_cong scaleR_cong_right) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

347 
fix y assume y: "y \<in> space M" "f y \<noteq> 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

348 
have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

349 
{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

350 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

351 
have eq:"{x \<in> space M. f x = f y} = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

352 
(\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i})" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

353 
by (auto simp: eq_commute cong: sub rev_conj_cong) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

354 
have "finite (g`space M)" by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

355 
then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

356 
by (rule rev_finite_subset) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

357 
moreover 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

358 
{ fix x assume "x \<in> space M" "f x = f y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

359 
then have "x \<in> space M" "f x \<noteq> 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

360 
using y by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

361 
then have "emeasure M {y \<in> space M. g y = g x} \<le> emeasure M {y \<in> space M. f y \<noteq> 0}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

362 
by (auto intro!: emeasure_mono cong: sub) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

363 
then have "emeasure M {xa \<in> space M. g xa = g x} < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

364 
using f by (auto simp: simple_bochner_integrable.simps) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

365 
ultimately 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

366 
show "measure M {x \<in> space M. f x = f y} = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

367 
(\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then measure M {x \<in> space M. g x = z} else 0)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

368 
apply (simp add: setsum_cases eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

369 
apply (subst measure_finite_Union[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

370 
apply (auto simp: disjoint_family_on_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

371 
done 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

372 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

373 
also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

374 
if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} *\<^sub>R y else 0))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

375 
by (auto intro!: setsum_cong simp: scaleR_setsum_left) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

376 
also have "\<dots> = ?r" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

377 
by (subst setsum_commute) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

378 
(auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

379 
finally show "simple_bochner_integral M f = ?r" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

380 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

381 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

382 
lemma simple_bochner_integral_add: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

383 
assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

384 
shows "simple_bochner_integral M (\<lambda>x. f x + g x) = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

385 
simple_bochner_integral M f + simple_bochner_integral M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

386 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

387 
from f g have "simple_bochner_integral M (\<lambda>x. f x + g x) = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

388 
(\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R (fst y + snd y))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

389 
by (intro simple_bochner_integral_partition) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

390 
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

391 
moreover from f g have "simple_bochner_integral M f = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

392 
(\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R fst y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

393 
by (intro simple_bochner_integral_partition) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

394 
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

395 
moreover from f g have "simple_bochner_integral M g = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

396 
(\<Sum>y\<in>(\<lambda>x. (f x, g x)) ` space M. measure M {x \<in> space M. (f x, g x) = y} *\<^sub>R snd y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

397 
by (intro simple_bochner_integral_partition) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

398 
(auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

399 
ultimately show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

400 
by (simp add: setsum_addf[symmetric] scaleR_add_right) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

401 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

402 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

403 
lemma (in linear) simple_bochner_integral_linear: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

404 
assumes g: "simple_bochner_integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

405 
shows "simple_bochner_integral M (\<lambda>x. f (g x)) = f (simple_bochner_integral M g)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

406 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

407 
from g have "simple_bochner_integral M (\<lambda>x. f (g x)) = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

408 
(\<Sum>y\<in>g ` space M. measure M {x \<in> space M. g x = y} *\<^sub>R f y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

409 
by (intro simple_bochner_integral_partition) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

410 
(auto simp: simple_bochner_integrable_compose2[where p="\<lambda>x y. f x"] zero 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

411 
elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

412 
also have "\<dots> = f (simple_bochner_integral M g)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

413 
by (simp add: simple_bochner_integral_def setsum scaleR) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

414 
finally show ?thesis . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

415 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

416 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

417 
lemma simple_bochner_integral_minus: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

418 
assumes f: "simple_bochner_integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

419 
shows "simple_bochner_integral M (\<lambda>x.  f x) =  simple_bochner_integral M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

420 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

421 
interpret linear uminus by unfold_locales auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

422 
from f show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

423 
by (rule simple_bochner_integral_linear) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

424 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

425 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

426 
lemma simple_bochner_integral_diff: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

427 
assumes f: "simple_bochner_integrable M f" and g: "simple_bochner_integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

428 
shows "simple_bochner_integral M (\<lambda>x. f x  g x) = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

429 
simple_bochner_integral M f  simple_bochner_integral M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

430 
unfolding diff_conv_add_uminus using f g 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

431 
by (subst simple_bochner_integral_add) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

432 
(auto simp: simple_bochner_integral_minus simple_bochner_integrable_compose2[where p="\<lambda>x y.  y"]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

433 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

434 
lemma simple_bochner_integral_norm_bound: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

435 
assumes f: "simple_bochner_integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

436 
shows "norm (simple_bochner_integral M f) \<le> simple_bochner_integral M (\<lambda>x. norm (f x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

437 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

438 
have "norm (simple_bochner_integral M f) \<le> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

439 
(\<Sum>y\<in>f ` space M. norm (measure M {x \<in> space M. f x = y} *\<^sub>R y))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

440 
unfolding simple_bochner_integral_def by (rule norm_setsum) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

441 
also have "\<dots> = (\<Sum>y\<in>f ` space M. measure M {x \<in> space M. f x = y} *\<^sub>R norm y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

442 
by (simp add: measure_nonneg) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

443 
also have "\<dots> = simple_bochner_integral M (\<lambda>x. norm (f x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

444 
using f 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

445 
by (intro simple_bochner_integral_partition[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

446 
(auto intro: f simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

447 
finally show ?thesis . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

448 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

449 

56996  450 
lemma simple_bochner_integral_eq_nn_integral: 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

451 
assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

452 
shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

453 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

454 
{ fix x y z have "(x \<noteq> 0 \<Longrightarrow> y = z) \<Longrightarrow> ereal x * y = ereal x * z" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

455 
by (cases "x = 0") (auto simp: zero_ereal_def[symmetric]) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

456 
note ereal_cong_mult = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

457 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

458 
have [measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

459 
using f(1) by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

460 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

461 
{ fix y assume y: "y \<in> space M" "f y \<noteq> 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

462 
have "ereal (measure M {x \<in> space M. f x = f y}) = emeasure M {x \<in> space M. f x = f y}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

463 
proof (rule emeasure_eq_ereal_measure[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

464 
have "emeasure M {x \<in> space M. f x = f y} \<le> emeasure M {x \<in> space M. f x \<noteq> 0}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

465 
using y by (intro emeasure_mono) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

466 
with f show "emeasure M {x \<in> space M. f x = f y} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

467 
by (auto simp: simple_bochner_integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

468 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

469 
moreover have "{x \<in> space M. f x = f y} = (\<lambda>x. ereal (f x)) ` {ereal (f y)} \<inter> space M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

470 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

471 
ultimately have "ereal (measure M {x \<in> space M. f x = f y}) = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

472 
emeasure M ((\<lambda>x. ereal (f x)) ` {ereal (f y)} \<inter> space M)" by simp } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

473 
with f have "simple_bochner_integral M f = (\<integral>\<^sup>Sx. f x \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

474 
unfolding simple_integral_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

475 
by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

476 
(auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

477 
intro!: setsum_cong ereal_cong_mult 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

478 
simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

479 
simp del: setsum_ereal times_ereal.simps(1)) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

480 
also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

481 
using f 
56996  482 
by (intro nn_integral_eq_simple_integral[symmetric]) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

483 
(auto simp: simple_function_compose1 simple_bochner_integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

484 
finally show ?thesis . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

485 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

486 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

487 
lemma simple_bochner_integral_bounded: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

488 
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

489 
assumes f[measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

490 
assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

491 
shows "ereal (norm (simple_bochner_integral M s  simple_bochner_integral M t)) \<le> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

492 
(\<integral>\<^sup>+ x. norm (f x  s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x  t x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

493 
(is "ereal (norm (?s  ?t)) \<le> ?S + ?T") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

494 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

495 
have [measurable]: "s \<in> borel_measurable M" "t \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

496 
using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

497 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

498 
have "ereal (norm (?s  ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x  t x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

499 
using s t by (subst simple_bochner_integral_diff) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

500 
also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x  t x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

501 
using simple_bochner_integrable_compose2[of "op " M "s" "t"] s t 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

502 
by (auto intro!: simple_bochner_integral_norm_bound) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

503 
also have "\<dots> = (\<integral>\<^sup>+x. norm (s x  t x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

504 
using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x  y)" M "s" "t"] s t 
56996  505 
by (auto intro!: simple_bochner_integral_eq_nn_integral) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

506 
also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x  s x)) + ereal (norm (f x  t x)) \<partial>M)" 
56996  507 
by (auto intro!: nn_integral_mono) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

508 
(metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

509 
norm_minus_commute norm_triangle_ineq4 order_refl) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

510 
also have "\<dots> = ?S + ?T" 
56996  511 
by (rule nn_integral_add) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

512 
finally show ?thesis . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

513 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

514 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

515 
inductive has_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::{real_normed_vector, second_countable_topology} \<Rightarrow> bool" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

516 
for M f x where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

517 
"f \<in> borel_measurable M \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

518 
(\<And>i. simple_bochner_integrable M (s i)) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

519 
(\<lambda>i. \<integral>\<^sup>+x. norm (f x  s i x) \<partial>M) > 0 \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

520 
(\<lambda>i. simple_bochner_integral M (s i)) > x \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

521 
has_bochner_integral M f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

522 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

523 
lemma has_bochner_integral_cong: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

524 
assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

525 
shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

526 
unfolding has_bochner_integral.simps assms(1,3) 
56996  527 
using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

528 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

529 
lemma has_bochner_integral_cong_AE: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

530 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

531 
has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

532 
unfolding has_bochner_integral.simps 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

533 
by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x > 0"] 
56996  534 
nn_integral_cong_AE) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

535 
auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

536 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

537 
lemma borel_measurable_has_bochner_integral[measurable_dest]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

538 
"has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

539 
by (auto elim: has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

540 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

541 
lemma has_bochner_integral_simple_bochner_integrable: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

542 
"simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

543 
by (rule has_bochner_integral.intros[where s="\<lambda>_. f"]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

544 
(auto intro: borel_measurable_simple_function 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

545 
elim: simple_bochner_integrable.cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

546 
simp: zero_ereal_def[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

547 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

548 
lemma has_bochner_integral_real_indicator: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

549 
assumes [measurable]: "A \<in> sets M" and A: "emeasure M A < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

550 
shows "has_bochner_integral M (indicator A) (measure M A)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

551 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

552 
have sbi: "simple_bochner_integrable M (indicator A::'a \<Rightarrow> real)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

553 
proof 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

554 
have "{y \<in> space M. (indicator A y::real) \<noteq> 0} = A" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

555 
using sets.sets_into_space[OF `A\<in>sets M`] by (auto split: split_indicator) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

556 
then show "emeasure M {y \<in> space M. (indicator A y::real) \<noteq> 0} \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

557 
using A by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

558 
qed (rule simple_function_indicator assms)+ 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

559 
moreover have "simple_bochner_integral M (indicator A) = measure M A" 
56996  560 
using simple_bochner_integral_eq_nn_integral[OF sbi] A 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

561 
by (simp add: ereal_indicator emeasure_eq_ereal_measure) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

562 
ultimately show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

563 
by (metis has_bochner_integral_simple_bochner_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

564 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

565 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

566 
lemma has_bochner_integral_add: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

567 
"has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

568 
has_bochner_integral M (\<lambda>x. f x + g x) (x + y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

569 
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

570 
fix sf sg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

571 
assume f_sf: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x  sf i x) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

572 
assume g_sg: "(\<lambda>i. \<integral>\<^sup>+ x. norm (g x  sg i x) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

573 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

574 
assume sf: "\<forall>i. simple_bochner_integrable M (sf i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

575 
and sg: "\<forall>i. simple_bochner_integrable M (sg i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

576 
then have [measurable]: "\<And>i. sf i \<in> borel_measurable M" "\<And>i. sg i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

577 
by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

578 
assume [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

579 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

580 
show "\<And>i. simple_bochner_integrable M (\<lambda>x. sf i x + sg i x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

581 
using sf sg by (simp add: simple_bochner_integrable_compose2) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

582 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

583 
show "(\<lambda>i. \<integral>\<^sup>+ x. (norm (f x + g x  (sf i x + sg i x))) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

584 
(is "?f > 0") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

585 
proof (rule tendsto_sandwich) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

586 
show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) > 0" 
56996  587 
by (auto simp: nn_integral_nonneg) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

588 
show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x  sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x  sg i x)) \<partial>M) sequentially" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

589 
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

590 
proof (intro always_eventually allI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

591 
fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x  sf i x)) + ereal (norm (g x  sg i x)) \<partial>M)" 
56996  592 
by (auto intro!: nn_integral_mono norm_diff_triangle_ineq) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

593 
also have "\<dots> = ?g i" 
56996  594 
by (intro nn_integral_add) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

595 
finally show "?f i \<le> ?g i" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

596 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

597 
show "?g > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

598 
using tendsto_add_ereal[OF _ _ f_sf g_sg] by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

599 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

600 
qed (auto simp: simple_bochner_integral_add tendsto_add) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

601 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

602 
lemma has_bochner_integral_bounded_linear: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

603 
assumes "bounded_linear T" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

604 
shows "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M (\<lambda>x. T (f x)) (T x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

605 
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

606 
interpret T: bounded_linear T by fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

607 
have [measurable]: "T \<in> borel_measurable borel" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

608 
by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

609 
assume [measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

610 
then show "(\<lambda>x. T (f x)) \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

611 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

612 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

613 
fix s assume f_s: "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x  s i x) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

614 
assume s: "\<forall>i. simple_bochner_integrable M (s i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

615 
then show "\<And>i. simple_bochner_integrable M (\<lambda>x. T (s i x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

616 
by (auto intro: simple_bochner_integrable_compose2 T.zero) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

617 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

618 
have [measurable]: "\<And>i. s i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

619 
using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

620 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

621 
obtain K where K: "K > 0" "\<And>x i. norm (T (f x)  T (s i x)) \<le> norm (f x  s i x) * K" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

622 
using T.pos_bounded by (auto simp: T.diff[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

623 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

624 
show "(\<lambda>i. \<integral>\<^sup>+ x. norm (T (f x)  T (s i x)) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

625 
(is "?f > 0") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

626 
proof (rule tendsto_sandwich) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

627 
show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) > 0" 
56996  628 
by (auto simp: nn_integral_nonneg) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

629 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

630 
show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x  s i x) \<partial>M)) sequentially" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

631 
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

632 
proof (intro always_eventually allI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

633 
fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x  s i x) \<partial>M)" 
56996  634 
using K by (intro nn_integral_mono) (auto simp: mult_ac) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

635 
also have "\<dots> = ?g i" 
56996  636 
using K by (intro nn_integral_cmult) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

637 
finally show "?f i \<le> ?g i" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

638 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

639 
show "?g > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

640 
using ereal_lim_mult[OF f_s, of "ereal K"] by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

641 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

642 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

643 
assume "(\<lambda>i. simple_bochner_integral M (s i)) > x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

644 
with s show "(\<lambda>i. simple_bochner_integral M (\<lambda>x. T (s i x))) > T x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

645 
by (auto intro!: T.tendsto simp: T.simple_bochner_integral_linear) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

646 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

647 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

648 
lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

649 
by (auto intro!: has_bochner_integral.intros[where s="\<lambda>_ _. 0"] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

650 
simp: zero_ereal_def[symmetric] simple_bochner_integrable.simps 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

651 
simple_bochner_integral_def image_constant_conv) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

652 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

653 
lemma has_bochner_integral_scaleR_left[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

654 
"(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x *\<^sub>R c) (x *\<^sub>R c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

655 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

656 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

657 
lemma has_bochner_integral_scaleR_right[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

658 
"(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c *\<^sub>R f x) (c *\<^sub>R x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

659 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

660 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

661 
lemma has_bochner_integral_mult_left[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

662 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

663 
shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x * c) (x * c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

664 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

665 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

666 
lemma has_bochner_integral_mult_right[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

667 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

668 
shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c * f x) (c * x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

669 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

670 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

671 
lemmas has_bochner_integral_divide = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

672 
has_bochner_integral_bounded_linear[OF bounded_linear_divide] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

673 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

674 
lemma has_bochner_integral_divide_zero[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

675 
fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

676 
shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

677 
using has_bochner_integral_divide by (cases "c = 0") auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

678 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

679 
lemma has_bochner_integral_inner_left[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

680 
"(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

681 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

682 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

683 
lemma has_bochner_integral_inner_right[intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

684 
"(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c \<bullet> f x) (c \<bullet> x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

685 
by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

686 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

687 
lemmas has_bochner_integral_minus = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

688 
has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

689 
lemmas has_bochner_integral_Re = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

690 
has_bochner_integral_bounded_linear[OF bounded_linear_Re] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

691 
lemmas has_bochner_integral_Im = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

692 
has_bochner_integral_bounded_linear[OF bounded_linear_Im] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

693 
lemmas has_bochner_integral_cnj = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

694 
has_bochner_integral_bounded_linear[OF bounded_linear_cnj] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

695 
lemmas has_bochner_integral_of_real = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

696 
has_bochner_integral_bounded_linear[OF bounded_linear_of_real] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

697 
lemmas has_bochner_integral_fst = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

698 
has_bochner_integral_bounded_linear[OF bounded_linear_fst] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

699 
lemmas has_bochner_integral_snd = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

700 
has_bochner_integral_bounded_linear[OF bounded_linear_snd] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

701 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

702 
lemma has_bochner_integral_indicator: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

703 
"A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

704 
has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

705 
by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

706 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

707 
lemma has_bochner_integral_diff: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

708 
"has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

709 
has_bochner_integral M (\<lambda>x. f x  g x) (x  y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

710 
unfolding diff_conv_add_uminus 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

711 
by (intro has_bochner_integral_add has_bochner_integral_minus) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

712 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

713 
lemma has_bochner_integral_setsum: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

714 
"(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

715 
has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

716 
by (induct I rule: infinite_finite_induct) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

717 
(auto intro: has_bochner_integral_zero has_bochner_integral_add) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

718 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

719 
lemma has_bochner_integral_implies_finite_norm: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

720 
"has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

721 
proof (elim has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

722 
fix s v 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

723 
assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

724 
lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

725 
from order_tendstoD[OF lim_0, of "\<infinity>"] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

726 
obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

727 
by (metis (mono_tags, lifting) eventually_False_sequentially eventually_elim1 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

728 
less_ereal.simps(4) zero_ereal_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

729 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

730 
have [measurable]: "\<And>i. s i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

731 
using s by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

732 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

733 
def m \<equiv> "if space M = {} then 0 else Max ((\<lambda>x. norm (s i x))`space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

734 
have "finite (s i ` space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

735 
using s by (auto simp: simple_function_def simple_bochner_integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

736 
then have "finite (norm ` s i ` space M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

737 
by (rule finite_imageI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

738 
then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

739 
by (auto simp: m_def image_comp comp_def Max_ge_iff) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

740 
then have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ereal m * indicator {x\<in>space M. s i x \<noteq> 0} x \<partial>M)" 
56996  741 
by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

742 
also have "\<dots> < \<infinity>" 
56996  743 
using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

744 
finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

745 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

746 
have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x  s i x)) + ereal (norm (s i x)) \<partial>M)" 
56996  747 
by (auto intro!: nn_integral_mono) (metis add_commute norm_triangle_sub) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

748 
also have "\<dots> = (\<integral>\<^sup>+x. norm (f x  s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)" 
56996  749 
by (rule nn_integral_add) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

750 
also have "\<dots> < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

751 
using s_fin f_s_fin by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

752 
finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

753 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

754 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

755 
lemma has_bochner_integral_norm_bound: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

756 
assumes i: "has_bochner_integral M f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

757 
shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

758 
using assms proof 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

759 
fix s assume 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

760 
x: "(\<lambda>i. simple_bochner_integral M (s i)) > x" (is "?s > x") and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

761 
s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

762 
lim: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) > 0" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

763 
f[measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

764 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

765 
have [measurable]: "\<And>i. s i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

766 
using s by (auto simp: simple_bochner_integrable.simps intro: borel_measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

767 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

768 
show "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

769 
proof (rule LIMSEQ_le) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

770 
show "(\<lambda>i. ereal (norm (?s i))) > norm x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

771 
using x by (intro tendsto_intros lim_ereal[THEN iffD2]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

772 
show "\<exists>N. \<forall>n\<ge>N. norm (?s n) \<le> (\<integral>\<^sup>+x. norm (f x  s n x) \<partial>M) + (\<integral>\<^sup>+x. norm (f x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

773 
(is "\<exists>N. \<forall>n\<ge>N. _ \<le> ?t n") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

774 
proof (intro exI allI impI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

775 
fix n 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

776 
have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

777 
by (auto intro!: simple_bochner_integral_norm_bound) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

778 
also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)" 
56996  779 
by (intro simple_bochner_integral_eq_nn_integral) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

780 
(auto intro: s simple_bochner_integrable_compose2) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

781 
also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x  s n x)) + norm (f x) \<partial>M)" 
56996  782 
by (auto intro!: nn_integral_mono) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

783 
(metis add_commute norm_minus_commute norm_triangle_sub) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

784 
also have "\<dots> = ?t n" 
56996  785 
by (rule nn_integral_add) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

786 
finally show "norm (?s n) \<le> ?t n" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

787 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

788 
have "?t > 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

789 
using has_bochner_integral_implies_finite_norm[OF i] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

790 
by (intro tendsto_add_ereal tendsto_const lim) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

791 
then show "?t > \<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

792 
by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

793 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

794 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

795 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

796 
lemma has_bochner_integral_eq: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

797 
"has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M f y \<Longrightarrow> x = y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

798 
proof (elim has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

799 
assume f[measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

800 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

801 
fix s t 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

802 
assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x  s i x) \<partial>M) > 0" (is "?S > 0") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

803 
assume "(\<lambda>i. \<integral>\<^sup>+ x. norm (f x  t i x) \<partial>M) > 0" (is "?T > 0") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

804 
assume s: "\<And>i. simple_bochner_integrable M (s i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

805 
assume t: "\<And>i. simple_bochner_integrable M (t i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

806 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

807 
have [measurable]: "\<And>i. s i \<in> borel_measurable M" "\<And>i. t i \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

808 
using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

809 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

810 
let ?s = "\<lambda>i. simple_bochner_integral M (s i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

811 
let ?t = "\<lambda>i. simple_bochner_integral M (t i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

812 
assume "?s > x" "?t > y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

813 
then have "(\<lambda>i. norm (?s i  ?t i)) > norm (x  y)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

814 
by (intro tendsto_intros) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

815 
moreover 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

816 
have "(\<lambda>i. ereal (norm (?s i  ?t i))) > ereal 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

817 
proof (rule tendsto_sandwich) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

818 
show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i  ?t i))) sequentially" "(\<lambda>_. 0) > ereal 0" 
56996  819 
by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric]) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

820 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

821 
show "eventually (\<lambda>i. norm (?s i  ?t i) \<le> ?S i + ?T i) sequentially" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

822 
by (intro always_eventually allI simple_bochner_integral_bounded s t f) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

823 
show "(\<lambda>i. ?S i + ?T i) > ereal 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

824 
using tendsto_add_ereal[OF _ _ `?S > 0` `?T > 0`] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

825 
by (simp add: zero_ereal_def[symmetric]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

826 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

827 
then have "(\<lambda>i. norm (?s i  ?t i)) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

828 
by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

829 
ultimately have "norm (x  y) = 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

830 
by (rule LIMSEQ_unique) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

831 
then show "x = y" by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

832 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

833 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

834 
lemma has_bochner_integralI_AE: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

835 
assumes f: "has_bochner_integral M f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

836 
and g: "g \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

837 
and ae: "AE x in M. f x = g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

838 
shows "has_bochner_integral M g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

839 
using f 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

840 
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

841 
fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

842 
also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x  s i x)) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

843 
using ae 
56996  844 
by (intro ext nn_integral_cong_AE, eventually_elim) simp 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

845 
finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x  s i x)) \<partial>M) > 0" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

846 
qed (auto intro: g) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

847 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

848 
lemma has_bochner_integral_eq_AE: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

849 
assumes f: "has_bochner_integral M f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

850 
and g: "has_bochner_integral M g y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

851 
and ae: "AE x in M. f x = g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

852 
shows "x = y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

853 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

854 
from assms have "has_bochner_integral M g x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

855 
by (auto intro: has_bochner_integralI_AE) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

856 
from this g show "x = y" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

857 
by (rule has_bochner_integral_eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

858 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

859 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

860 
inductive integrable for M f where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

861 
"has_bochner_integral M f x \<Longrightarrow> integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

862 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

863 
definition lebesgue_integral ("integral\<^sup>L") where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

864 
"integral\<^sup>L M f = (THE x. has_bochner_integral M f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

865 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

866 
syntax 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

867 
"_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

868 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

869 
translations 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

870 
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

871 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

872 
lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

873 
by (metis the_equality has_bochner_integral_eq lebesgue_integral_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

874 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

875 
lemma has_bochner_integral_integrable: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

876 
"integrable M f \<Longrightarrow> has_bochner_integral M f (integral\<^sup>L M f)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

877 
by (auto simp: has_bochner_integral_integral_eq integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

878 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

879 
lemma has_bochner_integral_iff: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

880 
"has_bochner_integral M f x \<longleftrightarrow> integrable M f \<and> integral\<^sup>L M f = x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

881 
by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

882 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

883 
lemma simple_bochner_integrable_eq_integral: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

884 
"simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integral M f = integral\<^sup>L M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

885 
using has_bochner_integral_simple_bochner_integrable[of M f] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

886 
by (simp add: has_bochner_integral_integral_eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

887 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

888 
lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = (THE x. False)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

889 
unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The]) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

890 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

891 
lemma integral_eq_cases: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

892 
"integrable M f \<longleftrightarrow> integrable N g \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

893 
(integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

894 
integral\<^sup>L M f = integral\<^sup>L N g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

895 
by (metis not_integrable_integral_eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

896 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

897 
lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

898 
by (auto elim: integrable.cases has_bochner_integral.cases) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

899 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

900 
lemma integrable_cong: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

901 
"M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

902 
using assms by (simp cong: has_bochner_integral_cong add: integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

903 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

904 
lemma integrable_cong_AE: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

905 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

906 
integrable M f \<longleftrightarrow> integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

907 
unfolding integrable.simps 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

908 
by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

909 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

910 
lemma integral_cong: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

911 
"M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

912 
using assms by (simp cong: has_bochner_integral_cong add: lebesgue_integral_def) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

913 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

914 
lemma integral_cong_AE: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

915 
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

916 
integral\<^sup>L M f = integral\<^sup>L M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

917 
unfolding lebesgue_integral_def 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

918 
by (intro has_bochner_integral_cong_AE arg_cong[where f=The] ext) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

919 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

920 
lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

921 
by (auto simp: integrable.simps intro: has_bochner_integral_add) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

922 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

923 
lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

924 
by (metis has_bochner_integral_zero integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

925 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

926 
lemma integrable_setsum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

927 
by (metis has_bochner_integral_setsum integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

928 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

929 
lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

930 
integrable M (\<lambda>x. indicator A x *\<^sub>R c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

931 
by (metis has_bochner_integral_indicator integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

932 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

933 
lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

934 
integrable M (indicator A :: 'a \<Rightarrow> real)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

935 
by (metis has_bochner_integral_real_indicator integrable.simps) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

936 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

937 
lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x  g x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

938 
by (auto simp: integrable.simps intro: has_bochner_integral_diff) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

939 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

940 
lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

941 
by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

942 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

943 
lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

944 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

945 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

946 
lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

947 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

948 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

949 
lemma integrable_mult_left[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

950 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

951 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

952 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

953 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

954 
lemma integrable_mult_right[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

955 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

956 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

957 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

958 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

959 
lemma integrable_divide_zero[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

960 
fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

961 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

962 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

963 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

964 
lemma integrable_inner_left[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

965 
"(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

966 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

967 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

968 
lemma integrable_inner_right[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

969 
"(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

970 
unfolding integrable.simps by fastforce 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

971 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

972 
lemmas integrable_minus[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

973 
integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

974 
lemmas integrable_divide[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

975 
integrable_bounded_linear[OF bounded_linear_divide] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

976 
lemmas integrable_Re[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

977 
integrable_bounded_linear[OF bounded_linear_Re] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

978 
lemmas integrable_Im[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

979 
integrable_bounded_linear[OF bounded_linear_Im] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

980 
lemmas integrable_cnj[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

981 
integrable_bounded_linear[OF bounded_linear_cnj] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

982 
lemmas integrable_of_real[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

983 
integrable_bounded_linear[OF bounded_linear_of_real] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

984 
lemmas integrable_fst[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

985 
integrable_bounded_linear[OF bounded_linear_fst] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

986 
lemmas integrable_snd[simp, intro] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

987 
integrable_bounded_linear[OF bounded_linear_snd] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

988 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

989 
lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

990 
by (intro has_bochner_integral_integral_eq has_bochner_integral_zero) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

991 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

992 
lemma integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

993 
integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

994 
by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

995 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

996 
lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

997 
integral\<^sup>L M (\<lambda>x. f x  g x) = integral\<^sup>L M f  integral\<^sup>L M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

998 
by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

999 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1000 
lemma integral_setsum[simp]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1001 
integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1002 
by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1003 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1004 
lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1005 
integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1006 
by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1007 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1008 
lemma integral_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1009 
integral\<^sup>L M (\<lambda>x. indicator A x *\<^sub>R c) = measure M A *\<^sub>R c" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1010 
by (intro has_bochner_integral_integral_eq has_bochner_integral_indicator has_bochner_integral_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1011 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1012 
lemma integral_real_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1013 
integral\<^sup>L M (indicator A :: 'a \<Rightarrow> real) = measure M A" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1014 
by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator has_bochner_integral_integrable) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1015 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1016 
lemma integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1017 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1018 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1019 
lemma integral_scaleR_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1020 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_right) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1021 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1022 
lemma integral_mult_left[simp]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1023 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1024 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1025 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1026 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1027 
lemma integral_mult_right[simp]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1028 
fixes c :: "_::{real_normed_algebra,second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1029 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1030 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1031 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1032 
lemma integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1033 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1034 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1035 
lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1036 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1037 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1038 
lemma integral_divide_zero[simp]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1039 
fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1040 
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1041 
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_divide_zero) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1042 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1043 
lemmas integral_minus[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1044 
integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1045 
lemmas integral_divide[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1046 
integral_bounded_linear[OF bounded_linear_divide] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1047 
lemmas integral_Re[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1048 
integral_bounded_linear[OF bounded_linear_Re] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1049 
lemmas integral_Im[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1050 
integral_bounded_linear[OF bounded_linear_Im] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1051 
lemmas integral_cnj[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1052 
integral_bounded_linear[OF bounded_linear_cnj] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1053 
lemmas integral_of_real[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1054 
integral_bounded_linear[OF bounded_linear_of_real] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1055 
lemmas integral_fst[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1056 
integral_bounded_linear[OF bounded_linear_fst] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1057 
lemmas integral_snd[simp] = 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1058 
integral_bounded_linear[OF bounded_linear_snd] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1059 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1060 
lemma integral_norm_bound_ereal: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1061 
"integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1062 
by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1063 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1064 
lemma integrableI_sequence: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1065 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1066 
assumes f[measurable]: "f \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1067 
assumes s: "\<And>i. simple_bochner_integrable M (s i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1068 
assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x  s i x) \<partial>M) > 0" (is "?S > 0") 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1069 
shows "integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1070 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1071 
let ?s = "\<lambda>n. simple_bochner_integral M (s n)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1072 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1073 
have "\<exists>x. ?s > x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1074 
unfolding convergent_eq_cauchy 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1075 
proof (rule metric_CauchyI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1076 
fix e :: real assume "0 < e" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1077 
then have "0 < ereal (e / 2)" by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1078 
from order_tendstoD(2)[OF lim this] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1079 
obtain M where M: "\<And>n. M \<le> n \<Longrightarrow> ?S n < e / 2" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1080 
by (auto simp: eventually_sequentially) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1081 
show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (?s m) (?s n) < e" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1082 
proof (intro exI allI impI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1083 
fix m n assume m: "M \<le> m" and n: "M \<le> n" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1084 
have "?S n \<noteq> \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1085 
using M[OF n] by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1086 
have "norm (?s n  ?s m) \<le> ?S n + ?S m" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1087 
by (intro simple_bochner_integral_bounded s f) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1088 
also have "\<dots> < ereal (e / 2) + e / 2" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1089 
using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]] 
56996  1090 
by (auto simp: nn_integral_nonneg) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1091 
also have "\<dots> = e" by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1092 
finally show "dist (?s n) (?s m) < e" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1093 
by (simp add: dist_norm) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1094 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1095 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1096 
then obtain x where "?s > x" .. 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1097 
show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1098 
by (rule, rule) fact+ 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1099 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1100 

56996  1101 
lemma nn_integral_dominated_convergence_norm: 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1102 
fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1103 
assumes [measurable]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1104 
"\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1105 
and bound: "\<And>j. AE x in M. norm (u j x) \<le> w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1106 
and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1107 
and u': "AE x in M. (\<lambda>i. u i x) > u' x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1108 
shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x  u i x) \<partial>M)) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1109 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1110 
have "AE x in M. \<forall>j. norm (u j x) \<le> w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1111 
unfolding AE_all_countable by rule fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1112 
with u' have bnd: "AE x in M. \<forall>j. norm (u' x  u j x) \<le> 2 * w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1113 
proof (eventually_elim, intro allI) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1114 
fix i x assume "(\<lambda>i. u i x) > u' x" "\<forall>j. norm (u j x) \<le> w x" "\<forall>j. norm (u j x) \<le> w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1115 
then have "norm (u' x) \<le> w x" "norm (u i x) \<le> w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1116 
by (auto intro: LIMSEQ_le_const2 tendsto_norm) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1117 
then have "norm (u' x) + norm (u i x) \<le> 2 * w x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1118 
by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1119 
also have "norm (u' x  u i x) \<le> norm (u' x) + norm (u i x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1120 
by (rule norm_triangle_ineq4) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1121 
finally (xtrans) show "norm (u' x  u i x) \<le> 2 * w x" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1122 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1123 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1124 
have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x  u i x) \<partial>M)) > (\<integral>\<^sup>+x. 0 \<partial>M)" 
56996  1125 
proof (rule nn_integral_dominated_convergence) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1126 
show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>" 
56996  1127 
by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1128 
show "AE x in M. (\<lambda>i. ereal (norm (u' x  u i x))) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1129 
using u' 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1130 
proof eventually_elim 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1131 
fix x assume "(\<lambda>i. u i x) > u' x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1132 
from tendsto_diff[OF tendsto_const[of "u' x"] this] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1133 
show "(\<lambda>i. ereal (norm (u' x  u i x))) > 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1134 
by (simp add: zero_ereal_def tendsto_norm_zero_iff) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1135 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1136 
qed (insert bnd, auto) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1137 
then show ?thesis by simp 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1138 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1139 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1140 
lemma integrableI_bounded: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1141 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1142 
assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1143 
shows "integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1144 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1145 
from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1146 
s: "\<And>i. simple_function M (s i)" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1147 
pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) > f x" and 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1148 
bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1149 
by (simp add: norm_conv_dist) metis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1150 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1151 
show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1152 
proof (rule integrableI_sequence) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1153 
{ fix i 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1154 
have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)" 
56996  1155 
by (intro nn_integral_mono) (simp add: bound) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1156 
also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)" 
56996  1157 
by (rule nn_integral_cmult) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1158 
finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1159 
using fin by auto } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1160 
note fin_s = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1161 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1162 
show "\<And>i. simple_bochner_integrable M (s i)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1163 
by (rule simple_bochner_integrableI_bounded) fact+ 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1164 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1165 
show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x  s i x)) \<partial>M) > 0" 
56996  1166 
proof (rule nn_integral_dominated_convergence_norm) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1167 
show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1168 
using bound by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1169 
show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1170 
using s by (auto intro: borel_measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1171 
show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>" 
56996  1172 
using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1173 
show "AE x in M. (\<lambda>i. s i x) > f x" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1174 
using pointwise by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1175 
qed fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1176 
qed fact 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1177 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1178 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1179 
lemma integrableI_nonneg: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1180 
fixes f :: "'a \<Rightarrow> real" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1181 
assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1182 
shows "integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1183 
proof  
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1184 
have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)" 
56996  1185 
using assms by (intro nn_integral_cong_AE) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1186 
then show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1187 
using assms by (intro integrableI_bounded) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1188 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1189 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1190 
lemma integrable_iff_bounded: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1191 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1192 
shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1193 
using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1194 
unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1195 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1196 
lemma integrable_bound: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1197 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1198 
and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1199 
shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1200 
integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1201 
unfolding integrable_iff_bounded 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1202 
proof safe 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1203 
assume "f \<in> borel_measurable M" "g \<in> borel_measurable M" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1204 
assume "AE x in M. norm (g x) \<le> norm (f x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1205 
then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)" 
56996  1206 
by (intro nn_integral_mono_AE) auto 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1207 
also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1208 
finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" . 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1209 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1210 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1211 
lemma integrable_abs[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1212 
fixes f :: "'a \<Rightarrow> real" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1213 
assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1214 
using assms by (rule integrable_bound) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1215 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1216 
lemma integrable_norm[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1217 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1218 
assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1219 
using assms by (rule integrable_bound) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1220 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1221 
lemma integrable_norm_cancel: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1222 
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1223 
assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1224 
using assms by (rule integrable_bound) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1225 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1226 
lemma integrable_abs_cancel: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1227 
fixes f :: "'a \<Rightarrow> real" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1228 
assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1229 
using assms by (rule integrable_bound) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1230 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1231 
lemma integrable_max[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1232 
fixes f :: "'a \<Rightarrow> real" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1233 
assumes fg[measurable]: "integrable M f" "integrable M g" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1234 
shows "integrable M (\<lambda>x. max (f x) (g x))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1235 
using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1236 
by (rule integrable_bound) auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1237 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1238 
lemma integrable_min[simp, intro]: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
diff
changeset

1239 
fixes f :: "'a \<Rightarrow> real" 