Theory No_Free_Lunch_ML
section ‹No-Free-Lunch Theorem for ML›
theory No_Free_Lunch_ML
imports
"HOL-Probability.Probability"
begin
subsection ‹Preliminaries›
lemma sum_le_card_Max_of_nat:"finite A
⟹ sum f A ≤ (of_nat :: _ ⇒ _ ::{semiring_1,ordered_comm_monoid_add}) (card A) * Max (f ` A)"
using sum_bounded_above[of A f "Max (f ` A)"] by simp
lemma card_Min_le_sum_of_nat: "finite A
⟹ (of_nat :: _ ⇒ _ ::{semiring_1,ordered_comm_monoid_add}) (card A) * Min (f ` A) ≤ sum f A"
using sum_bounded_below[of A "Min (f ` A)" f] by simp
text ‹ The following lemma is used to show the last equation of the proof of the no-free-lunch theorem
in the book~\cite{shalev2014}.›
text ‹ Let $A$ be a finite set. If $A$ is divided into the pairs $(x_1,y_1),\dots,(x_n,y_n)$
such that $f(x_i) + f(y_i) = k$ for all $i = 1,\dots, n$.
Then, we have $\sum_{x\in A} f(x) = k * |A| / 2$.›
lemma sum_of_const_pairs:
fixes k :: "real"
assumes A:"finite A"
and "fst ` B ∪ snd ` B = A" "fst ` B ∩ snd ` B = {}"
and "inj_on fst B" "inj_on snd B"
and sum: "⋀x y. (x,y) ∈ B ⟹ f x + f y = k"
shows "(∑x∈A. f x) = k * real (card A) / 2"
using assms
proof(induction A arbitrary: B rule: finite_psubset_induct)
case ih:(psubset A)
show ?case
proof(cases "A ={}")
assume "A ≠ {}"
then obtain x where x:"x ∈ A"
by blast
then obtain y where xy:"(x,y) ∈ B ∨ (y,x) ∈ B"
using ih(3) by fastforce
then have xy':"x ≠ y"
by (metis emptyE fst_eqD ih(4) imageI mem_simps(4) snd_eqD)
have y:"y ∈ A"
using ih(3) xy by force
have *:"(∑a∈A - {x,y}. f a) = k * real (card (A - {x,y})) / 2"
proof -
consider "(x,y) ∈ B" | "(y,x) ∈ B"
using xy by blast
then show ?thesis
proof cases
assume xy:"(x,y) ∈ B"
show ?thesis
proof(intro ih(2))
have *:"fst ` (B - {(x, y)}) = fst ` B - {x}"
by(subst inj_on_image_set_diff[of fst B]) (use ih(5) xy in auto)
have **: "snd ` (B - {(x, y)}) = snd ` B - {y}"
by(subst inj_on_image_set_diff[of snd B]) (use ih(6) xy in auto)
have "x ∉ snd ` B" "y ∉ fst ` B"
using ih(4) xy by(force simp: disjoint_iff)+
thus "fst ` (B - {(x,y)}) ∪ snd ` (B - {(x,y)}) = A - {x,y}"
using ih(3) by(auto simp: * **)
qed(use x ih(4) in "auto intro!: inj_on_diff ih(5,6,7)")
next
assume xy:"(y,x) ∈ B"
show ?thesis
proof(intro ih(2))
have *:"fst ` (B - {(y, x)}) = fst ` B - {y}"
by(subst inj_on_image_set_diff[of fst B]) (use ih(5) xy in auto)
have **: "snd ` (B - {(y, x)}) = snd ` B - {x}"
by(subst inj_on_image_set_diff[of snd B]) (use ih(6) xy in auto)
have "y ∉ snd ` B" "x ∉ fst ` B"
using ih(4) xy by(force simp: disjoint_iff)+
thus "fst ` (B - {(y,x)}) ∪ snd ` (B - {(y,x)}) = A - {x,y}"
using ih(3) by(auto simp: * **)
qed(use x ih(4) in "auto intro!: inj_on_diff ih(5,6,7)")
qed
qed
have "(∑a∈A. f a) = (∑a∈A - {x,y}. f a) + (f x + f y)"
using x y xy' by (simp add: ih(1) sum_diff)
also have "... = k * real (card (A - {x,y})) / 2 + (f x + f y)"
by(simp add: *)
also have "... = k * real (card (A - {x,y})) / 2 + k"
using xy ih(7) by fastforce
also have "... = k * real (card A) / 2"
using x y xy' by(subst card_Diff_subset)
(auto simp: of_nat_diff_if card_le_Suc0_iff_eq[OF ih(1)] not_less_eq_eq right_diff_distrib)
finally show ?thesis .
qed simp
qed
lemma(in prob_space) Markov_inequality_measure_minus:
assumes "u ∈ borel_measurable M" and "AE x in M. 0 ≤ u x" "AE x in M. 1 ≥ u x"
and [arith]: "0 < (a::real)"
shows "𝒫(x in M. u x > 1 - a) ≥ ((∫x. u x ∂M) - (1 - a)) / a"
proof -
have [measurable,simp]:"integrable M u"
using assms by(auto intro!: integrable_const_bound[where B=1])
have "measure M {x∈space M. u x ≤ 1 - a} = measure M {x∈space M. a ≤ 1 - u x}"
by(rule arg_cong[where f="measure M"]) auto
also have "... ≤ (∫x. 1 - u x ∂M) / a"
using assms by(intro integral_Markov_inequality_measure) auto
finally have *:"measure M {x∈space M. u x ≤ 1 - a} ≤ (∫x. 1 - u x ∂M) / a" .
have "((∫x. u x ∂M) - (1 - a)) / a = 1 - (∫x. 1 - u x ∂M) / a"
by (auto simp : prob_space diff_divide_distrib)
also have "... ≤ 1 - measure M {x∈space M. u x ≤ 1 - a}"
using * by simp
also have "... = measure M {x∈space M. ¬ u x ≤ 1 - a}"
by(intro prob_neg[symmetric]) simp
also have "... = measure M {x∈space M. u x > 1 - a}"
by(rule arg_cong[where f="measure M"]) auto
finally show ?thesis .
qed
subsection ‹No-Free-Lunch Theorem›
text ‹ In our implementation, a learning algorithm of binary clasification
is represented as a function
$A :$ @{typ ‹nat ⇒ (nat ⇒ 'a × bool) ⇒ 'a ⇒ bool›}
where the first argument is the number of training data,
the second argument is the training data (\isa{S\ n}$= (x_n, y_n)$ denotes the \isa{n}th data for
a training data \isa{S}),
and \isa{A\ m\ S} is a predictor.
The first argument, which denotes the number of training data,
is normally used to specify the number of loop executions in learning algorithm.
In this formalization, we omit the first argument
because we do not need the concrete definitions of learning algorithms.›
text ‹ Let $X$ be the domain set.
In order to analyze the error of predictors, we assume that each data $(x,y)$ is obtained from
a distribution $\mathcal{D}$ on $X\times \mathbb{B}$.
The error of a predictor $f$ with respect to $\mathcal{D}$ is defined as follows.
\begin{align*}
\mathcal{L}_{\mathcal{D}}(f) &\stackrel{\text{def}}{=} \mathop{\mathrm{P}}_{(x,y)\sim \mathcal{D}}(f(x) \neq y) \\
&= \mathcal{D}(\{(x,y)\in X\times \mathbb{B}\mid f(x)\neq y\})
\end{align*}›
text ‹ In these settings, the no-free-lunch theorem states that
for any learning algorithm $A$ and $m < |X|/2$,
there exists a distribution $\mathcal{D}$ on $X\times \mathbb{B}$
and a predictor $f$ such that
\begin{itemize}
\item $\mathcal{L}_{\mathcal{D}}(f) = 0$, and
\item $\displaystyle \mathop{\mathrm{P}}_{S\sim \mathcal{D}^m}\left(\mathcal{L}_{\mathcal{D}}(A(S)) > \frac{1}{8}\right) \geq \frac{1}{7}$.
\end{itemize}›
theorem no_free_lunch_ML:
fixes X :: "'a measure" and m :: nat
and A :: "(nat ⇒ 'a × bool) ⇒ 'a ⇒ bool"
assumes X1:"finite (space X) ⟹ 2 * m < card (space X)"
and X2[measurable]:"⋀x. x ∈ space X ⟹ {x} ∈ sets X"
and m[arith]:"0 < m"
and A[measurable]: "(λ(s,x). A s x) ∈ (PiM {..<m} (λi. X ⨂⇩M count_space (UNIV :: bool set))) ⨂⇩M X
→⇩M count_space (UNIV :: bool set)"
shows "∃𝒟 :: ('a × bool) measure. sets 𝒟 = sets (X ⨂⇩M count_space (UNIV :: bool set)) ∧
prob_space 𝒟 ∧
(∃f. f ∈ X →⇩M count_space (UNIV :: bool set) ∧ 𝒫((x, y) in 𝒟. f x ≠ y) = 0) ∧
𝒫(s in Pi⇩M {..<m} (λi. 𝒟). 𝒫((x, y) in 𝒟. A s x ≠ y) > 1 / 8) ≥ 1 / 7"
proof -
let ?B = "count_space (UNIV :: bool set)"
let ?B' = "UNIV :: bool set"
let ?L = "λD f. 𝒫((x, y) in D. f x = (¬ y))"
have XB[measurable]: "xy ∈ space (X ⨂⇩M ?B) ⟹ {xy} ∈ sets (X ⨂⇩M ?B)" for xy
by (auto simp: space_pair_measure sets_Pair)
have "space X ≠ {}"
using X1 by force
have "∃C⊆space X. finite C ∧ card C = 2 * m"
by (meson X1 infinite_arbitrarily_large obtain_subset_with_card_n order_less_le)
then obtain C where C: "C ⊆ space X" "finite C" "card C = 2 * m"
by blast
have C_ne:"C ≠ {}"
using C assms by force
have C_sets[measurable]:"C ∈ sets X"
using C by(auto intro!: sets.countable[OF X2 countable_finite])
have meas[measurable]:"{(x, y). (x, y) ∈ space (X ⨂⇩M ?B) ∧ g x = (¬ y)} ∈ sets (X ⨂⇩M ?B)"
if g[measurable]: "g ∈ X →⇩M ?B" for g
proof -
have "{(x, y). (x, y) ∈ space (X ⨂⇩M ?B) ∧ g x = (¬ y)}
= (g -` {True} ∩ space X) × {False} ∪ (g -` {False} ∩ space X) × {True}"
by(auto simp: space_pair_measure)
also have "... ∈ sets (X ⨂⇩M ?B)"
by simp
finally show ?thesis .
qed
define fn where "fn ≡ from_nat_into (C →⇩E (UNIV :: bool set))"
define Dn where "Dn ≡ (λn. measure_of (space (X ⨂⇩M ?B)) (sets (X ⨂⇩M ?B))
(λU. real (card ((SIGMA x:C. {fn n x}) ∩ U)) / real (card C)))"
have fn_PiE:"n < card (C →⇩E ?B') ⟹ fn n ∈ C →⇩E ?B'" for n
by (simp add: PiE_eq_empty_iff fn_def from_nat_into)
have ex_n:"f ∈ C →⇩E ?B' ⟹ ∃n < card (C →⇩E ?B'). f = fn n" for f
using bij_betw_from_nat_into_finite[OF finite_PiE[OF C(2),of "λi. ?B'"]]
by(auto simp: bij_betw_def fn_def)
have fn_inj: "n < card (C →⇩E ?B') ⟹ n' < card (C →⇩E ?B') ⟹ (⋀x. x ∈ C ⟹ fn n x = fn n' x) ⟹ n = n'" for n n'
using bij_betw_from_nat_into_finite[OF finite_PiE[OF C(2),of "λi. ?B'"]] PiE_ext[OF fn_PiE[of n] fn_PiE[of n']]
by(auto simp: bij_betw_def fn_def inj_on_def)
have fn_meas[measurable]:"fn n ∈ X →⇩M ?B" for n
proof -
have "countable (C →⇩E (UNIV :: bool set))"
using C by(auto intro!: countable_PiE)
hence "fn n ∈ C →⇩E (UNIV :: bool set)"
by (simp add: PiE_eq_empty_iff fn_def from_nat_into)
hence "fn n = (λx. if x ∈ C then fn n x else undefined)"
by auto
also have "... ∈ X →⇩M ?B"
proof(subst measurable_restrict_space_iff[symmetric])
have "sets (restrict_space X C) = Pow C"
using X2 C by(intro sets_eq_countable) (auto simp: countable_finite sets_restrict_space_iff)
thus "fn n ∈ restrict_space X C →⇩M ?B"
by (simp add: Measurable.pred_def assms(1))
qed auto
finally show ?thesis .
qed
have sets_Dn[measurable_cong]: "⋀n. sets (Dn n) = sets (X ⨂⇩M ?B)"
and space_Dn:"⋀n. space (Dn n) = space (X ⨂⇩M ?B)"
by(simp_all add: Dn_def)
have emeasure_Dn: "emeasure (Dn n) U = ennreal (real (card ((SIGMA x:C. {fn n x}) ∩ U)) / real (card C))"
(is "_ = ennreal (?μ U)")
if U[measurable]:"U ∈ X ⨂⇩M ?B" for U n
proof(rule emeasure_measure_of[where Ω="space (X ⨂⇩M ?B)" and A="sets (X ⨂⇩M ?B)"])
let ?μ' = "λU. ennreal (?μ U)"
show "countably_additive (sets (Dn n)) ?μ'"
unfolding countably_additive_def
proof safe
fix Ui :: "nat ⇒ _ set"
assume Ui:"range Ui ⊆ sets (Dn n)" "disjoint_family Ui"
have fin: "finite {i. (SIGMA x:C. {fn n x}) ∩ Ui i ≠ {}}" (is "finite ?I")
proof(rule ccontr)
assume "infinite {i. (SIGMA x:C. {fn n x}) ∩ Ui i ≠ {}}"
with Ui(2)
have "infinite (⋃ ((λi. (SIGMA x:C. {fn n x}) ∩ Ui i) ` {i. (SIGMA x:C. {fn n x}) ∩ Ui i ≠ {}}))"
(is "infinite ?𝒰")
by(intro infinite_disjoint_family_imp_infinite_UNION) (auto simp: disjoint_family_on_def)
moreover have "?𝒰 ⊆ (SIGMA x:C. {fn n x})"
by blast
ultimately have "infinite (SIGMA x:C. {fn n x})"
by fastforce
with C(2) show False
by blast
qed
hence sum:"summable (λi. ?μ (Ui i))"
by(intro summable_finite[where N="{i. (SIGMA x:C. {fn n x}) ∩ Ui i ≠ {}}"]) auto
have "(∑i. ?μ' (Ui i)) = ennreal (∑i. ?μ (Ui i))"
by(intro sum suminf_ennreal2) auto
also have "... = (∑i∈?I. ?μ (Ui i))"
by(subst suminf_finite[OF fin]) auto
also have "... = ?μ' (⋃ (range Ui))"
proof -
have *:"(∑i∈?I. real (card ((SIGMA x:C. {fn n x}) ∩ Ui i))) = real (∑i∈?I. (card ((SIGMA x:C. {fn n x}) ∩ Ui i)))"
by simp
also have "... = real (card (⋃ ((λi. (SIGMA x:C. {fn n x}) ∩ Ui i) ` ?I)))"
using C Ui fin unfolding disjoint_family_on_def
by(subst card_UN_disjoint) blast+
also have "... = real (card ((SIGMA x:C. {fn n x}) ∩ ⋃ (range Ui)))"
by(rule arg_cong[where f="λx. real (card x)"]) blast
finally show ?thesis
by(simp add: sum_divide_distrib[symmetric])
qed
finally show "(∑i. ?μ' (Ui i)) = ?μ' (⋃ (range Ui))" .
qed
qed(auto simp: Dn_def positive_def intro!:sets.sets_into_space)
interpret Dn: prob_space "Dn n" for n
proof
have [simp]: "(SIGMA x:C. {fn n x}) ∩ space (X ⨂⇩M ?B) = (SIGMA x:C. {fn n x})"
using measurable_space[OF fn_meas] C(1) space_pair_measure by blast
show "emeasure (Dn n) (space (Dn n)) = 1"
using C_ne C by(simp add: emeasure_Dn space_Dn)
qed
interpret fp: finite_product_prob_space "λi. Dn n" "{..<m}" for n
by standard auto
have measure_Dn: "measure (Dn n) U = real (card ((SIGMA x:C. {fn n x}) ∩ U)) / real (card C)"
if U:"U ∈ X ⨂⇩M ?B" for U n
using emeasure_Dn[OF U] by(simp add: Dn.emeasure_eq_measure)
have measure_Dn': "measure (Dn n) U = (∑x∈C. of_bool ((x,fn n x) ∈ U)) / real (card C)"
if U[measurable]:"U ∈ X ⨂⇩M ?B" for U n
proof -
have *:"(SIGMA x:C. {fn n x}) ∩ U = (SIGMA x:C. {y. y = fn n x ∧ (x,y) ∈ U})"
by blast
have "(x,fn n x) ∈ U ⟹ {y. y = fn n x ∧ (x, y) ∈ U} = {fn n x}"
and "(x,fn n x) ∉ U ⟹ {y. y = fn n x ∧ (x, y) ∈ U} = {}" for x
by blast+
hence **:"real (card {y. y = fn n x ∧ (x, y) ∈ U}) = of_bool ((x,fn n x) ∈ U)" for x
by auto
show ?thesis
by(auto simp: measure_Dn * card_SigmaI[OF C(2)] **)
qed
let ?LossA = "λn s. ?L (Dn n) (A s)"
have [measurable]: "(λs. ?LossA n s) ∈ borel_measurable (PiM {..<m} (λi. X ⨂⇩M ?B))" for n
by measurable (auto simp add: space_Dn)
have Dn_fn_0:"𝒫((x, y) in Dn n. fn n x ≠ y) = 0" for n
proof -
have "(SIGMA x:C. {fn n x}) ∩ {(x, y). (x, y) ∈ space (X ⨂⇩M count_space UNIV) ∧ fn n x = (¬ y)} = {}"
by auto
thus ?thesis
by(simp add: measure_Dn space_Dn)
qed
have [measurable]:"(SIGMA x:C. {fn n x}) ∈ sets (X ⨂⇩M count_space UNIV)" for n
by(rule sets.countable) (use C in "auto intro!: sets_Pair X2 C(1) countable_finite")
have integ[simp]:"integrable (PiM {..<m} (λi. Dn n)) (λs. ?LossA n s)" for n
by(auto intro!: fp.P.integrable_const_bound[where B=1])
have [measurable]:"{xn} ∈ sets (Pi⇩M {..<m} (λi. X ⨂⇩M ?B))"
and fp_prob:"fp.prob n {xn} = 1 / real (card C) ^ m"
if h:"xn ∈ {..<m} →⇩E (SIGMA x:C. {fn n x})" for xn n
proof -
have [simp]: "i < m ⟹ xn i ∈ space (X ⨂⇩M ?B)" for i
using h C(1) by(fastforce simp: PiE_def space_pair_measure Pi_def)
have *:"{xn} = (Π⇩E i∈{..<m}. {xn i})"
proof safe
show "⋀x. x ∈ (Π⇩E i∈{..<m}. {xn i}) ⟹ x = xn"
by standard (metis PiE_E singletonD h)
qed(use h in auto)
also have "... ∈ sets (Pi⇩M {..<m} (λi. X ⨂⇩M ?B))"
by measurable
finally show "{xn} ∈ sets (Pi⇩M {..<m} (λi. X ⨂⇩M ?B))" .
have "fp.prob n (Π⇩E i∈{..<m}. {xn i}) = (∏i<m. Dn.prob n {xn i})"
using h by(intro fp.finite_measure_PiM_emb) simp
also have "... = (1 / real (card C) ^m) "
proof -
have "⋀i. i < m ⟹ ((SIGMA x:C. {fn n x}) ∩ {xn i}) = {xn i}"
using h by blast
thus ?thesis
by(simp add: measure_Dn power_one_over)
qed
finally show "fp.prob n {xn} = 1 / real (card C) ^ m"
using * by simp
qed
have exp_eq:"(∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n))) = (∑s∈{..<m} →⇩E C. ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card C) ^ m" for n
proof -
have "(∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n)))
= (∫s. ?LossA n s * indicat_real (PiE {..<m} (λi. (SIGMA x:C. {fn n x}))) s
+ ?LossA n s * indicat_real (space (PiM {..<m} (λi. Dn n)) - (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))) s ∂(PiM {..<m} (λi. Dn n)))"
by(auto intro!: Bochner_Integration.integral_cong simp: indicator_def)
also have "... = (∫s. ?LossA n s * indicat_real (PiE {..<m} (λi. (SIGMA x:C. {fn n x}))) s ∂(PiM {..<m} (λi. Dn n)))
+ (∫s. ?LossA n s * indicat_real (space (PiM {..<m} (λi. Dn n)) - (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))) s ∂(PiM {..<m} (λi. Dn n)))"
by(rule Bochner_Integration.integral_add)
(auto intro!: fp.P.integrable_const_bound[where B=1] simp: mult_le_one)
also have "... = (∫s. ?LossA n s * indicat_real (PiE {..<m} (λi. (SIGMA x:C. {fn n x}))) s ∂(PiM {..<m} (λi. Dn n)))"
proof -
have *:"(∫s. ?LossA n s * indicat_real (space (PiM {..<m} (λi. Dn n)) - (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))) s ∂(PiM {..<m} (λi. Dn n))) ≥ 0"
by simp
have "(∫s. ?LossA n s * indicat_real (space (PiM {..<m} (λi. Dn n)) - (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))) s ∂(PiM {..<m} (λi. Dn n)))
≤ (∫s. indicat_real (space (PiM {..<m} (λi. Dn n)) - (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))) s ∂(PiM {..<m} (λi. Dn n)))"
by(intro integral_mono) (auto intro!: fp.P.integrable_const_bound[where B=1] simp: mult_le_one indicator_def)
also have "... = 1 - fp.prob n (PiE {..<m} (λi. (SIGMA x:C. {fn n x})))"
by(simp add: fp.P.prob_compl)
also have "... = 0"
using C by(simp add: fp.finite_measure_PiM_emb measure_Dn )
finally show ?thesis
using * by simp
qed
also have "... = (∑s∈{..<m} →⇩E (SIGMA x:C. {fn n x}). ?LossA n s * fp.prob n {s})"
using C by(auto intro!: integral_indicator_finite_real finite_PiE le_neq_trans)
also have "... = (∑s∈{..<m} →⇩E (SIGMA x:C. {fn n x}). ?LossA n s) / real (card C) ^ m"
by(simp add: fp_prob sum_divide_distrib)
also have "... = (∑s∈{..<m} →⇩E C. ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card C) ^ m"
proof -
have *:"{..<m} →⇩E (SIGMA x:C. {fn n x}) = (λs. λi∈{..<m}. (s i, fn n (s i))) ` ({..<m} →⇩E C)"
unfolding set_eq_iff
proof safe
show "s ∈ {..<m} →⇩E (SIGMA x:C. {fn n x}) ⟹ s ∈ (λs. λi∈{..<m}. (s i, fn n (s i))) ` ({..<m} →⇩E C)" for s
by(intro rev_image_eqI[where b=s and x="λi∈{..<m}. fst (s i)"]) (force simp: PiE_def Pi_def extensional_def)+
qed auto
have **:"inj_on (λs. λi∈{..<m}. (s i, fn n (s i))) ({..<m} →⇩E C)"
by(intro inj_onI) (metis (mono_tags, lifting) PiE_ext prod.simps(1) restrict_apply')
show ?thesis
by(subst sum.reindex[where A="{..<m} →⇩E C" and h="λs. λi∈{..<m}. (s i, fn n (s i))",simplified,symmetric])
(use * ** in auto)
qed
finally show ?thesis .
qed
have eqL:"?L (Dn n) h = (∑x∈C. of_bool (h x = (¬ fn n x))) / real (card C)" if h[measurable]:"h ∈ X →⇩M ?B" for n h
proof -
have "?L (Dn n) h = (∑x∈C. of_bool ((x, fn n x) ∈ space (X ⨂⇩M ?B) ∧ h x = (¬ fn n x))) / real (card C)"
by(simp add: space_Dn measure_Dn')
also have "... = (∑x∈C. of_bool (h x = (¬ fn n x))) / real (card C)"
using C by(auto simp: space_pair_measure Collect_conj_eq Int_assoc[symmetric])
finally show ?thesis .
qed
have nz1[arith]:"real (card (C →⇩E ?B')) > 0" "real (card C) > 0" "0 < real (card ({..<m} →⇩E C))"
using C(2) C_ne by(simp_all add: card_funcsetE card_gt_0_iff)
have ne:"finite ((λn. fp.expectation n
(λs. Dn.prob n {(x, y). (x, y) ∈ space (Dn n) ∧ A s x = (¬ y)})) ` {..<card (C →⇩E ?B')})"
"((λn. fp.expectation n
(λs. Dn.prob n {(x, y). (x, y) ∈ space (Dn n) ∧ A s x = (¬ y)})) ` {..<card (C →⇩E ?B')}) ≠ {}" (is ?ne)
proof -
have "0 < card (C →⇩E ?B')"
using C_ne C(2) by(auto simp: card_gt_0_iff finite_PiE)
thus ?ne
by blast
qed simp
have max_geq_q:"(MAX n∈{..<card (C →⇩E ?B')}. (∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n)))) ≥ 1 / 4" (is "_ ≤ ?Max")
proof -
have "(MIN s∈{..<m} →⇩E C. (∑n<card (C →⇩E ?B'). ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card (C →⇩E ?B')))
≤ ?Max" (is "?Min1 ≤ _")
proof -
have "?Min1
≤ (∑s∈{..<m} →⇩E C.
(∑n<card (C →⇩E ?B').
?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card (C →⇩E ?B'))) / real (card ({..<m} →⇩E C))"
proof(subst pos_le_divide_eq)
show "?Min1 * real (card ({..<m} →⇩E C))
≤ (∑s∈{..<m} →⇩E C. (∑n<card (C →⇩E ?B'). ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card (C →⇩E ?B')))"
using C by(simp add: mult.commute) (auto intro!: finite_PiE card_Min_le_sum_of_nat)
qed fact
also have "...
= (∑s∈{..<m} →⇩E C.
(∑n<card (C →⇩E ?B').
?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card (C →⇩E ?B'))) / real (card C) ^ m"
by(simp add: card_PiE)
also have "...
= (∑n<card (C →⇩E ?B').
(∑s∈{..<m} →⇩E C.
?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card C) ^ m) / real (card (C →⇩E ?B'))"
unfolding sum_divide_distrib[symmetric] by(subst sum.swap) simp
also have "... ≤ ?Max"
proof -
have "real (card (C →⇩E ?B')) * ?Max
= real (card (C →⇩E ?B'))
* (MAX n∈{..<card (C →⇩E ?B')}. (∑s∈{..<m} →⇩E C. ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card C) ^ m)"
by (simp add: exp_eq)
also have "... ≥ (∑n<card (C →⇩E ?B'). (∑s∈{..<m} →⇩E C. ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card C) ^ m)"
using sum_le_card_Max_of_nat[of "{..<card (C →⇩E ?B')}"] finite_PiE[OF C(2)] by auto
finally show ?thesis
by(subst pos_divide_le_eq) (simp, argo)
qed
finally show ?thesis .
qed
have "1 / 4 ≤ ?Min1"
proof(safe intro!: Min_ge_iff[THEN iffD2])
fix s
assume s: "s ∈ {..<m} →⇩E C"
hence [measurable]: "(λi∈{..<m}. (s i, fn n (s i))) ∈ space (PiM {..<m} (λi. X ⨂⇩M ?B))" for n
using C by(auto simp: space_PiM space_pair_measure)
let ?V = "C - (s ` {..<m})"
have fin_V:"finite ?V"
using C by blast
have cardV: "card ?V ≥ m"
proof -
have "card (s ` {..<m}) ≤ m"
by (metis card_image_le card_lessThan finite_lessThan)
hence "m ≤ card C - card (s ` {..<m})"
using C(3) by simp
also have "card C - card (s ` {..<m}) ≤ card ?V"
by(rule diff_card_le_card_Diff) simp
finally show ?thesis .
qed
hence V_ne: "?V ≠ {}" "card ?V > 0"
using m by force+
have "(1 / 2) * (1 / 2)
= (1 / 2)
* (MIN v∈?V. (∑n<card (C →⇩E ?B'). of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / real (card (C →⇩E ?B')))"
proof(rule arg_cong[where f="(*) (1 / 2)"])
have "(∑n<card (C →⇩E ?B'). of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / real (card (C →⇩E ?B')) = 1 / 2"
if v:"v ∈ ?V" for v
proof -
define B where "B ≡ {(n, n')|n n'. n < card (C →⇩E ?B') ∧ fn n v = False ∧ n' < card (C →⇩E ?B')
∧ fn n' v = True ∧ (∀x∈C - {v}. fn n x = fn n' x)}"
have B1:"fst ` B ∪ snd ` B = {..<card (C →⇩E ?B')}"
proof -
have "n ∈ fst ` B ∪ snd ` B" if n:"n < card (C →⇩E ?B')" for n
proof(cases "fn n v = True")
assume h:"fn n v = True"
let ?fn' = "λx. if x = v then False else fn n x"
have fn':"⋀x. x ≠ v ⟹ fn n x = ?fn' x" "?fn' v = False"
by auto
hence fn'1:"?fn' ∈ C →⇩E ?B'"
using fn_PiE[OF n] v by auto
then obtain n' where n': "n' < card (C →⇩E ?B')" "fn n' = ?fn'"
using ex_n by (metis (lifting))
hence "(n',n) ∈ B"
using n' fn'1 fn_PiE[OF n] n h fn' by(auto simp: B_def)
thus ?thesis
by force
next
assume h:"fn n v ≠ True"
let ?fn' = "λx. if x = v then True else fn n x"
have fn':"⋀x. x ≠ v ⟹ fn n x = ?fn' x" "?fn' v = True"
by auto
hence fn'1:"?fn' ∈ C →⇩E ?B'"
using fn_PiE[OF n] v by auto
then obtain n' where n': "n' < card (C →⇩E ?B')" "fn n' = ?fn'"
using ex_n by (metis (lifting))
hence "(n,n') ∈ B"
using n' fn'1 fn_PiE[OF n] n h fn' by(auto simp: B_def)
thus ?thesis
by force
qed
moreover have "⋀n. n ∈ fst ` B ∪ snd ` B ⟹ n < card (C →⇩E ?B')"
by(auto simp: B_def)
ultimately show ?thesis
by blast
qed
have B2:"fst ` B ∩ snd ` B = {}"
by(auto simp: B_def)
have B3: "inj_on fst B"
by(auto intro!: fn_inj inj_onI simp: B_def)
have B4: "inj_on snd B"
by(fastforce intro!: fn_inj inj_onI simp: B_def)
have B5:"of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v
= (¬ fn n v)) + of_bool (A (λi∈{..<m}. (s i, fn n' (s i))) v = (¬ fn n' v)) = (1 :: real)"
if nn':"(n,n') ∈ B" for n n'
proof -
have "(λi∈{..<m}. (s i, fn n (s i))) = (λi∈{..<m}. (s i, fn n' (s i)))"
by standard (use s nn' v in "auto simp: B_def")
thus ?thesis
using nn' by(auto simp: B_def)
qed
have "(∑n<card (C →⇩E ?B'). of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v)))
= 1 * real (card {..<card (C →⇩E ?B')}) / 2"
by(intro sum_of_const_pairs[where B=B] B1 B2 B3 B4 B5) simp
thus ?thesis
by simp
qed
thus "1 / 2 = (MIN v∈?V. (∑n<card (C →⇩E ?B'). of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / real (card (C →⇩E ?B')))"
by (metis (mono_tags, lifting) V_ne(1) fin_V obtains_MIN)
qed
also have "...
≤ (1 / 2)
* ((∑v∈?V. (∑n<card (C →⇩E ?B'). of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v)))
/ real (card (C →⇩E ?B')))
/ real (card ?V))"
using V_ne by(intro mult_le_cancel_left_pos[THEN iffD2] pos_le_divide_eq[THEN iffD2])
(simp_all add: Groups.mult_ac(2) card_Min_le_sum_of_nat fin_V)
also have "...
= (∑n<card (C →⇩E ?B'). ((∑v∈?V. of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v)))
/ (2 * real (card ?V))) / real (card (C →⇩E ?B')))"
unfolding sum_divide_distrib[symmetric] by(subst sum.swap) simp
also have "... ≤ (∑n<card (C →⇩E ?B'). ?LossA n (λi∈{..<m}. (s i, fn n (s i))) / real (card (C →⇩E ?B')))"
proof(safe intro!: sum_mono divide_right_mono)
fix n
have "(∑v∈?V. of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / (2 * real (card ?V))
≤ (∑v∈?V. of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / real (card C)"
using cardV by(auto simp: C(3) intro!: divide_left_mono sum_nonneg)
also have "... ≤ (∑x∈C. of_bool (A (λi∈{..<m}. (s i, fn n (s i))) x = (¬ fn n x))) / real (card C)"
using C by(intro sum_mono2 divide_right_mono) auto
also have "... = ?LossA n (λi∈{..<m}. (s i, fn n (s i)))"
by(simp add: eqL)
finally show "(∑v∈?V. of_bool (A (λi∈{..<m}. (s i, fn n (s i))) v = (¬ fn n v))) / (2 * real (card ?V))
≤ ?LossA n (λi∈{..<m}. (s i, fn n (s i)))" .
qed simp
finally show "1 / 4 ≤ (∑n<card (C →⇩E ?B'). ?LossA n (λi∈{..<m}. (s i, fn n (s i)))) / real (card (C →⇩E ?B'))"
by(simp add: sum_divide_distrib)
qed(use m C in "auto intro!: finite_PiE simp: PiE_eq_empty_iff")
also have "... ≤ ?Max"
by fact
finally show ?thesis .
qed
hence "∃n. n < card (C →⇩E ?B') ∧ (∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n))) ≥ 1 / 4"
using Max_ge_iff[OF ne] by blast
then obtain n where n:"n < card (C →⇩E ?B')" "(∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n))) ≥ 1 / 4"
by blast
have "1 / 7 ≤ ((∫s. ?LossA n s ∂(PiM {..<m} (λi. Dn n))) - (1 - 7/ 8)) / (7 / 8)"
using n by argo
also have "... ≤ 𝒫(s in Pi⇩M {..<m} (λi. Dn n). 𝒫((x, y) in Dn n. A s x = (¬ y)) > 1 - 7 / 8)"
by(intro fp.Markov_inequality_measure_minus) auto
also have "... = 𝒫(s in Pi⇩M {..<m} (λi. Dn n). 𝒫((x, y) in Dn n. A s x = (¬ y)) > 1 / 8)"
by simp
finally have "1 / 7 ≤ 𝒫(s in Pi⇩M {..<m} (λi. Dn n). 𝒫((x, y) in Dn n. A s x = (¬ y)) > 1 / 8)" .
thus ?thesis
using Dn_fn_0[of n]
by(auto intro!: exI[where x="Dn n"] exI[where x="fn n"] simp: sets_Dn Dn.prob_space_axioms)
qed
end