Theory Measure_Convergence
section "Convergence in measure"
theory Measure_Convergence
imports "HOL-Probability.Probability"
begin
text ‹ We use measure rather than emeasure because ennreal is not a metric space, which we need to
reason about convergence. By intersecting with the set of finite measure A, we don't run into issues
where infinity is collapsed to 0.
For finite measures this definition is equal to the definition without set A -- see below. ›
definition tendsto_measure :: "'b measure ⇒ ('a ⇒ 'b ⇒ ('c :: {second_countable_topology,metric_space}))
⇒ ('b ⇒ 'c) ⇒ 'a filter ⇒ bool"
where "tendsto_measure M X l F ≡ (∀n. X n ∈ borel_measurable M) ∧ l ∈ borel_measurable M ∧
(∀ε > 0. ∀A ∈ fmeasurable M.
((λn. measure M ({ω ∈ space M. dist (X n ω) (l ω) > ε} ∩ A)) ⤏ 0) F)"
abbreviation (in prob_space) tendsto_prob (infixr "⤏⇩P" 55) where
"(f ⤏⇩P l) F ≡ tendsto_measure M f l F"
lemma tendsto_measure_measurable[measurable_dest]:
"tendsto_measure M X l F ⟹ X n ∈ borel_measurable M"
unfolding tendsto_measure_def by meson
lemma tendsto_measure_measurable_lim[measurable_dest]:
"tendsto_measure M X l F ⟹ l ∈ borel_measurable M"
unfolding tendsto_measure_def by meson
lemma tendsto_measure_mono: "F ≤ F' ⟹ tendsto_measure M f l F' ⟹ tendsto_measure M f l F"
unfolding tendsto_measure_def by (simp add: tendsto_mono)
lemma tendsto_measureI:
assumes [measurable]: "⋀n. X n ∈ borel_measurable M" "l ∈ borel_measurable M"
and "⋀ε A. ε > 0 ⟹ A ∈ fmeasurable M ⟹
((λn. measure M ({ω ∈ space M. dist (X n ω) (l ω) > ε} ∩ A)) ⤏ 0) F"
shows "tendsto_measure M X l F"
unfolding tendsto_measure_def using assms by fast
lemma (in finite_measure) finite_tendsto_measureI:
assumes [measurable]: "⋀n. f' n ∈ borel_measurable M" "f ∈ borel_measurable M"
and "⋀ε. ε > 0 ⟹ ((λn. measure M {ω ∈ space M. dist (f' n ω) (f ω) > ε}) ⤏ 0) F"
shows "tendsto_measure M f' f F"
proof (intro tendsto_measureI)
fix ε :: real assume "ε > 0"
then have prob_conv: "((λn. measure M {ω ∈ space M. ε < dist (f' n ω) (f ω)}) ⤏ 0) F"
using assms by simp
fix A assume "A ∈ fmeasurable M"
have "⋀n. measure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)}) ≥
measure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A)"
by (rule finite_measure_mono; measurable)
then show "((λn. measure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A)) ⤏ 0) F"
by (simp add: tendsto_0_le[OF prob_conv, where K=1])
qed measurable
lemma (in finite_measure) finite_tendsto_measureD:
assumes [measurable]: "tendsto_measure M f' f F"
shows "(∀ε > 0. ((λn. measure M {ω ∈ space M. dist (f' n ω) (f ω) > ε}) ⤏ 0) F)"
proof -
from assms have "((λn. measure M ({ω ∈ space M. dist (f' n ω) (f ω) > ε} ∩ space M)) ⤏ 0) F"
if "ε > 0" for ε
unfolding tendsto_measure_def using that fmeasurable_eq_sets by blast
then show ?thesis
by (simp add: sets.Int_space_eq2[symmetric, where M=M])
qed
lemma (in finite_measure) tendsto_measure_leq:
assumes [measurable]: "⋀n. f' n ∈ borel_measurable M" "f ∈ borel_measurable M"
shows "tendsto_measure M f' f F ⟷
(∀ε > 0. ((λn. measure M {ω ∈ space M. dist (f' n ω) (f ω) ≥ ε}) ⤏ 0) F)" (is "?L ⟷ ?R")
proof (rule iffI, goal_cases)
case 1
{
fix ε :: real assume "ε > 0"
then have "((λn. measure M {ω ∈ space M. dist (f' n ω) (f ω) > ε/2}) ⤏ 0) F"
using finite_tendsto_measureD[OF 1] half_gt_zero by blast
then have "((λn. measure M {ω ∈ space M. dist (f' n ω) (f ω) ≥ ε}) ⤏ 0) F"
apply (rule metric_tendsto_imp_tendsto)
using ‹ε > 0› by (auto intro!: eventuallyI finite_measure_mono)
}
then show ?case
by simp
next
case 2
{
fix ε :: real assume "ε > 0"
then have *: "((λn. 𝒫(ω in M. ε ≤ dist (f' n ω) (f ω))) ⤏ 0) F"
using 2 by blast
then have "((λn. 𝒫(ω in M. ε < dist (f' n ω) (f ω))) ⤏ 0) F"
apply (rule metric_tendsto_imp_tendsto)
using ‹ε > 0› by (auto intro!: eventuallyI finite_measure_mono)
}
then show ?case
by (simp add: finite_tendsto_measureI[OF assms])
qed
abbreviation "LIMSEQ_measure M f l ≡ tendsto_measure M f l sequentially"
lemma LIMSEQ_measure_def: "LIMSEQ_measure M f l ⟷
(∀n. f n ∈ borel_measurable M) ∧ (l ∈ borel_measurable M) ∧
(∀ε > 0. ∀A ∈ fmeasurable M.
(λn. measure M ({ω ∈ space M. dist (f n ω) (l ω) > ε} ∩ A)) ⇢ 0)"
unfolding tendsto_measure_def ..
lemma LIMSEQ_measureD:
assumes "LIMSEQ_measure M f l" "ε > 0" "A ∈ fmeasurable M"
shows "(λn. measure M ({ω ∈ space M. dist (f n ω) (l ω) > ε} ∩ A)) ⇢ 0"
using assms LIMSEQ_measure_def by blast
lemma fmeasurable_inter: "⟦A ∈ sets M; B ∈ fmeasurable M⟧ ⟹ A ∩ B ∈ fmeasurable M"
proof (intro fmeasurableI, goal_cases measurable finite)
case measurable
then show ?case by simp
next
case finite
then have "emeasure M (A ∩ B) ≤ emeasure M B"
by (simp add: emeasure_mono)
also have "emeasure M B < ∞"
using finite(2)[THEN fmeasurableD2] by (simp add: top.not_eq_extremum)
finally show ?case .
qed
lemma LIMSEQ_measure_emeasure:
assumes "LIMSEQ_measure M f l" "ε > 0" "A ∈ fmeasurable M"
and [measurable]: "⋀i. f i ∈ borel_measurable M" "l ∈ borel_measurable M"
shows "(λn. emeasure M ({ω ∈ space M. dist (f n ω) (l ω) > ε} ∩ A)) ⇢ 0"
proof -
have fmeasurable: "{ω ∈ space M. dist (f n ω) (l ω) > ε} ∩ A ∈ fmeasurable M" for n
by (rule fmeasurable_inter; simp add: assms(3))
then show ?thesis
apply (simp add: emeasure_eq_measure2 ennreal_tendsto_0_iff)
using LIMSEQ_measure_def assms by blast
qed
lemma measure_Lim_within_LIMSEQ:
fixes a :: "'a :: first_countable_topology"
assumes "⋀t. X t ∈ borel_measurable M" "L ∈ borel_measurable M"
assumes "⋀S. ⟦(∀n. S n ≠ a ∧ S n ∈ T); S ⇢ a⟧ ⟹ LIMSEQ_measure M (λn. X (S n)) L"
shows "tendsto_measure M X L (at a within T)"
apply (intro tendsto_measureI[OF assms(1,2)])
unfolding tendsto_measure_def[where l=L] tendsto_def apply safe
apply (rule sequentially_imp_eventually_within)
using assms unfolding LIMSEQ_measure_def tendsto_def by presburger
definition tendsto_AE :: "'b measure ⇒ ('a ⇒ 'b ⇒ 'c :: topological_space) ⇒ ('b ⇒ 'c) ⇒ 'a filter ⇒ bool" where
"tendsto_AE M f' l F ⟷ (AE ω in M. ((λn. f' n ω) ⤏ l ω) F)"
lemma LIMSEQ_ae_pointwise: "(⋀x. (λn. f n x) ⇢ l x) ⟹ tendsto_AE M f l sequentially"
unfolding tendsto_AE_def by simp
lemma tendsto_AE_within_LIMSEQ:
fixes a :: "'a :: first_countable_topology"
assumes "⋀S. ⟦(∀n. S n ≠ a ∧ S n ∈ T); S ⇢ a⟧ ⟹ tendsto_AE M (λn. X (S n)) L sequentially"
shows "tendsto_AE M X L (at a within T)"
oops
lemma LIMSEQ_dominated_convergence:
fixes X :: "nat ⇒ real"
assumes "X ⇢ L" "(⋀n. Y n ≤ X n)" "(⋀n. Y n ≥ L)"
shows "Y ⇢ L"
proof (rule metric_LIMSEQ_I)
have "X n ≥ L" for n
using assms(2,3)[of n] by linarith
fix r :: real assume "0 < r"
then obtain N where "∀n≥N. dist (X n) L < r"
using metric_LIMSEQ_D[OF assms(1) ‹0 < r›] by blast
then have N: "∀n≥N. X n - L < r"
using ‹⋀n. L ≤ X n› by (auto simp: dist_real_def)
have "∀n≥N. Y n - L < r"
proof clarify
fix n assume ‹n ≥ N›
then have "X n - L < r"
using N by blast
then show "Y n - L < r"
using assms(2)[of n] by auto
qed
then show "∃no. ∀n≥no. dist (Y n) L < r"
apply (intro exI[where x=N])
using assms(3) dist_real_def by auto
qed
text ‹ Klenke remark 6.4 ›
lemma measure_conv_imp_AE_sequentially:
assumes [measurable]: "⋀n. f' n ∈ borel_measurable M" "f ∈ borel_measurable M"
and "tendsto_AE M f' f sequentially"
shows "LIMSEQ_measure M f' f"
proof (unfold tendsto_measure_def, safe)
fix ε :: real assume "0 < ε"
fix A assume A[measurable]: "A ∈ fmeasurable M"
text ‹ From AE convergence we know there's a null set where f' doesn't converge ›
obtain N where N: "N ∈ null_sets M" "{ω ∈ space M. ¬ (λn. f' n ω) ⇢ f ω} ⊆ N"
using assms unfolding tendsto_AE_def by (simp add: eventually_ae_filter, blast)
then have measure_0: "measure M {ω ∈ space M. ¬ (λn. f' n ω) ⇢ f ω} = 0"
by (meson measure_eq_0_null_sets measure_notin_sets null_sets_subset)
text ‹ D is a sequence of sets that converges to N ›
define D where "D ≡ λn. {ω ∈ space M. ∃m ≥ n. dist (f' m ω) (f ω) > ε}"
have "⋀n. D n ∈ sets M"
unfolding D_def by measurable
then have [measurable]: "⋀n. D n ∩ A ∈ sets M"
by simp
have "(⋂n. D n) ∈ sets M"
unfolding D_def by measurable
then have measurable_D_A: "(⋂n. D n ∩ A) ∈ sets M"
by simp
have "(⋂n. D n) ⊆ {ω ∈ space M. ¬ (λn. (f' n ω)) ⇢ f ω}"
proof (intro subsetI)
fix x assume "x ∈ (⋂n. D n)"
then have "x ∈ space M" "⋀n. ∃m ≥ n. ε < dist (f' m x) (f x)"
unfolding D_def by simp_all
then have "¬ (λn. f' n x) ⇢ f x"
by (simp add: LIMSEQ_def) (meson ‹0 < ε› not_less_iff_gr_or_eq order_less_le)
then show "x ∈ {ω ∈ space M. ¬ (λn. f' n ω) ⇢ f ω}"
using ‹x ∈ space M› by blast
qed
then have "measure M (⋂n. D n) = 0"
by (metis (no_types, lifting) N ‹⋂ (range D) ∈ sets M› measure_eq_0_null_sets null_sets_subset subset_trans)
then have "measure M (⋂n. D n ∩ A) = 0"
proof -
have "emeasure M (⋂n. D n ∩ A) ≤ emeasure M (⋂n. D n)"
apply (rule emeasure_mono)
apply blast
unfolding D_def apply measurable
done
then show ?thesis
by (smt (verit, del_insts) N Sigma_Algebra.measure_def ‹measure M (⋂ (range D)) = 0›
‹⋂ (range D) ∈ sets M› ‹⋂ (range D) ⊆ {ω ∈ space M. ¬ (λn. f' n ω) ⇢ f ω}›
dual_order.trans enn2real_mono ennreal_zero_less_top measure_nonneg null_setsD1 null_sets_subset)
qed
moreover have "(λn. measure M (D n ∩ A)) ⇢ measure M (⋂n. D n ∩ A)"
apply (rule Lim_measure_decseq)
using A(1) ‹⋀n. D n ∈ sets M› apply blast
subgoal
apply (intro monotoneI)
apply clarsimp
apply (simp add: D_def)
by (meson order_trans)
apply (simp add: A ‹⋀n. D n ∈ sets M› fmeasurableD2 fmeasurable_inter)
done
ultimately have measure_D_0: "(λn. measure M (D n ∩ A)) ⇢ 0"
by presburger
have "⋀n. {ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A ⊆ (D n ∩ A)"
unfolding D_def by blast
then have "⋀n. emeasure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A) ≤ emeasure M (D n ∩ A)"
by (rule emeasure_mono) measurable
then have "⋀n. measure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A) ≤ measure M (D n ∩ A)"
unfolding measure_def apply (rule enn2real_mono)
by (meson A ‹⋀n. D n ∈ sets M› fmeasurableD2 fmeasurable_inter top.not_eq_extremum)
then show "(λn. measure M ({ω ∈ space M. ε < dist (f' n ω) (f ω)} ∩ A)) ⇢ 0"
by (simp add: LIMSEQ_dominated_convergence[OF measure_D_0])
qed simp_all
corollary LIMSEQ_measure_pointwise:
assumes "⋀x. (λn. f n x) ⇢ f' x" "⋀n. f n ∈ borel_measurable M" "f' ∈ borel_measurable M"
shows "LIMSEQ_measure M f f'"
by (simp add: LIMSEQ_ae_pointwise measure_conv_imp_AE_sequentially assms)
lemma Lim_measure_pointwise:
fixes a :: "'a :: first_countable_topology"
assumes "⋀x. ((λn. f n x) ⤏ f' x)(at a within T)" "⋀n. f n ∈ borel_measurable M" "f' ∈ borel_measurable M"
shows "tendsto_measure M f f' (at a within T)"
proof (intro measure_Lim_within_LIMSEQ)
fix S assume "∀n. S n ≠ a ∧ S n ∈ T" "S ⇢ a"
then have "(λn. f (S n) x) ⇢ f' x" for x
using assms(1) by (simp add: tendsto_at_iff_sequentially o_def)
then show "LIMSEQ_measure M (λn. f (S n)) f'"
by (simp add: LIMSEQ_measure_pointwise assms(2,3))
qed (simp_all add: assms)
corollary measure_conv_imp_AE_at_within:
fixes x :: "'a :: first_countable_topology"
assumes [measurable]: "⋀n. f' n ∈ borel_measurable M" "f ∈ borel_measurable M"
and "tendsto_AE M f' f (at x within S)"
shows "tendsto_measure M f' f (at x within S)"
proof (rule measure_Lim_within_LIMSEQ[OF assms(1,2)])
fix s assume *: "∀n. s n ≠ x ∧ s n ∈ S" "s ⇢ x"
have AE_seq: "AE ω in M. ∀X. (∀i. X i ∈ S - {x}) ⟶ X ⇢ x ⟶ ((λn. f' n ω) ∘ X) ⇢ f ω"
using assms(3) by (simp add: tendsto_AE_def tendsto_at_iff_sequentially)
then have "AE ω in M. (∀i. s i ∈ S - {x}) ⟶ s ⇢ x ⟶ ((λn. f' n ω) ∘ s) ⇢ f ω"
by force
then have "AE ω in M. ((λn. f' n ω) ∘ s) ⇢ f ω"
using * by force
then have "tendsto_AE M (λn. f' (s n)) f sequentially"
unfolding tendsto_AE_def comp_def by blast
then show "LIMSEQ_measure M (λn. f' (s n)) f"
by (rule measure_conv_imp_AE_sequentially[OF assms(1,2)])
qed
text ‹ Klenke remark 6.5 ›
lemma (in sigma_finite_measure) LIMSEQ_measure_unique_AE:
fixes f :: "nat ⇒ 'a ⇒ 'b :: {second_countable_topology,metric_space}"
assumes [measurable]: "⋀n. f n ∈ borel_measurable M" "l ∈ borel_measurable M" "l' ∈ borel_measurable M"
and "LIMSEQ_measure M f l" "LIMSEQ_measure M f l'"
shows "AE x in M. l x = l' x"
proof -
obtain A :: "nat ⇒ 'a set" where A: "⋀i. A i ∈ fmeasurable M" "(⋃i. A i) = space M"
by (metis fmeasurableI infinity_ennreal_def rangeI sigma_finite subset_eq top.not_eq_extremum)
have "⋀m ε. {x ∈ space M. dist (l x) (l' x) > ε} ∩ A m ∈ fmeasurable M"
by (intro fmeasurable_inter; simp add: A)
then have emeasure_leq: "emeasure M ({x ∈ space M. dist (l x) (l' x) > ε} ∩ A m) ≤
emeasure M ({x ∈ space M. dist (l x) (f n x) > ε/2} ∩ A m) +
emeasure M ({x ∈ space M. dist (f n x) (l' x) > ε/2} ∩ A m)" if "ε > 0" for n m ε
proof -
have [measurable]:
"{x ∈ space M. ε / 2 < dist (l x) (f n x)} ∩ A m ∈ sets M"
"{x ∈ space M. ε / 2 < dist (f n x) (l' x)} ∩ A m ∈ sets M"
using A by (measurable; auto)+
have "dist (l x) (l' x) ≤ dist (l x) (f n x) + dist (f n x) (l' x)" for x
by (simp add: dist_triangle)
then have "{x. dist (l x) (l' x) > ε} ⊆ {x. dist (l x) (f n x) > ε/2} ∪ {x. dist (f n x) (l' x) > ε/2}"
by (safe, smt (verit, best) field_sum_of_halves)
then have "{x ∈ space M. dist (l x) (l' x) > ε} ∩ A m ⊆
({x ∈ space M. dist (l x) (f n x) > ε/2} ∩ A m) ∪ ({x ∈ space M. dist (f n x) (l' x) > ε/2} ∩ A m)"
by blast
then have "emeasure M ({x ∈ space M. dist (l x) (l' x) > ε} ∩ A m) ≤
emeasure M ({x ∈ space M. dist (l x) (f n x) > ε/2} ∩ A m ∪ {x ∈ space M. dist (f n x) (l' x) > ε/2} ∩ A m)"
apply (rule emeasure_mono)
using A by measurable
also have "... ≤ emeasure M ({x ∈ space M. dist (l x) (f n x) > ε/2} ∩ A m) +
emeasure M ({x ∈ space M. dist (f n x) (l' x) > ε/2} ∩ A m)"
apply (rule emeasure_subadditive)
using A by measurable
finally show ?thesis .
qed
moreover have tendsto_zero: "(λn. emeasure M ({x ∈ space M. ε / 2 < dist (f n x) (l x)} ∩ A m)
+ emeasure M ({x ∈ space M. ε / 2 < dist (f n x) (l' x)} ∩ A m)) ⇢ 0"
if ‹ε > 0› for ε m
apply (rule tendsto_add_zero)
apply (rule LIMSEQ_measure_emeasure[OF assms(4)])
prefer 5 apply (rule LIMSEQ_measure_emeasure[OF assms(5)])
using that A apply simp_all
done
have dist_ε_emeasure: "emeasure M ({x ∈ space M. ε < dist (l x) (l' x)} ∩ A m) = 0"
if ‹ε > 0› for ε m
proof (rule ccontr)
assume "emeasure M ({x ∈ space M. ε < dist (l x) (l' x)} ∩ A m) ≠ 0"
then obtain e where e: "e > 0" "emeasure M ({x ∈ space M. ε < dist (l x) (l' x)} ∩ A m) ≥ e"
using not_gr_zero by blast
have "∃no. ∀n≥no. (emeasure M ({x ∈ space M. ε / 2 < dist (f n x) (l x)} ∩ A m)
+ emeasure M ({x ∈ space M. ε / 2 < dist (f n x) (l' x)} ∩ A m)) < e"
proof -
have measure_tendsto_0: "(λn. measure M ({x ∈ space M. ε / 2 < dist (f n x) (l x)} ∩ A m)
+ measure M ({x ∈ space M. ε / 2 < dist (f n x) (l' x)} ∩ A m)) ⇢ 0"
apply (rule tendsto_add_zero)
using A(1) LIMSEQ_measure_def assms(4,5) half_gt_zero that by blast+
have "enn2real e > 0"
by (metis (no_types, lifting) A(1) e(1) e(2) emeasure_neq_0_sets enn2real_eq_0_iff
enn2real_nonneg fmeasurableD2 fmeasurable_inter inf_right_idem linorder_not_less nless_le top.not_eq_extremum)
then obtain no where "∀n≥no. (measure M ({x ∈ space M. ε / 2 < dist (f n x) (l x)} ∩ A m)
+ measure M ({x ∈ space M. ε / 2 < dist (f n x) (l' x)} ∩ A m)) < enn2real e"
using LIMSEQ_D[OF measure_tendsto_0 ‹enn2real e > 0›] by (simp) blast
then show ?thesis
apply (safe intro!: exI[where x=no])
by (smt (verit, del_insts) A(1) Sigma_Algebra.measure_def add_eq_0_iff_both_eq_0
emeasure_eq_measure2 emeasure_neq_0_sets enn2real_mono enn2real_plus enn2real_top
ennreal_0 ennreal_zero_less_top fmeasurable_inter inf_sup_ord(2) le_iff_inf
linorder_not_less top.not_eq_extremum zero_less_measure_iff)
qed
then obtain N where N: "emeasure M ({x ∈ space M. ε / 2 < dist (f N x) (l x)} ∩ A m)
+ emeasure M ({x ∈ space M. ε / 2 < dist (f N x) (l' x)} ∩ A m) < e"
by auto
then have "emeasure M ({x ∈ space M. ε < dist (l x) (l' x)} ∩ A m) < e"
by (smt (verit, del_insts) emeasure_leq[OF that] Collect_cong dist_commute e(2) leD order_less_le_trans)
then show False
using e(2) by auto
qed
have "emeasure M ({x ∈ space M. 0 < dist (l x) (l' x)} ∩ A m) = 0" for m
proof -
have sets: "range (λn. {x ∈ space M. 1/2^n < dist (l x) (l' x)} ∩ A m) ⊆ sets M"
using A by force
have "(⋃n. {x ∈ space M. 1/2^n < dist (l x) (l' x)}) = {x ∈ space M. 0 < dist (l x) (l' x)}"
apply (intro subset_antisym subsetI)
apply force
apply simp
by (metis one_less_numeral_iff power_one_over reals_power_lt_ex semiring_norm(76) zero_less_dist_iff)
moreover have "emeasure M ({x ∈ space M. 1/2^n < dist (l x) (l' x)} ∩ A m) = 0" for n
using dist_ε_emeasure by simp
then have suminf_zero: "(∑n. emeasure M ({x ∈ space M. 1/2^n < dist (l x) (l' x)} ∩ A m)) = 0"
by auto
then have "emeasure M (⋃n. ({x ∈ space M. 1/2^n < dist (l x) (l' x)} ∩ A m)) ≤ 0"
apply (subst suminf_zero[symmetric])
apply (rule emeasure_subadditive_countably)
by (simp add: emeasure_subadditive_countably sets)
ultimately show ?thesis
by simp
qed
then have "(∑m. emeasure M ({x ∈ space M. 0 < dist (l x) (l' x)} ∩ A m)) = 0"
by simp
then have "emeasure M (⋃m. {x ∈ space M. 0 < dist (l x) (l' x)} ∩ A m) = 0"
proof -
let ?S = "λm. {x ∈ space M. 0 < dist (l x) (l' x)} ∩ A m"
have "emeasure M (⋃m. ?S m) ≤ (∑m. emeasure M (?S m))"
apply (rule emeasure_subadditive_countably)
using ‹⋀m ε. {x ∈ space M. ε < dist (l x) (l' x)} ∩ A m ∈ fmeasurable M› by blast
then show ?thesis
using ‹(∑m. emeasure M (?S m)) = 0› by force
qed
then have "emeasure M {x ∈ space M. 0 < dist (l x) (l' x)} = 0"
using A by simp
then show ?thesis
by (auto simp add: AE_iff_null)
qed
corollary (in sigma_finite_measure) LIMSEQ_ae_unique_AE:
fixes f :: "nat ⇒ 'a ⇒ 'b :: {second_countable_topology,metric_space}"
assumes "⋀n. f n ∈ borel_measurable M" "l ∈ borel_measurable M" "l' ∈ borel_measurable M"
and "tendsto_AE M f l sequentially" "tendsto_AE M f l' sequentially"
shows "AE x in M. l x = l' x"
proof -
have "LIMSEQ_measure M f l" "LIMSEQ_measure M f l'"
using assms measure_conv_imp_AE_sequentially by blast+
then show ?thesis
using assms(1-3) LIMSEQ_measure_unique_AE by blast
qed
lemma (in sigma_finite_measure) tendsto_measure_at_within_eq_AE:
fixes f :: "'b :: first_countable_topology ⇒ 'a ⇒ 'c :: {second_countable_topology,metric_space}"
assumes f_measurable: "⋀x. x ∈ S ⟹ f x ∈ borel_measurable M"
and l_measurable: "l ∈ borel_measurable M" "l' ∈ borel_measurable M"
and tendsto: "tendsto_measure M f l (at t within S)" "tendsto_measure M f l' (at t within S)"
and not_bot: "(at t within S) ≠ ⊥"
shows "AE x in M. l x = l' x"
proof -
from not_bot have "t islimpt S"
using trivial_limit_within by blast
then obtain s :: "nat ⇒ 'b" where s: "⋀i. s i ∈ S - {t}" "s ⇢ t"
using islimpt_sequential by meson
then have fs_measurable: "⋀n. f (s n) ∈ borel_measurable M"
using f_measurable by blast
have *: "LIMSEQ_measure M (λn. f (s n)) l"
if "l ∈ borel_measurable M" "tendsto_measure M f l (at t within S)" for l
proof (intro tendsto_measureI[OF fs_measurable that(1)], goal_cases)
case (1 ε A)
then have "((λn. measure M ({ω ∈ space M. ε < dist (f n ω) (l ω)} ∩ A)) ⤏ 0)(at t within S)"
using that(2) 1 tendsto_measure_def by blast
then show ?case
apply (rule filterlim_compose[where f=s])
by (smt (verit, del_insts) DiffD1 DiffD2 eventuallyI filterlim_at insertI1 s)
qed
show ?thesis
apply (rule LIMSEQ_measure_unique_AE[OF fs_measurable l_measurable])
using * tendsto l_measurable by simp_all
qed
end