theory Scratch
imports Probability
begin

lemma distr_bij_count_space:
  assumes f: "bij_betw f A B"
  shows "distr (count_space A) (count_space B) f = count_space B"
proof (rule measure_eqI)
  have f': "f \<in> measurable (count_space A) (count_space B)"
    using f unfolding Pi_def bij_betw_def by auto
  fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)"
  then have X: "X \<in> sets (count_space B)" by auto
  moreover then have "f -` X \<inter> A = the_inv_into A f ` X"
    using f by (auto simp: bij_betw_def subset_image_iff image_iff the_inv_into_f_f intro: the_inv_into_f_f[symmetric])
  moreover have "inj_on (the_inv_into A f) B"
    using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
  with X have "inj_on (the_inv_into A f) X"
    by (auto intro: subset_inj_on)
  ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X"
    using f unfolding emeasure_distr[OF f' X]
    by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD)
qed simp

lemma nn_integral_bij_count_space:
  assumes g: "bij_betw g A B"
  shows "(\<integral>\<^sup>+x. f (g x) \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
  using g[THEN bij_betw_imp_funcset]
  by (subst distr_bij_count_space[OF g, symmetric])
     (auto intro!: nn_integral_distr[symmetric])

lemma ereal_suminf_bij:
  fixes f :: "nat \<Rightarrow> ereal"
  assumes g: "bij g"
  shows "(\<And>n. 0 \<le> f n) \<Longrightarrow> (\<Sum>x. f (g x)) = (\<Sum>x. f x)"
  apply (subst (1 2) nn_integral_count_space_nat[symmetric])
  apply (auto simp: g nn_integral_bij_count_space)
  done

lemma summable_ereal_iff: "(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<longleftrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
  by (metis suminf_ereal_finite summable_ereal)

lemma summable_bij:
  fixes f :: "nat \<Rightarrow> real"
  assumes g: "bij g"
  shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> summable (\<lambda>x. f (g x)) \<longleftrightarrow> summable f"
  by (simp add: summable_ereal_iff ereal_suminf_bij[OF g, of f])

lemma sums_bij:
  fixes f :: "nat \<Rightarrow> real"
  shows "bij g \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>x. f (g x)) = suminf f"
  unfolding ereal.inject[symmetric]
  by (subst (1 2) suminf_ereal'[symmetric]) (auto simp: summable_bij intro!: ereal_suminf_bij)

end