# Theory Projective_Limit

theory Projective_Limit
imports Fin_Map Infinite_Product_Measure Diagonal_Subsequence

section

theory Projective_Limit
imports
Fin_Map
Infinite_Product_Measure

begin

subsection

locale finmap_seqs_into_compact =
fixes K:: and f:: and M
assumes compact:
assumes f_in_K:
assumes domain_K:
assumes proj_in_K:

begin

lemma proj_in_K':
using proj_in_K f_in_K
proof cases
obtain k where  using f_in_K by auto
assume
thus ?thesis
by (auto intro!: exI[where x=1] image_eqI[OF _ ]
simp: domain_K[OF ])
qed blast

lemma proj_in_KE:
obtains n where
using proj_in_K' by blast

lemma compact_projset:
shows
using continuous_proj compact by (rule compact_continuous_image)

end

lemma compactE':
fixes S ::
assumes
obtains l r where
proof atomize_elim
have  by (simp add: strict_mono_def)
have  using assms by auto
from seq_compactE[OF [unfolded compact_eq_seq_compact_metric] this] guess l r .
hence
using strict_mono_o[OF  ] by (auto simp: o_def)
thus  by blast
qed

sublocale finmap_seqs_into_compact  subseqs
proof
fix n and s ::
assume
from proj_in_KE[of n] guess n0 . note n0 = this
have
proof safe
fix i assume
also have  by (rule seq_suble) fact
finally have  .
with n0 show
by auto
qed
from compactE'[OF compact_projset this] guess ls rs .
thus  by (auto simp: o_def)
qed

lemma (in finmap_seqs_into_compact) diagonal_tendsto:
proof -
obtain l where
proof (atomize_elim, rule diagseq_holds)
fix r s n
assume
assume
then obtain l where
by (auto simp: o_def)
hence  using
by (rule LIMSEQ_subseq_LIMSEQ)
thus  by (auto simp add: o_def)
qed
hence  by (simp add: ac_simps)
hence  by (rule LIMSEQ_offset)
thus ?thesis ..
qed

subsection

text

locale polish_projective = projective_family I P
for I:: and P
begin

lemma emeasure_lim_emb:
assumes X:
shows
proof (rule emeasure_lim)
write mu_G ()
interpret generator: algebra  generator
by (rule algebra_generator)

fix J and B ::
assume J:
and B:
and  (is )
moreover have
using J by (auto intro!: INF_lower2[of 0] prob_space_P[THEN prob_space.measure_le_1])
ultimately obtain r where r:
by (cases ) (auto simp: top_unique)
define Z where  for n
have Z_mono:  for n m
unfolding Z_def using B[THEN antimonoD, of n m] .
have J_mono:
using  by (force simp: incseq_def)
note [simp] =
interpret prob_space  for i using J prob_space_P by simp

have P_eq[simp]:
for i
using J by (auto simp: sets_P space_P)

have  for i
unfolding Z_def by (auto intro!: generator.intros J)

have countable_UN_J:  by (simp add: countable_finite)
define Utn where
interpret function_to_finmap  Utn  for n
by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
have inj_on_Utn:
unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
hence inj_on_Utn_J:  by (rule subset_inj_on) auto
define P' where  for n
interpret P': prob_space  for n
unfolding P'_def mapmeasure_def using J
by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P])

let ?SUP =
{ fix n
have
using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P)
also
have
proof (rule inner_regular)
show  by (simp add: borel_eq_PiF_borel P'_def)
next
show
unfolding borel_eq_PiF_borel by (auto simp: P'_def fm_image_measurable_finite sets_P J(3))
qed simp
finally have *:  .
have
unfolding *[symmetric] by simp
note * this
} note R = this
have
proof
fix n show
unfolding R[of n]
proof (rule ccontr)
assume H:
have
using R[of n] unfolding ennreal_add_left_cancel_less ennreal_zero_less_mult_iff
by (auto intro: )
also have
by (rule ennreal_SUP_add_left[symmetric]) auto
also have
proof (intro SUP_least)
fix K assume
with H have
by auto
then show
by (subst (asm) less_diff_eq_ennreal) (auto simp: less_top[symmetric] R(1)[symmetric] ac_simps)
qed
finally show False by simp
qed
qed
then obtain K' where K':

unfolding choice_iff by blast
define K where  for n
have K_sets:
unfolding K_def
using compact_imp_closed[OF ]
by (intro measurable_sets[OF fm_measurable, of _ ])
(auto simp: borel_eq_PiF_borel[symmetric])
have K_B:
proof
fix x n assume
then have fm_in:
using K' by (force simp: K_def)
show
using  K_sets sets.sets_into_space J(1,2,3)[of n] inj_on_image_mem_iff[OF inj_on_fm]
by (metis (no_types) Int_iff K_def fm_in space_borel)
qed
define Z' where  for n
have Z':
unfolding Z'_def Z_def
proof (rule prod_emb_mono, safe)
fix n x assume
hence
by (simp_all add: K_def space_P)
note this(1)
also have  by (simp add: K')
finally have  .
thus
proof safe
fix y assume y:
hence  using J sets.sets_into_space[of  ]
by (auto simp add: space_P sets_P)
assume
note inj_onD[OF inj_on_fm[OF space_borel],
OF   ]
with y show  by simp
qed
qed
have  using J K'(2) unfolding Z'_def
by (auto intro!: generator.intros measurable_sets[OF fm_measurable[of _ ]]
simp: K_def borel_eq_PiF_borel[symmetric] compact_imp_closed)
define Y where  for n
hence  by (induct_tac k) (auto simp: Y_def)
hence Y_mono:  by (auto simp: le_iff_add)
have Y_Z':  by (auto simp: Y_def)
hence Y_Z:  using Z' by auto

have Y_notempty:
proof -
fix n::nat assume  hence  by fact
have  using J J_mono
by (auto simp: Y_def Z'_def)
also have
using
by (subst prod_emb_INT) auto
finally
have Y_emb:
.
hence  using J J_mono K_sets
by (auto simp del: prod_emb_INT intro!: generator.intros)
have *:
unfolding Z_def using J by (intro mu_G_spec) auto
then have  by auto
note *
moreover have *:
unfolding Y_emb using J J_mono K_sets  by (subst mu_G_spec) auto
then have  by auto
note *
moreover have
unfolding Z_def Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets
by (subst mu_G_spec) (auto intro!: sets.Diff)
ultimately
have
using J J_mono K_sets
by (simp only: emeasure_eq_measure Z_def)
(auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B]
intro!: arg_cong[where f=ennreal]
simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P
ennreal_minus measure_nonneg)
also have subs:
using  unfolding Y_def UN_extend_simps(7) by (intro UN_mono Diff_mono Z_mono order_refl) auto
have
using    by auto
hence
unfolding increasing_def by auto
also have  using
also have
proof (rule sum_mono)
fix i assume  hence  by simp
have
unfolding Z'_def Z_def by simp
also have
using J K_sets by (subst mu_G_spec) auto
also have
using K_sets J  by (simp add: emeasure_Diff)
also have
unfolding K_def P'_def
by (auto simp: mapmeasure_PiF borel_eq_PiF_borel[symmetric]
compact_imp_closed[OF ] space_PiM PiE_def)
also have  using K'(1)[of i] .
finally show  .
qed
also have
using r by (simp add: sum_distrib_right ennreal_mult[symmetric])
also have
proof (intro ennreal_lessI mult_strict_right_mono)
have
by (rule sum.cong) (auto simp: powr_realpow powr_divide power_divide powr_minus_divide)
also have  by auto
also have  by (auto simp: sum_diff1)
also have  by (subst geometric_sum) auto
finally show  by simp
qed (auto simp: r enn2real_positive_iff)
also have  by (auto simp: r)
also have
using J by (auto intro: INF_lower simp: Z_def mu_G_spec)
finally have  .
hence R:
using  by (auto simp: zero_less_iff_neq_zero)
then have
by simp
thus  using positive_mu_G by (auto simp add: positive_def)
qed
hence  by auto
then obtain y where y:  unfolding bchoice_iff by force
{
fix t and n m::nat
assume   hence  by simp
from Y_mono[OF ] y[OF ] have  by auto
also have  using Y_Z'[OF ] .
finally
have
unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
moreover have
using J by (simp add: fm_def)
ultimately have  by simp
} note fm_in_K' = this
interpret finmap_seqs_into_compact   borel
proof
fix n show  by fact
next
fix n
from Y_mono[of n ] y[of ] have  by auto
also have  using Y_Z' by auto
finally
have
unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
thus  by auto
fix k
assume
with K'[of ] sets.sets_into_space have  by auto
then obtain b where  by auto
thus
by (simp_all add: fm_def)
next
fix t and n m::nat
assume  hence  by simp
assume
then obtain j where j:   by auto
hence  using J_mono[OF ] by auto
have img:  using
by (intro fm_in_K') simp_all
show
apply (rule image_eqI[OF _ img])
using
unfolding j by (subst proj_fm, auto)+
qed
have
using diagonal_tendsto ..
then obtain z where z:

unfolding choice_iff by blast
{
fix n :: nat assume
have
by simp
moreover
{
fix t
assume t:
hence  by simp
then obtain j where j:   by auto
have
apply (subst (2) tendsto_iff, subst eventually_sequentially)
proof safe
fix e :: real assume
{ fix i and x ::  assume i:
assume
hence  using J_mono[OF ] by auto
with i have
using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
} note index_shift = this
have I:
apply (rule le_SucI)
apply (rule order_trans) apply simp
apply (rule seq_suble[OF subseq_diagseq])
done
from z
have
unfolding tendsto_iff eventually_sequentially using  by auto
then obtain N where N:  by auto
show
proof (rule exI[where x=], safe)
fix na assume
hence   using t
by (subst index_shift[OF I]) auto
also have  using  by (intro N) simp
finally show  .
qed
qed
hence
by (simp add: tendsto_intros)
} ultimately
have
by (rule tendsto_finmap)
hence
by (rule LIMSEQ_subseq_LIMSEQ) (simp add: strict_mono_def)
moreover
have
apply (auto simp add: o_def intro!: fm_in_K'  le_SucI)
apply (rule le_trans)
using seq_suble[OF subseq_diagseq]
apply auto
done
moreover
from  have  by (rule compact_imp_closed)
ultimately
have
unfolding closed_sequential_limits by blast
also have
unfolding finmap_eq_iff
proof clarsimp
fix i assume i:
hence
unfolding Utn_def
by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
with i show
by (simp add: finmap_eq_iff fm_def compose_def)
qed
finally have  .
moreover
let ?J =
have  by auto
ultimately have
unfolding K_def by (auto simp: space_P space_PiM)
hence  unfolding Z'_def
using J by (auto simp: prod_emb_def PiE_def extensional_def)
also have  using Z' by simp
finally have  .
} note in_Z = this
hence  by auto
thus
using INT_decseq_offset[OF antimonoI[OF Z_mono]] by simp
qed fact+

lemma measure_lim_emb:

unfolding measure_def by (subst emeasure_lim_emb) auto

end

hide_const (open) PiF
hide_const (open) PiF
hide_const (open) Pi'
hide_const (open) finmap_of
hide_const (open) proj
hide_const (open) domain
hide_const (open) basis_finmap

sublocale polish_projective  P: prob_space lim
proof
have *:
by (auto simp: prod_emb_def space_PiM)
interpret prob_space
using prob_space_P by simp
show
using emeasure_lim_emb[of  ] emeasure_space_1
by (simp add: * PiM_empty space_P)
qed

locale polish_product_prob_space =
product_prob_space  I for I::

sublocale polish_product_prob_space  P: polish_projective I
..

lemma (in polish_product_prob_space) limP_eq_PiM:
by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb)

end