equal
deleted
inserted
replaced
14 Notation |
14 Notation |
15 *) |
15 *) |
16 |
16 |
17 syntax |
17 syntax |
18 "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
18 "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
19 ("(3LINT _|_. _)" [0,110,60] 60) |
19 ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60) |
20 |
20 |
21 translations |
21 translations |
22 "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)" |
22 "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)" |
23 |
23 |
24 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M" |
24 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M" |
27 |
27 |
28 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)" |
28 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)" |
29 |
29 |
30 syntax |
30 syntax |
31 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
31 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
32 ("(4LINT _:_|_. _)" [0,60,110,61] 60) |
32 ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60) |
33 |
33 |
34 translations |
34 translations |
35 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)" |
35 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)" |
36 |
36 |
37 abbreviation |
37 abbreviation |
38 "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x" |
38 "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x" |
39 |
39 |
40 syntax |
40 syntax |
41 "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" |
41 "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" |
42 ("AE _\<in>_ in _. _" [0,0,0,10] 10) |
42 ("AE _\<in>_ in _./ _" [0,0,0,10] 10) |
43 |
43 |
44 translations |
44 translations |
45 "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)" |
45 "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)" |
46 |
46 |
47 (* |
47 (* |
53 TODO: keep all these? Need unicode. |
53 TODO: keep all these? Need unicode. |
54 *) |
54 *) |
55 |
55 |
56 syntax |
56 syntax |
57 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real" |
57 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real" |
58 ("(2LBINT _. _)" [0,60] 60) |
58 ("(2LBINT _./ _)" [0,60] 60) |
59 |
59 |
60 translations |
60 translations |
61 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)" |
61 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)" |
62 |
62 |
63 syntax |
63 syntax |
64 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real" |
64 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real" |
65 ("(3LBINT _:_. _)" [0,60,61] 60) |
65 ("(3LBINT _:_./ _)" [0,60,61] 60) |
66 |
66 |
67 translations |
67 translations |
68 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)" |
68 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)" |
69 |
69 |
70 (* |
70 (* |