[STATEMENT]
lemma real_cond_exp_mult:
  assumes [measurable]:"f \<in> borel_measurable F" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f x * g x)"
  shows "AE x in M. real_cond_exp M F (\<lambda>x. f x * g x) x = f x * real_cond_exp M F g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M F (\<lambda>x. f x * g x) x = f x * real_cond_exp M F g x
[PROOF STEP]
proof (rule real_cond_exp_charact)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
assume "A \<in> sets F"
[PROOF STATE]
proof (state)
this:
A \<in> sets F

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> sets F
[PROOF STEP]
have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F"
[PROOF STATE]
proof (prove)
using this:
A \<in> sets F

goal (1 subgoal):
 1. (\<lambda>x. f x * indicat_real A x) \<in> borel_measurable F
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * indicat_real A x) \<in> borel_measurable F

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have [measurable]: "A \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> sets M
[PROOF STEP]
using subalg
[PROOF STATE]
proof (prove)
using this:
subalgebra M F

goal (1 subgoal):
 1. A \<in> sets M
[PROOF STEP]
by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
[PROOF STATE]
proof (state)
this:
A \<in> sets M

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x
[PROOF STEP]
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x
[PROOF STEP]
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * indicat_real A x * g x)
[PROOF STEP]
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)]
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. indicat_real A x *\<^sub>R (f x * g x))

goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * indicat_real A x * g x)
[PROOF STEP]
by (simp add: mult.commute mult.left_commute)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real A x * real_cond_exp M F g x = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * real_cond_exp M F g x = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
[PROOF STATE]
proof (prove)
using this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (1 subgoal):
 1. \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (3 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 3. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
qed (auto simp add: real_cond_exp_intg(1) assms)