equal
deleted
inserted
replaced
38 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
38 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
39 then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" |
39 then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" |
40 by (auto intro!: setsum_mono3 simp: pos) } |
40 by (auto intro!: setsum_mono3 simp: pos) } |
41 ultimately |
41 ultimately |
42 show ?thesis unfolding g_def using pos |
42 show ?thesis unfolding g_def using pos |
43 by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex SUP_upper2 |
43 by (auto intro!: SUP_eq simp: setsum_cartesian_product reindex SUP_upper2 |
44 setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair |
44 setsum_nonneg suminf_ereal_eq_SUP SUP_pair |
45 SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
45 SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
46 qed |
46 qed |
47 |
47 |
48 subsection {* Measure Spaces *} |
48 subsection {* Measure Spaces *} |
49 |
49 |
50 definition subadditive where "subadditive M f \<longleftrightarrow> |
50 definition subadditive where "subadditive M f \<longleftrightarrow> |