imports Probability_Misc Linorder_Relations

(* File: Random_List.thy Authors: Manuel Eberl Some facts about randomly permuted lists and how to obtain them by drawing i.i.d. priorities for every element. *) section ‹Randomly-permuted lists› theory Random_List_Permutation imports Probability_Misc Comparison_Sort_Lower_Bound.Linorder_Relations begin subsection ‹General facts about linear orderings› text ‹ We define the set of all linear orderings on a given set and show some properties about it. › definition linorders_on :: "'a set ⇒ ('a × 'a) set set" where "linorders_on A = {R. linorder_on A R}" lemma linorders_on_empty [simp]: "linorders_on {} = {{}}" by (auto simp: linorders_on_def linorder_on_def refl_on_def) lemma linorders_finite_nonempty: assumes "finite A" shows "linorders_on A ≠ {}" proof - from finite_distinct_list[OF assms] obtain xs where "set xs = A" "distinct xs" by blast hence "linorder_on A (linorder_of_list xs)" by auto thus ?thesis by (auto simp: linorders_on_def) qed text ‹ There is an obvious bijection between permutations of a set (i.\,e.\ lists with all elements from that set without repetition) and linear orderings on it. › lemma bij_betw_linorders_on: assumes "finite A" shows "bij_betw linorder_of_list (permutations_of_set A) (linorders_on A)" using bij_betw_linorder_of_list[of A] assms unfolding linorders_on_def by simp lemma sorted_wrt_list_of_set_linorder_of_list [simp]: assumes "distinct xs" shows "sorted_wrt_list_of_set (linorder_of_list xs) (set xs) = xs" by (rule sorted_wrt_list_of_set_eqI[of "set xs"]) (insert assms, auto) lemma linorder_of_list_sorted_wrt_list_of_set [simp]: assumes "linorder_on A R" "finite A" shows "linorder_of_list (sorted_wrt_list_of_set R A) = R" proof - from assms(1) have subset: "R ⊆ A × A" by (auto simp: linorder_on_def refl_on_def) from assms and subset show ?thesis by (auto simp: linorder_of_list_def linorder_sorted_wrt_list_of_set sorted_wrt_linorder_index_le_iff) qed lemma bij_betw_linorders_on': assumes "finite A" shows "bij_betw (λR. sorted_wrt_list_of_set R A) (linorders_on A) (permutations_of_set A)" by (rule bij_betw_byWitness[where f' = linorder_of_list]) (insert assms, auto simp: linorders_on_def permutations_of_set_def linorder_sorted_wrt_list_of_set) lemma finite_linorders_on [intro]: assumes "finite A" shows "finite (linorders_on A)" proof - have "finite (permutations_of_set A)" by simp also have "?this ⟷ finite (linorders_on A)" using assms by (rule bij_betw_finite [OF bij_betw_linorders_on]) finally show ?thesis . qed text ‹ Next, we look at the ordering defined by a list that is permuted with some permutation function. For this, we first define the composition of a relation with a function. › definition map_relation :: "'a set ⇒ ('a ⇒ 'b) ⇒ ('b × 'b) set ⇒ ('a × 'a) set" where "map_relation A f R = {(x,y)∈A×A. (f x, f y) ∈ R}" lemma index_distinct_eqI: assumes "distinct xs" "i < length xs" "xs ! i = x" shows "index xs x = i" using assms by (induction xs arbitrary: i) (auto simp: nth_Cons split: nat.splits) lemma index_permute_list: assumes "π permutes {..<length xs}" "distinct xs" "x ∈ set xs" shows "index (permute_list π xs) x = inv π (index xs x)" proof - have *: "inv π permutes {..<length xs}" by (rule permutes_inv) fact from assms show ?thesis using assms permutes_in_image[OF *] by (intro index_distinct_eqI) (simp_all add: permute_list_nth permutes_inverses) qed lemma linorder_of_list_permute: assumes "π permutes {..<length xs}" "distinct xs" shows "linorder_of_list (permute_list π xs) = map_relation (set xs) ((!) xs ∘ inv π ∘ index xs) (linorder_of_list xs)" proof - note * = permutes_inv[OF assms(1)] have less: "inv π i < length xs" if "i < length xs" for i using permutes_in_image[OF *] and that by simp from assms and * show ?thesis by (auto simp: linorder_of_list_def map_relation_def index_nth_id index_permute_list less) qed lemma inj_on_conv_Ex1: "inj_on f A ⟷ (∀y∈f`A. ∃!x∈A. y = f x)" by (auto simp: inj_on_def) lemma bij_betw_conv_Ex1: "bij_betw f A B ⟷ (∀y∈B. ∃!x∈A. f x = y) ∧ B = f ` A" unfolding bij_betw_def inj_on_conv_Ex1 by (auto simp: eq_commute) lemma permutesI: assumes "bij_betw f A A" "∀x. x ∉ A ⟶ f x = x" shows "f permutes A" unfolding permutes_def proof (intro conjI allI impI) fix y from assms have [simp]: "f x ∈ A ⟷ x ∈ A" for x by (auto simp: bij_betw_def) show "∃!x. f x = y" proof (cases "y ∈ A") case True also from assms have "A = f ` A" by (auto simp: bij_betw_def) finally obtain x where "x ∈ A" "y = f x" by auto with assms and ‹y ∈ A› show ?thesis by (intro ex1I[of _ x]) (auto simp: bij_betw_def dest: inj_onD) qed (insert assms, auto) qed (insert assms, auto) text ‹ We now show the important lemma that any two linear orderings on a finite set can be mapped onto each other by a permutation. › lemma linorder_permutation_exists: assumes "finite A" "linorder_on A R" "linorder_on A R'" obtains π where "π permutes A" "R' = map_relation A π R" proof - define xs where "xs = sorted_wrt_list_of_set R A" define ys where "ys = sorted_wrt_list_of_set R' A" have xs_ys: "distinct xs" "distinct ys" "set xs = A" "set ys = A" using assms by (simp_all add: linorder_sorted_wrt_list_of_set xs_def ys_def) from xs_ys have "mset ys = mset xs" by (simp add: set_eq_iff_mset_eq_distinct [symmetric]) from mset_eq_permutation[OF this] guess π . note π = this define π' where "π' = (λx. if x ∉ A then x else xs ! inv π (index xs x))" have π': "π' permutes A" proof (rule permutesI) have "bij_betw ((!) xs ∘ inv π) {..<length xs} A" by (rule bij_betw_trans permutes_imp_bij permutes_inv π bij_betw_nth)+ (simp_all add: xs_ys) hence "bij_betw ((!) xs ∘ inv π ∘ index xs) A A" by (rule bij_betw_trans [rotated] bij_betw_index)+ (insert bij_betw_index[of xs A "length xs"], simp_all add: xs_ys atLeast0LessThan) also have "bij_betw ((!) xs ∘ inv π ∘ index xs) A A ⟷ bij_betw π' A A" by (rule bij_betw_cong) (auto simp: π'_def) finally show … . qed (simp_all add: π'_def) from assms have "R' = linorder_of_list ys" by (simp add: ys_def) also from π have "ys = permute_list π xs" by simp also have "linorder_of_list (permute_list π xs) = map_relation A ((!) xs ∘ inv π ∘ index xs) (linorder_of_list xs)" using π by (subst linorder_of_list_permute) (simp_all add: xs_ys) also from assms have "linorder_of_list xs = R" by (simp add: xs_def) finally have "R' = map_relation A ((!) xs ∘ inv π ∘ index xs) R" . also have "… = map_relation A π' R" by (auto simp: map_relation_def π'_def) finally show ?thesis using π' and that[of π'] by simp qed text ‹ We now define the linear ordering defined by some priority function, i.\,e.\ a function that injectively associates priorities to every element such that elements with lower priority are smaller in the resulting ordering. › definition linorder_from_keys :: "'a set ⇒ ('a ⇒ 'b :: linorder) ⇒ ('a × 'a) set" where "linorder_from_keys A f = {(x,y)∈A×A. f x ≤ f y}" lemma linorder_from_keys_permute: assumes "g permutes A" shows "linorder_from_keys A (f ∘ g) = map_relation A g (linorder_from_keys A f)" using permutes_in_image[OF assms] by (auto simp: map_relation_def linorder_from_keys_def) lemma linorder_on_linorder_from_keys [intro]: assumes "inj_on f A" shows "linorder_on A (linorder_from_keys A f)" using assms by (auto simp: linorder_on_def refl_on_def antisym_def linorder_from_keys_def trans_def total_on_def dest: inj_onD) lemma linorder_from_keys_empty [simp]: "linorder_from_keys {} = (λ_. {})" by (simp add: linorder_from_keys_def fun_eq_iff) text ‹ We now show another important fact, namely that when we draw $n$ values i.\,i.\,d.\ uniformly from a non-trivial real interval, we almost surely get distinct values. › lemma emeasure_PiM_diagonal: fixes a b :: real assumes "x ∈ A" "y ∈ A" "x ≠ y" assumes "a < b" "finite A" defines "M ≡ uniform_measure lborel {a..b}" shows "emeasure (PiM A (λ_. M)) {h∈A →⇩_{E}UNIV. h x = h y} = 0" proof - from assms have M: "prob_space M" unfolding M_def by (intro prob_space_uniform_measure) auto then interpret product_prob_space "λ_. M" A unfolding product_prob_space_def product_prob_space_axioms_def product_sigma_finite_def by (auto simp: prob_space_imp_sigma_finite) from M interpret pair_sigma_finite M M by unfold_locales have [measurable]: "{h∈extensional {x, y}. h x = h y} ∈ sets (Pi⇩_{M}{x, y} (λi. lborel))" proof - have "{h∈extensional {x,y}. h x = h y} = {h ∈ space (Pi⇩_{M}{x, y} (λi. lborel)). h x = h y}" by (auto simp: extensional_def space_PiM) also have "... ∈ sets (Pi⇩_{M}{x, y} (λi. lborel))" by measurable finally show ?thesis . qed have [simp]: "sets (PiM A (λ_. M)) = sets (PiM A (λ_. lborel))" for A :: "'a set" by (intro sets_PiM_cong refl) (simp_all add: M_def) have sets_M_M: "sets (M ⨂⇩_{M}M) = sets (borel ⨂⇩_{M}borel)" by (intro sets_pair_measure_cong) (auto simp: M_def) have [measurable]: "(λ(b, a). if b = a then 1 else 0) ∈ borel_measurable (M ⨂⇩_{M}M)" unfolding measurable_split_conv by (subst measurable_cong_sets[OF sets_M_M refl]) (auto intro!: measurable_If measurable_const measurable_equality_set) have "{h∈A →⇩_{E}UNIV. h x = h y} = (λh. restrict h {x, y}) -` {h∈extensional {x, y}. h x = h y} ∩ space (PiM A (λ_. M :: real measure))" by (auto simp: space_PiM PiE_def extensional_def M_def) also have "emeasure (PiM A (λ_. M)) … = emeasure (distr (PiM A (λ_. M)) (PiM {x,y} (λ_. lborel :: real measure)) (λh. restrict h {x,y})) {h∈extensional {x, y}. h x = h y}" proof (rule emeasure_distr [symmetric]) have "(λh. restrict h {x, y}) ∈ Pi⇩_{M}A (λ_. lborel) →⇩_{M}Pi⇩_{M}{x, y} (λ_. lborel)" using assms by (intro measurable_restrict_subset) auto also have "… = Pi⇩_{M}A (λ_. M) →⇩_{M}Pi⇩_{M}{x, y} (λ_. lborel)" by (intro sets_PiM_cong measurable_cong_sets refl) (simp_all add: M_def) finally show "(λh. restrict h {x, y}) ∈ …" . next show "{h∈extensional {x, y}. h x = h y} ∈ sets (Pi⇩_{M}{x, y} (λ_. lborel))" by simp qed also have "distr (PiM A (λ_. M)) (PiM {x,y} (λ_. lborel :: real measure)) (λh. restrict h {x,y}) = distr (PiM A (λ_. M)) (PiM {x,y} (λ_. M)) (λh. restrict h {x,y})" by (intro distr_cong refl sets_PiM_cong) (simp_all add: M_def) also from assms have "… = Pi⇩_{M}{x, y} (λi. M)" by (intro distr_restrict [symmetric]) auto also have "emeasure … {h∈extensional {x, y}. h x = h y} = nn_integral … (λh. indicator {h∈extensional {x, y}. h x = h y} h)" by (intro nn_integral_indicator [symmetric]) simp_all also have "… = nn_integral (Pi⇩_{M}{x, y} (λi. M)) (λh. if h x = h y then 1 else 0)" by (intro nn_integral_cong) (auto simp add: indicator_def space_PiM PiE_def) also from ‹x ≠ y› have "… = (∫⇧^{+}z. (if fst z = snd z then 1 else 0) ∂(M ⨂⇩_{M}M))" by (intro product_nn_integral_pair) auto also have "… = (∫⇧^{+}x. (∫⇧^{+}y. (if x = y then 1 else 0) ∂M) ∂M)" by (subst M.nn_integral_fst [symmetric]) simp_all also have "… = (∫⇧^{+}x. (∫⇧^{+}y. indicator {x} y ∂M) ∂M)" by (simp add: indicator_def eq_commute) also have "… = (∫⇧^{+}x. emeasure M {x} ∂M)" by (subst nn_integral_indicator) (simp_all add: M_def) also have "… = (∫⇧^{+}x. 0 ∂M)" unfolding M_def by (intro nn_integral_cong_AE refl AE_uniform_measureI) auto also have "… = 0" by simp finally show ?thesis . qed lemma measurable_linorder_from_keys_restrict: assumes fin: "finite A" shows "linorder_from_keys A ∈ Pi⇩_{M}A (λ_. borel :: real measure) →⇩_{M}count_space (Pow (A × A))" (is "_ : ?M →⇩_{M}_") apply (subst measurable_count_space_eq2) apply (auto simp add: fin linorder_from_keys_def) proof - note fin[simp] fix R assume "R ⊆ A × A" then have "linorder_from_keys A -` {R} ∩ space ?M = {f ∈ space ?M. ∀x∈A. ∀y∈A. (x, y) ∈ R ⟷ f x ≤ f y}" by (auto simp add: linorder_from_keys_def set_eq_iff) also have "… ∈ sets ?M" by measurable finally show "linorder_from_keys A -` {R} ∩ space ?M ∈ sets ?M" . qed lemma measurable_count_space_extend: assumes "f ∈ measurable M (count_space A)" "A ⊆ B" shows "f ∈ measurable M (count_space B)" proof - note assms(1) also have "count_space A = restrict_space (count_space B) A" using assms(2) by (subst restrict_count_space) (simp_all add: Int_absorb2) finally show ?thesis by (simp add: measurable_restrict_space2_iff) qed lemma measurable_linorder_from_keys_restrict': assumes fin: "finite A" "A ⊆ B" shows "linorder_from_keys A ∈ Pi⇩_{M}A (λ_. borel :: real measure) →⇩_{M}count_space (Pow (B × B))" apply (rule measurable_count_space_extend) apply (rule measurable_linorder_from_keys_restrict[OF assms(1)]) using assms by auto context fixes a b :: real and A :: "'a set" and M and B assumes fin: "finite A" and ab: "a < b" and B: "A ⊆ B" defines "M ≡ distr (PiM A (λ_. uniform_measure lborel {a..b})) (count_space (Pow (B × B))) (linorder_from_keys A)" begin lemma measurable_linorder_from_keys [measurable]: "linorder_from_keys A ∈ Pi⇩_{M}A (λ_. borel :: real measure) →⇩_{M}count_space (Pow (B × B))" by (rule measurable_linorder_from_keys_restrict') (auto simp: fin B) text ‹ The ordering defined by randomly-chosen priorities is almost surely linear: › theorem almost_everywhere_linorder: "AE R in M. linorder_on A R" proof - define N where "N = PiM A (λ_. uniform_measure lborel {a..b})" have [simp]: "sets (Pi⇩_{M}A (λ_. uniform_measure lborel {a..b})) = sets (PiM A (λ_. lborel))" by (intro sets_PiM_cong) simp_all let ?M_A = "(Pi⇩_{M}A (λ_. lborel :: real measure))" have meas: "{h ∈ A →⇩_{E}UNIV. h i = h j} ∈ sets ?M_A" if [simp]: "i ∈ A" "j ∈ A" for i j proof - have "{h ∈ A →⇩_{E}UNIV. h i = h j} = {h ∈ space ?M_A. h i = h j}" by (auto simp: space_PiM) also have "... ∈ sets ?M_A" by measurable finally show ?thesis . qed define X :: "('a ⇒ real) set" where "X = (⋃x∈A. ⋃y∈A-{x}. {h∈A →⇩_{E}UNIV. h x = h y})" have "AE f in N. inj_on f A" proof (rule AE_I) show "{f ∈ space N. ¬ inj_on f A} ⊆ X" by (auto simp: inj_on_def X_def space_PiM N_def) next show "X ∈ sets N" unfolding X_def N_def using meas by (auto intro!: countable_finite fin sets.countable_UN') next have "emeasure N X ≤ (∑i∈A. emeasure N (⋃y∈A - {i}. {h ∈ A →⇩_{E}UNIV. h i = h y}))" unfolding X_def N_def using fin meas by (intro emeasure_subadditive_finite) (auto simp: disjoint_family_on_def intro!: sets.countable_UN' countable_finite) also have "… ≤ (∑i∈A. ∑j∈A-{i}. emeasure N {h ∈ A →⇩_{E}UNIV. h i = h j})" unfolding N_def using fin meas by (intro emeasure_subadditive_finite sum_mono) (auto simp: disjoint_family_on_def intro!: sets.countable_UN' countable_finite) also have "… = (∑i∈A. ∑j∈A-{i}. 0)" unfolding N_def using fin ab by (intro sum.cong refl emeasure_PiM_diagonal) auto also have "… = 0" by simp finally show "emeasure N X = 0" by simp qed hence "AE f in N. linorder_on A (linorder_from_keys A f)" by eventually_elim auto thus ?thesis unfolding M_def N_def by (subst AE_distr_iff) auto qed text ‹ Furthermore, this is equivalent to choosing one of the $|A|!$ linear orderings uniformly at random. › theorem random_linorder_by_prios: "M = uniform_measure (count_space (Pow (B × B))) (linorders_on A)" proof - from linorders_finite_nonempty[OF fin] obtain R where R: "linorder_on A R" by (auto simp: linorders_on_def) have *: "emeasure M {R} ≤ emeasure M {R'}" if "linorder_on A R" "linorder_on A R'" for R R' proof - define N where "N = PiM A (λ_. uniform_measure lborel {a..b})" from linorder_permutation_exists[OF fin that] obtain π where π: "π permutes A" "R' = map_relation A π R" by blast have "(λf. f ∘ π) ∈ Pi⇩_{M}A (λ_. lborel :: real measure) →⇩_{M}Pi⇩_{M}A (λ_. lborel :: real measure)" by (auto intro!: measurable_PiM_single' measurable_PiM_component_rev simp: comp_def permutes_in_image[OF π(1)] space_PiM PiE_def extensional_def) also have "… = N →⇩_{M}Pi⇩_{M}A (λ_. lborel)" unfolding N_def by (intro measurable_cong_sets refl sets_PiM_cong) simp_all finally have [measurable]: "(λf. f ∘ π) ∈ …" . have [simp]: "measurable N X = measurable (PiM A (λ_. lborel)) X" for X :: "('a × 'a) set measure" unfolding N_def by (intro measurable_cong_sets refl sets_PiM_cong) simp_all have [simp]: "measurable M X = measurable (count_space (Pow (B × B))) X" for X :: "('a × 'a) set measure" unfolding M_def by simp have M_eq: "M = distr N (count_space (Pow (B × B))) (linorder_from_keys A)" by (simp only: M_def N_def) also have "N = distr N (PiM A (λ_. lborel)) (λf. f ∘ π)" unfolding N_def by (rule PiM_uniform_measure_permute [symmetric]) fact+ also have "distr … (count_space (Pow (B × B))) (linorder_from_keys A) = distr N (count_space (Pow (B × B))) (linorder_from_keys A ∘ (λf. f ∘ π)) " by (intro distr_distr) simp_all also have "… = distr N (count_space (Pow (B × B))) (map_relation A π ∘ linorder_from_keys A)" by (intro distr_cong refl) (auto simp: linorder_from_keys_permute[OF π(1)]) also have "… = distr M (count_space (Pow (B × B))) (map_relation A π)" unfolding M_eq using B by (intro distr_distr [symmetric]) (auto simp: map_relation_def) finally have M_eq': "distr M (count_space (Pow (B × B))) (map_relation A π) = M" .. from that have subset': "R ⊆ B × B" "R' ⊆ B × B" using B by (auto simp: linorder_on_def refl_on_def) hence "emeasure M {R} ≤ emeasure M (map_relation A π -` {R'} ∩ space M)" using subset' by (intro emeasure_mono) (auto simp: M_def π ) also have "… = emeasure (distr M (count_space (Pow (B × B))) (map_relation A π)) {R'} " by (rule emeasure_distr [symmetric]) (insert subset' B, auto simp: map_relation_def) also note M_eq' finally show ?thesis . qed have same_prob: "emeasure M {R'} = emeasure M {R}" if "linorder_on A R'" for R' using *[of R R'] and *[of R' R] and R and that by simp from ab have "prob_space M" unfolding M_def by (intro prob_space.prob_space_distr prob_space_PiM prob_space_uniform_measure) simp_all hence "1 = emeasure M (Pow (B × B))" using prob_space.emeasure_space_1[OF ‹prob_space M›] by (simp add: M_def) also have "(Pow (B × B)) = linorders_on A ∪ ((Pow (B × B))-linorders_on A)" using B by (auto simp: linorders_on_def linorder_on_def refl_on_def) also have "emeasure M … = emeasure M (linorders_on A) + emeasure M (Pow (B × B)-linorders_on A)" using B by (subst plus_emeasure) (auto simp: M_def linorders_on_def linorder_on_def refl_on_def) also have "emeasure M (Pow (B × B)-linorders_on A) = 0" using almost_everywhere_linorder by (subst (asm) AE_iff_measurable) (auto simp: linorders_on_def M_def) also from fin have "emeasure M (linorders_on A) = (∑R'∈linorders_on A. emeasure M {R'})" using B by (intro emeasure_eq_sum_singleton) (auto simp: M_def linorders_on_def linorder_on_def refl_on_def) also have "… = (∑R'∈linorders_on A. emeasure M {R})" by (rule sum.cong) (simp_all add: linorders_on_def same_prob) also from fin have "… = fact (card A) * emeasure M {R}" by (simp add: linorders_on_def card_finite_linorders) finally have [simp]: "emeasure M {R} = inverse (fact (card A))" by (simp add: inverse_ennreal_unique) show ?thesis proof (rule measure_eqI_countable_AE') show "sets M = Pow (Pow (B × B))" by (simp add: M_def) next from ‹finite A› show "countable (linorders_on A)" by (blast intro: countable_finite) next show "AE R in uniform_measure (count_space (Pow (B × B))) (linorders_on A). R ∈ linorders_on A" by (rule AE_uniform_measureI) (insert B, auto simp: linorders_on_def linorder_on_def refl_on_def) next fix R' assume R': "R' ∈ linorders_on A" have subset: "linorders_on A ⊆ Pow (B × B)" using B by (auto simp: linorders_on_def linorder_on_def refl_on_def) have "emeasure (uniform_measure (count_space (Pow (B × B))) (linorders_on A)) {R'} = emeasure (count_space (Pow (B × B))) (linorders_on A ∩ {R'}) / emeasure (count_space (Pow (B × B))) (linorders_on A)" using R' B by (subst emeasure_uniform_measure) (auto simp: linorders_on_def linorder_on_def refl_on_def) also have "… = 1 / emeasure (count_space (Pow (B × B))) (linorders_on A)" using R' B by (subst emeasure_count_space) (auto simp: linorders_on_def linorder_on_def refl_on_def) also have "… = 1 / fact (card A)" using fin finite_linorders_on[of A] by (subst emeasure_count_space [OF subset]) (auto simp: divide_ennreal [symmetric] linorders_on_def card_finite_linorders) also have "… = emeasure M {R}" by (simp add: field_simps divide_ennreal_def) also have "… = emeasure M {R'}" using R' by (intro same_prob [symmetric]) (auto simp: linorders_on_def) finally show "emeasure M {R'} = emeasure (uniform_measure (count_space (Pow (B × B))) (linorders_on A)) {R'}" .. next show "linorders_on A ⊆ Pow (B × B)" using B by (auto simp: linorders_on_def linorder_on_def refl_on_def) qed (auto simp: M_def linorders_on_def almost_everywhere_linorder) qed end end