equal
deleted
inserted
replaced
44 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
44 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
45 then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" |
45 then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" |
46 by (auto intro!: setsum_mono3 simp: pos) } |
46 by (auto intro!: setsum_mono3 simp: pos) } |
47 ultimately |
47 ultimately |
48 show ?thesis unfolding g_def using pos |
48 show ?thesis unfolding g_def using pos |
49 by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex le_SUPI2 |
49 by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex SUP_upper2 |
50 setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair |
50 setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair |
51 SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
51 SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
52 qed |
52 qed |
53 |
53 |
54 subsection {* Measure Spaces *} |
54 subsection {* Measure Spaces *} |