equal
deleted
inserted
replaced
7 subsection \<open>Equiintegrability\<close> |
7 subsection \<open>Equiintegrability\<close> |
8 |
8 |
9 text\<open>The definition here only really makes sense for an elementary set. |
9 text\<open>The definition here only really makes sense for an elementary set. |
10 We just use compact intervals in applications below.\<close> |
10 We just use compact intervals in applications below.\<close> |
11 |
11 |
12 definition%important equiintegrable_on (infixr "equiintegrable'_on" 46) |
12 definition\<^marker>\<open>tag important\<close> equiintegrable_on (infixr "equiintegrable'_on" 46) |
13 where "F equiintegrable_on I \<equiv> |
13 where "F equiintegrable_on I \<equiv> |
14 (\<forall>f \<in> F. f integrable_on I) \<and> |
14 (\<forall>f \<in> F. f integrable_on I) \<and> |
15 (\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and> |
15 (\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and> |
16 (\<forall>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma> fine \<D> |
16 (\<forall>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma> fine \<D> |
17 \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < e))" |
17 \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < e))" |