Theory Random_List_Permutation
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])
then obtain π where π: "π permutes {..<length xs}" "permute_list π xs = ys"
by (rule mset_eq_permutation)
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 of_bool_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