[STATEMENT]
lemma variance_divide:
  fixes f :: "'a \<Rightarrow> real"
  assumes "integrable M f"
  shows "variance (\<lambda>\<omega>. f \<omega> / r) = variance f / r^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. (f x / r - expectation (\<lambda>\<omega>. f \<omega> / r))\<^sup>2) = expectation (\<lambda>x. (f x - expectation f)\<^sup>2) / r\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
integrable M f

goal (1 subgoal):
 1. expectation (\<lambda>x. (f x / r - expectation (\<lambda>\<omega>. f \<omega> / r))\<^sup>2) = expectation (\<lambda>x. (f x - expectation f)\<^sup>2) / r\<^sup>2
[PROOF STEP]
by (subst Bochner_Integration.integral_divide[OF assms(1)])
    (simp add:diff_divide_distrib[symmetric] power2_eq_square algebra_simps)