[STATEMENT]
lemma (in filtrated_prob_space) AE_borel_eq:
fixes f::"'a\<Rightarrow>real"
assumes "f\<in> borel_measurable (F t)"
and "g\<in> borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "{w\<in> space M. f w \<noteq> g w} \<in> sets (F t) \<and> emeasure M {w\<in> space M. f w \<noteq> g w} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t) \<and> emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
 2. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
show "{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
define minus where "minus = (\<lambda>w. (f w) - (g w))"
[PROOF STATE]
proof (state)
this:
minus = (\<lambda>w. f w - g w)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "minus \<in> borel_measurable (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minus \<in> borel_measurable (F t)
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. f w - g w) \<in> borel_measurable (F t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (F t)
g \<in> borel_measurable (F t)
AE w in M. f w = g w

goal (1 subgoal):
 1. (\<lambda>w. f w - g w) \<in> borel_measurable (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
hence "{w\<in> space (F t). 0 < minus w} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
using this:
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<in> sets (F t)
[PROOF STEP]
using borel_measurable_iff_greater
[PROOF STATE]
proof (prove)
using this:
minus \<in> borel_measurable (F t)
(?f \<in> borel_measurable ?M) = (\<forall>a. {w \<in> space ?M. a < ?f w} \<in> sets ?M)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<in> sets (F t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). minus w < 0} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
using borel_measurable_iff_less
      \<open>minus \<in> borel_measurable (F t)\<close>
[PROOF STATE]
proof (prove)
using this:
(?f \<in> borel_measurable ?M) = (\<forall>a. {w \<in> space ?M. ?f w < a} \<in> sets ?M)
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)
{w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). 0 < minus w} \<union> {w\<in> space (F t). minus w < 0} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)
{w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). f w \<noteq> g w} = {w\<in> space (F t). 0 < minus w} \<union> {w\<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
 2. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
show "{w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
assume "w \<in> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (state)
this:
w \<in> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
hence "w\<in> space (F t)" and "f w \<noteq> g w"
[PROOF STATE]
proof (prove)
using this:
w \<in> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. w \<in> space (F t) &&& f w \<noteq> g w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
thus "w\<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
using this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. w \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
using this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. w \<in> {w \<in> space (F t). 0 < f w - g w} \<union> {w \<in> space (F t). f w - g w < 0}
[PROOF STEP]
by (cases "f w < g w") auto
[PROOF STATE]
proof (state)
this:
w \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
have "{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). 0 < f w - g w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
have "{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w - g w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
show "{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "space (F t) = space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
using filtration
[PROOF STATE]
proof (prove)
using this:
Filtration.filtration M F

goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
unfolding filtration_def subalgebra_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>t. space (F t) = space M \<and> sets (F t) \<subseteq> events) \<and> (\<forall>s t. s \<le> t \<longrightarrow> space (F s) = space (F t) \<and> sets (F s) \<subseteq> sets (F t))

goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
space (F t) = space M

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
space (F t) = space M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
space (F t) = space M

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)

goal (1 subgoal):
 1. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
show "emeasure M {w\<in> space M. f w \<noteq> g w} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
by (metis (no_types) AE_iff_measurable assms(3) emeasure_notin_sets)
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. f w \<noteq> g w} = 0

goal:
No subgoals!
[PROOF STEP]
qed