Theory McDiarmid_Inequality
section ‹McDiarmid's inequality›
text ‹In this section we verify McDiarmid's inequality \cite[Lemma 1.2]{mcdiarmid1989}. In the
source and also further sources sometimes refer to the result as the ``independent bounded
differences'' inequality.›
theory McDiarmid_Inequality
imports Concentration_Inequalities_Preliminary
begin
lemma Collect_restr_cong:
assumes "A = B"
assumes "⋀x. x ∈ A ⟹ P x = Q x"
shows "{x ∈ A. P x} = {x ∈ B. Q x}"
using assms by auto
lemma ineq_chain:
fixes h :: "nat ⇒ real"
assumes "⋀i. i < n ⟹ h (i+1) ≤ h i"
shows "h n ≤ h 0"
using assms by (induction n) force+
lemma restrict_subset_eq:
assumes "A ⊆ B"
assumes "restrict f B = restrict g B"
shows "restrict f A = restrict g A"
using assms unfolding restrict_def by (meson subsetD)
text ‹Bochner Integral version of Hoeffding's Lemma using
@{thm [source] interval_bounded_random_variable.Hoeffdings_lemma_nn_integral_0}›
lemma (in prob_space) Hoeffdings_lemma_bochner:
assumes "l > 0" and E0: "expectation f = 0"
assumes "random_variable borel f"
assumes "AE x in M. f x ∈ {a..b::real}"
shows "expectation (λx. exp (l * f x)) ≤ exp (l⇧2 * (b - a)⇧2 / 8)" (is "?L ≤ ?R")
proof -
interpret interval_bounded_random_variable M f a b
using assms by (unfold_locales) auto
have "integrable M (λx. exp (l * f x))"
using assms(1,3,4) by (intro integrable_const_bound[where B="exp (l * b)"]) simp_all
hence "ennreal (?L) = (∫⇧+ x. exp (l * f x) ∂M)"
by (intro nn_integral_eq_integral[symmetric]) auto
also have "... ≤ ennreal (?R)"
by (intro Hoeffdings_lemma_nn_integral_0 assms)
finally have 0:"ennreal (?L) ≤ ennreal ?R"
by simp
show ?thesis
proof (cases "?L ≥ 0")
case True
thus ?thesis using 0 by simp
next
case False
hence "?L ≤ 0" by simp
also have "... ≤ ?R" by simp
finally show ?thesis by simp
qed
qed
lemma (in prob_space) Hoeffdings_lemma_bochner_2:
assumes "l > 0" and E0: "expectation f = 0"
assumes "random_variable borel f"
assumes "⋀x y. {x,y} ⊆ space M ⟹ ¦f x - f y¦ ≤ (c::real)"
shows "expectation (λx. exp (l * f x)) ≤ exp (l^2 * c^2 / 8)" (is "?L ≤ ?R")
proof -
define a :: real where "a = (INF x ∈ space M. f x)"
define b :: real where "b = a+c"
obtain ω where ω:"ω ∈ space M" using not_empty by auto
hence 0:"f ` space M ≠ {}" by auto
have 1: "c = b - a" unfolding b_def by simp
have "bdd_below (f ` space M)"
using ω assms(4) unfolding abs_le_iff
by (intro bdd_belowI[where m="f ω - c"]) (auto simp add:algebra_simps)
hence "f x ≥ a" if "x ∈ space M" for x unfolding a_def by (intro cINF_lower that)
moreover have "f x ≤ b" if x_space: "x ∈ space M" for x
proof (rule ccontr)
assume "¬(f x ≤ b)"
hence a:"f x > a + c" unfolding b_def by simp
have "f y ≥ f x - c" if "y ∈ space M" for y
using that x_space assms(4) unfolding abs_le_iff by (simp add:algebra_simps)
hence "f x - c ≤ a" unfolding a_def using cInf_greatest[OF 0] by auto
thus "False" using a by simp
qed
ultimately have "f x ∈ {a..b}" if "x ∈ space M" for x using that by auto
hence "AE x in M. f x ∈ {a..b}" by simp
thus ?thesis unfolding 1 by (intro Hoeffdings_lemma_bochner assms(1,2,3))
qed
lemma (in prob_space) Hoeffdings_lemma_bochner_3:
assumes "expectation f = 0"
assumes "random_variable borel f"
assumes "⋀x y. {x,y} ⊆ space M ⟹ ¦f x - f y¦ ≤ (c::real)"
shows "expectation (λx. exp (l * f x)) ≤ exp (l^2 * c^2 / 8)" (is "?L ≤ ?R")
proof -
consider (a) "l > 0" | (b) "l = 0" | (c) "l < 0"
by argo
then show ?thesis
proof (cases)
case a thus ?thesis by (intro Hoeffdings_lemma_bochner_2 assms) auto
next
case b thus ?thesis by simp
next
case c
have "?L = expectation (λx. exp ((-l) * (-f x)))" by simp
also have "... ≤ exp ((-l)^2 * c⇧2/8)" using c assms by (intro Hoeffdings_lemma_bochner_2) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed
qed
text ‹Version of @{thm [source] product_sigma_finite.product_integral_singleton} without the
condition that @{term "M i"} has to be sigma finite for all @{term "i"}:›
lemma product_integral_singleton:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "sigma_finite_measure (M i)"
assumes "f ∈ borel_measurable (M i)"
shows "(∫x. f (x i) ∂(PiM {i} M)) = (∫x. f x ∂(M i))" (is "?L = ?R")
proof -
define M' where "M' j = (if j=i then M i else count_space {undefined})" for j
interpret product_sigma_finite "M'"
using assms(1) unfolding product_sigma_finite_def M'_def
by (auto intro!:sigma_finite_measure_count_space_finite)
have "?L = ∫x. f (x i) ∂(PiM {i} M')"
by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def)
also have "... = (∫x. f x ∂(M' i))"
using assms(2) by (intro product_integral_singleton) (simp add:M'_def)
also have "... = ?R"
by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def)
finally show ?thesis by simp
qed
text ‹Version of @{thm [source] product_sigma_finite.product_integral_fold} without the
condition that @{term "M i"} has to be sigma finite for all @{term "i"}:›
lemma product_integral_fold:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "⋀i. i ∈ I ∪ J ⟹ sigma_finite_measure (M i)"
assumes "I ∩ J = {}"
assumes "finite I"
assumes "finite J"
assumes "integrable (PiM (I ∪ J) M) f"
shows "(∫x. f x ∂PiM (I ∪ J) M) = (∫x. (∫y. f (merge I J(x,y)) ∂PiM J M) ∂PiM I M)" (is "?L = ?R")
and "integrable (PiM I M) (λx. (∫y. f (merge I J(x,y)) ∂PiM J M))" (is "?I")
and "AE x in PiM I M. integrable (PiM J M) (λy. f (merge I J(x,y)))" (is "?T")
proof -
define M' where "M' i = (if i ∈ I ∪ J then M i else count_space {undefined})" for i
interpret product_sigma_finite "M'"
using assms(1) unfolding product_sigma_finite_def M'_def
by (auto intro!:sigma_finite_measure_count_space_finite)
interpret pair_sigma_finite "Pi⇩M I M'" "Pi⇩M J M'"
using assms(3,4) sigma_finite unfolding pair_sigma_finite_def by blast
have 0: "integrable (Pi⇩M (I ∪ J) M') f = integrable (Pi⇩M (I ∪ J) M) f"
by (intro Bochner_Integration.integrable_cong PiM_cong) (simp_all add:M'_def)
have "?L = (∫x. f x ∂PiM (I ∪ J) M')"
by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def)
also have "... = (∫x. (∫y. f (merge I J (x,y)) ∂PiM J M') ∂PiM I M')"
using assms(5) by (intro product_integral_fold assms(2,3,4)) (simp add:0)
also have "... = ?R"
by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def)
finally show "?L = ?R" by simp
have "integrable (Pi⇩M (I ∪ J) M') f = integrable (PiM I M' ⨂⇩M PiM J M') (λx. f (merge I J x))"
using assms(5) apply (subst distr_merge[OF assms(2,3,4),symmetric])
by (intro integrable_distr_eq) (simp_all add:0[symmetric])
hence 1:"integrable (PiM I M' ⨂⇩M PiM J M') (λx. f (merge I J x))"
using assms(5) 0 by simp
hence "integrable (PiM I M') (λx. (∫y. f (merge I J(x,y)) ∂PiM J M'))" (is "?I'")
by (intro integrable_fst') auto
moreover have "?I' = ?I"
by (intro Bochner_Integration.integrable_cong PiM_cong ext Bochner_Integration.integral_cong)
(simp_all add:M'_def)
ultimately show "?I"
by simp
have "AE x in Pi⇩M I M'. integrable (Pi⇩M J M') (λy. f (merge I J (x, y)))" (is "?T'")
by (intro AE_integrable_fst'[OF 1])
moreover have "?T' = ?T"
by (intro arg_cong2[where f="almost_everywhere"] PiM_cong ext Bochner_Integration.integrable_cong)
(simp_all add:M'_def)
ultimately show "?T"
by simp
qed
lemma product_integral_insert:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "⋀k. k ∈ {i} ∪ J ⟹ sigma_finite_measure (M k)"
assumes "i ∉ J"
assumes "finite J"
assumes "integrable (PiM (insert i J) M) f"
shows "(∫x. f x ∂PiM (insert i J) M) = (∫x. (∫y. f (y(i := x)) ∂PiM J M) ∂M i)" (is "?L = ?R")
proof -
note meas_cong = iffD1[OF measurable_cong]
have "integrable (PiM {i} M) (λx. (∫y. f (merge {i} J (x,y)) ∂PiM J M))"
using assms by (intro product_integral_fold) auto
hence 0:"(λx. (∫y. f (merge {i} J (x,y)) ∂PiM J M)) ∈ borel_measurable (PiM {i} M)"
using borel_measurable_integrable by simp
have 1:"(λx. (∫y. f (y(i := (x i))) ∂PiM J M)) ∈ borel_measurable (PiM {i} M)"
by (intro meas_cong[OF _ 0] Bochner_Integration.integral_cong arg_cong[where f="f"])
(auto simp add:space_PiM merge_def fun_upd_def PiE_def extensional_def)
have "(λx. (∫y. f (y(i := (λi∈{i}. x) i)) ∂PiM J M)) ∈ borel_measurable (M i)"
by (intro measurable_compose[OF _ 1, where f="(λx. (λi∈{i}. x))"] measurable_restrict) auto
hence 2:"(λx. (∫y. f (y(i := x )) ∂PiM J M)) ∈ borel_measurable (M i)" by simp
have "?L = (∫x. f x ∂PiM ({i} ∪ J) M)" by simp
also have "... = (∫x. (∫y. f (merge {i} J (x,y)) ∂PiM J M) ∂PiM {i} M)"
using assms(2,4) by (intro product_integral_fold assms(1,3)) auto
also have "... = (∫x. (∫y. f (y(i := (x i))) ∂PiM J M) ∂PiM {i} M)"
by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"])
(auto simp add:space_PiM merge_def fun_upd_def PiE_def extensional_def)
also have "... = ?R"
using assms(1,4) by (intro product_integral_singleton assms(1) 2) auto
finally show ?thesis by simp
qed
lemma product_integral_insert_rev:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "⋀k. k ∈ {i} ∪ J ⟹ sigma_finite_measure (M k)"
assumes "i ∉ J"
assumes "finite J"
assumes "integrable (PiM (insert i J) M) f"
shows "(∫x. f x ∂PiM (insert i J) M) = (∫y. (∫x. f (y(i := x)) ∂M i) ∂PiM J M)" (is "?L = ?R")
proof -
have "?L = (∫x. f x ∂PiM (J ∪ {i}) M)" by simp
also have "... = (∫x. (∫y. f (merge J {i} (x,y)) ∂PiM {i} M) ∂PiM J M)"
using assms(2,4) by (intro product_integral_fold assms(1,3)) auto
also have "... = (∫x. (∫y. f (x(i := (y i))) ∂PiM {i} M) ∂PiM J M)"
unfolding merge_singleton[OF assms(2)]
by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"])
(metis PiE_restrict assms(2) restrict_upd space_PiM)
also have "... = ?R"
using assms(1,4) by (intro Bochner_Integration.integral_cong product_integral_singleton) auto
finally show ?thesis by simp
qed
lemma merge_empty[simp]:
"merge {} I (y,x) = restrict x I"
"merge I {} (y,x) = restrict y I"
unfolding merge_def restrict_def by auto
lemma merge_cong:
assumes "restrict x1 I = restrict x2 I"
assumes "restrict y1 J = restrict y2 J"
shows "merge I J (x1,y1) = merge I J (x2,y2)"
using assms unfolding merge_def restrict_def
by (intro ext) (smt (verit, best) case_prod_conv)
lemma restrict_merge:
"restrict (merge I J x) K = merge (I ∩ K) (J ∩ K) x"
unfolding restrict_def merge_def by (intro ext) (auto simp:case_prod_beta)
lemma map_prod_measurable:
assumes "f ∈ M →⇩M M'"
assumes "g ∈ N →⇩M N'"
shows "map_prod f g ∈ M ⨂⇩M N →⇩M M' ⨂⇩M N'"
using assms by (subst measurable_pair_iff) simp
lemma mc_diarmid_inequality_aux:
fixes f :: "(nat ⇒ 'a) ⇒ real"
fixes n :: nat
assumes "⋀i. i < n ⟹ prob_space (M i)"
assumes "⋀i x y. i<n ⟹ {x,y} ⊆ space (PiM {..<n} M) ⟹ (∀j∈{..<n}-{i}. x j=y j) ⟹ ¦f x-f y¦≤c i"
assumes f_meas: "f ∈ borel_measurable (PiM {..<n} M)" and ε_gt_0: "ε >0"
shows "𝒫(ω in PiM {..<n} M. f ω - (∫ξ. f ξ ∂PiM {..<n} M) ≥ ε) ≤ exp (-(2*ε^2)/(∑i<n. (c i)^2))"
(is "?L ≤ ?R")
proof -
define h where "h k = (λξ. (∫ω. f (merge {..<k} {k..<n} (ξ, ω)) ∂PiM {k..<n} M))" for k
define t :: real where "t = 4 * ε / (∑i<n. (c i)^2)"
define V where "V i ξ = h (Suc i) ξ - h i ξ" for i ξ
obtain x0 where x0:"x0 ∈ space (PiM {..<n} M)"
using prob_space.not_empty[OF prob_space_PiM] assms(1) by fastforce
have delta: "¦f x - f y¦ ≤ c i" if "i < n"
"x ∈ PiE {..<n} (λi. space (M i))" "y ∈ PiE {..<n} (λi. space (M i))"
"restrict x ({..<n}-{i}) = restrict y ({..<n}-{i})"
for x y i
proof (rule assms(2)[OF that(1)], goal_cases)
case 1
then show ?case using that(2,3) unfolding space_PiM by auto
next
case 2
then show ?case using that(4) by (intro ballI) (metis restrict_apply')
qed
have c_ge_0: "c j ≥ 0" if "j < n" for j
proof -
have "0 ≤ ¦f x0 - f x0¦" by simp
also have "... ≤ c j" using x0 unfolding space_PiM by (intro delta that) auto
finally show ?thesis by simp
qed
hence sum_c_ge_0: "(∑i<n. (c i)^2) ≥ 0" by (meson sum_nonneg zero_le_power2)
hence t_ge_0: "t ≥ 0" using ε_gt_0 unfolding t_def by simp
note borel_rules =
borel_measurable_sum measurable_compose[OF _ borel_measurable_exp]
borel_measurable_times
note int_rules =
prob_space_PiM assms(1) borel_rules
prob_space.integrable_bounded bounded_intros
have h_n: "h n ξ = f ξ" if "ξ ∈ space (PiM {..<n} M)" for ξ
proof -
have "h n ξ = (∫ω. f (λi∈{..<n}. ξ i) ∂PiM {} M)"
unfolding h_def using leD
by (intro Bochner_Integration.integral_cong PiM_cong arg_cong[where f="f"] restrict_cong)
auto
also have "... = f (restrict ξ {..<n})"
unfolding PiM_empty by simp
also have "... = f ξ"
using that unfolding space_PiM PiE_def
by (simp add: extensional_restrict)
finally show ?thesis
by simp
qed
have h_0: "h 0 ξ = (∫ω. f ω ∂PiM {..<n} M)" for ξ
unfolding h_def by (intro Bochner_Integration.integral_cong PiM_cong refl)
(simp_all add:space_PiM atLeast0LessThan)
have h_cong: "h j ω = h j ξ" if "restrict ω {..<j} = restrict ξ {..<j}" for j ω ξ
using that unfolding h_def
by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"] merge_cong) auto
have h_meas: "h i ∈ borel_measurable (PiM I M)" if "i ≤ n" "{..<i} ⊆ I" for i I
proof -
have 0: "{..<n} = {..<i} ∪ {i..<n}"
using that(1) by auto
have 1: "merge {..<i} {i..<n} = merge {..<i} {i..<n} ∘ map_prod (λx. restrict x {..<i}) id"
unfolding merge_def map_prod_def restrict_def comp_def
by (intro ext) (auto simp:case_prod_beta')
have "merge {..<i} {i..<n} ∈ Pi⇩M I M ⨂⇩M Pi⇩M {i..<n} M →⇩M Pi⇩M {..<n} M"
unfolding 0 by (subst 1) (intro measurable_comp[OF _ measurable_merge] map_prod_measurable
measurable_ident measurable_restrict_subset that(2))
hence "(λx. f (merge {..<i} {i..<n} x)) ∈ borel_measurable (Pi⇩M I M ⨂⇩M Pi⇩M {i..<n} M)"
by (intro measurable_compose[OF _ f_meas])
thus ?thesis
unfolding h_def by (intro sigma_finite_measure.borel_measurable_lebesgue_integral
prob_space_imp_sigma_finite prob_space_PiM assms(1)) (auto simp:case_prod_beta')
qed
have merge_space_aux:"merge {..<j} {j..<n} u ∈ (Π⇩E i∈{..<n}. space (M i))"
if "j ≤ n" "fst u ∈ Pi {..<j} (λi. space (M i))" "snd u ∈ Pi {j..<n} (λi. space (M i))"
for u j
proof -
have "merge {..<j} {j..<n} (fst u, snd u) ∈ (PiE ({..<j} ∪ {j..<n}) (λi. space (M i)))"
using that by (intro iffD2[OF PiE_cancel_merge]) auto
also have "... = (Π⇩E i∈{..<n}. space (M i))"
using that by (intro arg_cong2[where f="PiE"] refl) auto
finally show ?thesis by simp
qed
have merge_space:"merge {..<j} {j..<n} (u, v) ∈ (Π⇩E i∈{..<n}. space (M i))"
if "j ≤ n" "u ∈ PiE {..<j} (λi. space (M i))" "v ∈ PiE {j..<n} (λi. space (M i))"
for u v j
using that by (intro merge_space_aux) (simp_all add:PiE_def)
have delta': "¦f x - f y¦ ≤ (∑i<n. c i)"
if "x ∈ PiE {..<n} (λi. space (M i))" "y ∈ PiE {..<n} (λi. space (M i))" for x y
proof -
define m where "m i = merge {..<i} {i..<n} (x,y)" for i
have 0: "z ∈ Pi I (λi. space (M i))" if "z ∈ PiE {..<n} (λi. space (M i))"
"I ⊆ {..<n}" for z I
using that unfolding PiE_def by auto
have 3: "{..<Suc i} ∩ ({..<n} - {i}) = {..<i}"
"{Suc i..<n} ∩ ({..<n} - {i}) = {Suc i..<n}"
"{..<i} ∩ ({..<n} - {i}) = {..<i}"
"{i..<n} ∩ ({..<n} - {i}) = {Suc i..<n}"
if "i < n" for i
using that by auto
have "¦f x - f y¦ = ¦f (m n) - f(m 0)¦"
using that unfolding m_def by (simp add:atLeast0LessThan)
also have "... = ¦∑i < n. f (m (Suc i)) - f (m i)¦"
by (subst sum_lessThan_telescope) simp
also have "... ≤ (∑i < n. ¦f (m (Suc i)) - f (m i)¦)"
by simp
also have "... ≤ (∑i < n. c i)"
using that unfolding m_def by (intro delta sum_mono merge_space_aux 0 subsetI)
(simp_all add:restrict_merge 3)
finally show ?thesis
by simp
qed
have "norm (f x) ≤ norm (f x0) + sum c {..<n}" if "x ∈ space (Pi⇩M {..<n} M)" for x
proof -
have "¦f x - f x0¦ ≤ sum c {..<n}"
using x0 that unfolding space_PiM by (intro delta') auto
thus ?thesis
by simp
qed
hence f_bounded: "bounded (f ` space (PiM {..<n} M))"
by (intro boundedI[where B="norm (f x0) + (∑i<n. c i)"]) auto
have f_merge_bounded:
"bounded ((λω. (f (merge {..<j} {j..<n} (u, ω)))) ` space (Pi⇩M {j..<n} M))"
if "j ≤ n" "u ∈ PiE {..<j} (λi. space (M i))" for u j
proof -
have "(λω. merge {..<j} {j..<n} (u, ω)) ` space (Pi⇩M {j..<n} M) ⊆ space (Pi⇩M {..<n} M)"
using that unfolding space_PiM
by (intro image_subsetI merge_space) auto
thus ?thesis
by (subst image_image[of "f",symmetric]) (intro bounded_subset[OF f_bounded] image_mono)
qed
have f_merge_meas_aux:
"(λω. f (merge {..<j} {j..<n} (u, ω))) ∈ borel_measurable (Pi⇩M {j..<n} M)"
if "j ≤ n" "u ∈ Pi {..<j} (λi. space (M i))" for j u
proof -
have 0: "{..<n} = {..<j } ∪ {j ..<n}"
using that(1) by auto
have 1: "merge {..<j} {j..<n} (u,ω) = merge {..<j} {j..<n} (restrict u {..<j},ω)" for ω
by (intro merge_cong) auto
have "(λω. merge {..<j} {j..<n} (u, ω)) ∈ Pi⇩M {j..<n} M →⇩M Pi⇩M {..<n} M"
using that unfolding 0 1
by (intro measurable_compose[OF _ measurable_merge] measurable_Pair1')
(simp add:space_PiM)
thus ?thesis
by (intro measurable_compose[OF _ f_meas])
qed
have f_merge_meas: "(λω. f (merge {..<j} {j..<n} (u, ω))) ∈ borel_measurable (Pi⇩M {j..<n} M)"
if "j ≤ n" "u ∈ PiE {..<j} (λi. space (M i))" for j u
using that unfolding PiE_def by (intro f_merge_meas_aux) auto
have h_bounded: "bounded (h i ` space (PiM I M))"
if h_bounded_assms: "i ≤ n" "{..<i} ⊆ I" for i I
proof -
have "merge {..<i} {i..<n} x ∈ space (Pi⇩M {..<n} M)"
if "x ∈ (Π⇩E i∈I. space (M i)) × (Π⇩E i∈{i..<n}. space (M i))" for x
using that h_bounded_assms unfolding space_PiM by (intro merge_space_aux)
(auto simp: PiE_def mem_Times_iff)
hence "bounded ((λx. f (merge {..<i} {i..<n} x)) `
((Π⇩E i∈I. space (M i)) × (Π⇩E i∈{i..<n}. space (M i))))"
by (subst image_image[of "f",symmetric])
(intro bounded_subset[OF f_bounded] image_mono image_subsetI)
thus ?thesis
using that unfolding h_def
by (intro prob_space.finite_measure finite_measure.bounded_int int_rules)
(auto simp:space_PiM PiE_def)
qed
have V_bounded: "bounded (V i ` space (PiM I M))"
if "i < n" "{..<i+1} ⊆ I" for i I
using that unfolding V_def by (intro bounded_intros h_bounded) auto
have V_upd_bounded: "bounded ((λx. V j (ξ(j := x))) ` space (M j))"
if V_upd_bounded_assms: "ξ ∈ space (Pi⇩M {..<j} M)" "j < n" for j ξ
proof -
have "ξ(j := v) ∈ space (Pi⇩M {..<j + 1} M)" if "v ∈ space (M j)" for v
using V_upd_bounded_assms that unfolding space_PiM PiE_def extensional_def Pi_def by auto
thus ?thesis
using that unfolding image_image[of "V j" "(λx. (ξ(j := x)))",symmetric]
by (intro bounded_subset[OF V_bounded[of "j" "{..<j+1}"]] that image_mono) auto
qed
have h_step: "h j ω = ∫τ. h (j+1) (ω (j := τ)) ∂ M j" (is "?L1 = ?R1")
if "ω ∈ space (PiM {..<j} M)" "j < n" for j ω
proof -
have 0: "(λx. f (merge {..<j} {j..<n} (ω, x))) ∈ borel_measurable (Pi⇩M {j..<n} M)"
using that unfolding space_PiM by (intro f_merge_meas) auto
have 1: "insert j {Suc j..<n} = {j..<n}"
using that by auto
have 2: "bounded ((λx.(f (merge {..<j} {j..<n} (ω, x)))) ` space (Pi⇩M {j..<n} M))"
using that by (intro f_merge_bounded) (simp_all add: space_PiM)
have "?L1 = (∫ξ. f (merge {..<j} {j..<n} (ω, ξ)) ∂PiM (insert j {j+1..<n}) M)"
unfolding h_def using that by (intro Bochner_Integration.integral_cong refl PiM_cong) auto
also have "...=(∫τ.(∫ξ. f (merge {..<j} {j..<n} (ω, (ξ(j := τ)))) ∂PiM {j+1..<n} M)∂M j)"
using that(1,2) 0 1 2 by (intro product_integral_insert prob_space_imp_sigma_finite assms(1)
int_rules f_merge_meas) (simp_all)
also have "... = ?R1"
using that(2) unfolding h_def
by (intro Bochner_Integration.integral_cong arg_cong[where f="f"] ext) (auto simp:merge_def)
finally show ?thesis
by simp
qed
have V_meas: "V i ∈ borel_measurable (PiM I M)" if "i < n" "{..<i+1} ⊆ I" for i I
unfolding V_def using that by (intro borel_measurable_diff h_meas) auto
have V_upd_meas: "(λx. V j (ξ(j := x))) ∈ borel_measurable (M j)"
if "j < n" "ξ ∈ space (Pi⇩M {..<j} M)" for j ξ
using that by (intro measurable_compose[OF _ V_meas[where I="insert j {..<j}"]]
measurable_component_update) auto
have V_cong:
"V j ω = V j ξ" if "restrict ω {..<(j+1)} = restrict ξ {..<(j+1)}" for j ω ξ
using that restrict_subset_eq[OF _ that] unfolding V_def
by (intro arg_cong2[where f="(-)"] h_cong) simp_all
have exp_V: "(∫ω. V j (ξ(j := ω)) ∂M j) = 0" (is "?L1 = 0")
if "j < n" "ξ ∈ space (PiM {..<j} M)" for j ξ
proof -
have "fun_upd ξ j ` space (M j) ⊆ space (Pi⇩M (insert j {..<j}) M)"
using that unfolding space_PiM by (intro image_subsetI PiE_fun_upd) auto
hence 0:"bounded ((λx. h (Suc j) (ξ(j := x))) ` space (M j))"
unfolding image_image[of "h (Suc j)" "λx. ξ(j := x)",symmetric] using that
by (intro bounded_subset[OF h_bounded[where i="j+1" and I="{..<j+1}"]] image_mono)
(auto simp:lessThan_Suc)
have 1:"(λx. h (Suc j) (ξ(j := x))) ∈ borel_measurable (M j)"
using h_meas that by (intro measurable_compose[OF _ h_meas[where I="insert j {..<j}"]]
measurable_component_update) auto
have "?L1 =(∫ω. h (Suc j) (ξ(j := ω)) - h j ξ ∂M j)"
unfolding V_def
by (intro Bochner_Integration.integral_cong arg_cong2[where f="(-)"] refl h_cong) auto
also have "... = (∫ω. h (Suc j) (ξ(j := ω)) ∂M j) - (∫ω. h j ξ ∂M j)"
using that by (intro Bochner_Integration.integral_diff int_rules 0 1) auto
also have "... = 0"
using that(1) assms(1) prob_space.prob_space unfolding h_step[OF that(2,1)] by auto
finally show ?thesis
by simp
qed
have var_V: "¦V j x - V j y¦ ≤ c j" (is "?L1 ≤ ?R1")
if var_V_assms: "j < n" "{x,y} ⊆ space (PiM {..<j+1} M)"
"restrict x {..<j} = restrict y {..<j}" for x y j
proof -
have x_ran: "x ∈ PiE {..<j+1} (λi. space (M i))" and y_ran: "y ∈ PiE {..<j+1} (λi. space (M i))"
using that(2) by (simp_all add:space_PiM)
have 0: "j+1 ≤ n"
using that by simp
have "?L1 = ¦h (Suc j) x - h j y - (h (Suc j) y - h j y)¦"
unfolding V_def by (intro arg_cong[where f="abs"] arg_cong2[where f="(-)"] refl h_cong that)
also have "... = ¦h (j+1) x - h (j+1) y¦"
by simp
also have "... =
¦(∫ω. f(merge {..<j+1} {j+1..<n} (x,ω))-f(merge {..<j+1} {j+1..<n} (y,ω)) ∂PiM {j+1..<n} M)¦"
using that unfolding h_def by (intro arg_cong[where f="abs"] f_merge_meas[OF 0] x_ran
Bochner_Integration.integral_diff[symmetric] int_rules f_merge_bounded[OF 0] y_ran) auto
also have "... ≤
(∫ω. ¦f(merge {..<j+1} {j+1..<n} (x,ω))-f(merge {..<j+1} {j+1..<n} (y,ω))¦ ∂PiM {j+1..<n} M)"
by (intro integral_abs_bound)
also have "... ≤ (∫ω. c j ∂PiM {j+1..<n} M)"
proof (intro Bochner_Integration.integral_mono' delta int_rules c_ge_0 ballI merge_space 0)
fix ω assume "ω ∈ space (Pi⇩M {j + 1..<n} M)"
have "{..<j + 1} ∩ ({..<n} - {j}) = {..<j}"
using that by auto
thus "restrict (merge {..<j+1} {j+1..<n} (x, ω)) ({..<n}-{j}) =
restrict (merge {..<j+1} {j+1..<n} (y, ω)) ({..<n}-{j})"
using that(1,3) less_antisym unfolding restrict_merge by (intro merge_cong refl) auto
qed (simp_all add: space_PiM that(1) x_ran[simplified] y_ran[simplified])
also have "... = c j"
by (auto intro!:prob_space.prob_space prob_space_PiM assms(1))
finally show ?thesis by simp
qed
have "f ξ - (∫ω. f ω ∂(PiM {..<n} M)) = (∑i < n. V i ξ)" if "ξ ∈ space (PiM {..<n} M)" for ξ
using that unfolding V_def by (subst sum_lessThan_telescope) (simp add: h_0 h_n)
hence "?L = 𝒫(ξ in PiM {..<n} M. (∑i < n. V i ξ) ≥ ε)"
by (intro arg_cong2[where f="measure"] refl Collect_restr_cong arg_cong2[where f="(≤)"]) auto
also have "... ≤ 𝒫(ξ in PiM {..<n} M. exp( t * (∑i < n. V i ξ) ) ≥ exp (t * ε))"
proof (intro finite_measure.finite_measure_mono subsetI prob_space.finite_measure int_rules)
show "{ξ ∈ space (Pi⇩M {..<n} M). exp (t * ε) ≤ exp (t * (∑i<n. V i ξ))} ∈ sets (Pi⇩M {..<n} M)"
using V_meas by measurable
qed (auto intro!:mult_left_mono[OF _ t_ge_0])
also have "... ≤ (∫ξ. exp(t*(∑i < n. V i ξ)) ∂PiM {..<n} M)/ exp (t*ε)"
by (intro integral_Markov_inequality_measure[where A="{}"] int_rules V_bounded V_meas) auto
also have "... = exp(t^2 * (∑i∈{n..<n}. c i^2)/8-t*ε)*(∫ξ. exp(t*(∑i < n. V i ξ)) ∂PiM {..<n} M)"
by (simp add:exp_minus inverse_eq_divide)
also have "... ≤ exp(t^2 * (∑i∈{0..<n}. c i^2)/8-t*ε)*(∫ξ. exp(t*(∑i < 0. V i ξ)) ∂PiM {..<0} M)"
proof (rule ineq_chain)
fix j assume a:"j < n"
let ?L1 = "exp (t⇧2*(∑i=j+1..<n. (c i)⇧2)/8-t*ε)"
let ?L2 = "?L1 * (∫ξ. exp (t * (∑i<j+1. V i ξ)) ∂PiM {..<j+1} M)"
note V_upd_meas = V_upd_meas[OF a]
have "?L2 = ?L1 * (∫ξ. exp (t * (∑i<j. V i ξ)) * exp(t * V j ξ) ∂PiM (insert j {..<j}) M)"
by (simp add:algebra_simps exp_add lessThan_Suc)
also have "... = ?L1 *
(∫ξ. (∫ω. exp (t * (∑i<j. V i (ξ(j := ω)))) * exp(t * V j (ξ(j := ω))) ∂M j) ∂PiM {..<j} M)"
using a by (intro product_integral_insert_rev arg_cong2[where f="(*)"] int_rules
prob_space_imp_sigma_finite V_bounded V_meas) auto
also have "... =?L1*(∫ξ.(∫ω. exp (t*(∑i<j. V i ξ))*exp(t*V j (ξ(j := ω))) ∂M j) ∂PiM {..<j} M)"
by (intro arg_cong2[where f="(*)"] Bochner_Integration.integral_cong
arg_cong[where f="exp"] sum.cong V_cong restrict_fupd) auto
also have "... =?L1*(∫ξ. exp (t*(∑i<j. V i ξ))*(∫ω. exp(t*V j (ξ(j := ω))) ∂M j) ∂PiM {..<j} M)"
using a by (intro arg_cong2[where f="(*)"] Bochner_Integration.integral_cong refl
Bochner_Integration.integral_mult_right V_upd_meas V_upd_bounded int_rules) auto
also have "... ≤ ?L1 * ∫ξ. exp (t*(∑i<j. V i ξ))* exp (t^2 * c j^2/8) ∂PiM {..<j} M"
proof (intro mult_left_mono integral_mono')
fix ξ assume c:"ξ ∈ space (Pi⇩M {..<j} M)"
hence b:"ξ ∈ PiE {..<j} (λi. space (M i))"
unfolding space_PiM by simp
moreover have "ξ(j := v) ∈ PiE {..<j+1} (λi. space (M i))" if "v ∈ space (M j)" for v
using b that unfolding PiE_def extensional_def Pi_def by auto
ultimately show "LINT ω|M j. exp (t * V j (ξ(j := ω))) ≤ exp (t⇧2 * (c j)⇧2 / 8)"
using V_upd_meas[OF c]
by (intro prob_space.Hoeffdings_lemma_bochner_3 exp_V var_V a int_rules)
(auto simp: space_PiM)
next
show "integrable (Pi⇩M {..<j} M) (λx. exp (t * (∑i<j. V i x)) * exp (t⇧2 * (c j)⇧2 / 8))"
using a by (intro int_rules V_bounded V_meas) auto
qed auto
also have "... = ?L1 * ((∫ξ. exp (t*(∑i<j. V i ξ)) ∂PiM {..<j} M) * exp (t^2 * c j^2/8))"
proof (subst Bochner_Integration.integral_mult_left)
show "integrable (Pi⇩M {..<j} M) (λξ. exp (t * (∑i<j. V i ξ)))"
using a by (intro int_rules V_bounded V_meas) auto
qed auto
also have "... =
exp (t⇧2*(∑i∈insert j {j+1..<n}. (c i)⇧2)/8-t*ε) * (∫ξ. exp (t * (∑i<j. V i ξ))∂PiM {..<j} M)"
by (simp_all add:exp_add[symmetric] field_simps)
also have "...=exp (t⇧2*(∑i=j..<n. (c i)⇧2)/8-t*ε) * (∫ξ. exp (t * (∑i<j. V i ξ))∂PiM {..<j} M)"
using a by (intro arg_cong2[where f="(*)"] arg_cong[where f="exp"] refl arg_cong2
[where f="(-)"] arg_cong2[where f="(/)"] sum.cong) auto
finally show "?L2≤exp(t⇧2*(∑i=j..<n. (c i)⇧2)/8-t*ε)*(∫ξ. exp (t*(∑i<j. V i ξ))∂PiM {..<j} M)"
by simp
qed
also have "... = exp(t^2 * (∑i<n. c i^2)/8-t*ε)" by (simp add:PiM_empty atLeast0LessThan)
also have "... = exp(t * ((t * (∑i<n. c i^2)/8)-ε))" by (simp add:algebra_simps power2_eq_square)
also have "... = exp(t * (-ε/2))" using sum_c_ge_0 by (auto simp add:divide_simps t_def)
also have "... = ?R" unfolding t_def by (simp add:field_simps power2_eq_square)
finally show ?thesis by simp
qed
theorem mc_diarmid_inequality_distr:
fixes f :: "('i ⇒ 'a) ⇒ real"
assumes "finite I"
assumes "⋀i. i ∈ I ⟹ prob_space (M i)"
assumes "⋀i x y. i ∈ I ⟹ {x,y} ⊆ space (PiM I M) ⟹ (∀j∈I-{i}. x j=y j) ⟹ ¦f x-f y¦≤c i"
assumes f_meas: "f ∈ borel_measurable (PiM I M)" and ε_gt_0: "ε > 0"
shows "𝒫(ω in PiM I M. f ω - (∫ξ. f ξ ∂PiM I M) ≥ ε) ≤ exp (-(2*ε^2)/(∑i∈I. (c i)^2))"
(is "?L ≤ ?R")
proof -
define n where "n = card I"
let ?q = "from_nat_into I"
let ?r = "to_nat_on I"
let ?f = "(λξ. f (λi∈I. ξ (?r i)))"
have q: "bij_betw ?q {..<n} I" unfolding n_def by (intro bij_betw_from_nat_into_finite assms(1))
have r: "bij_betw ?r I {..<n}" unfolding n_def by (intro to_nat_on_finite assms(1))
have [simp]: "?q (?r x) = x" if "x ∈ I" for x
by (intro from_nat_into_to_nat_on that countable_finite assms(1))
have [simp]: "?r (?q x) = x" if "x < n" for x
using bij_betw_imp_surj_on[OF r] that by (intro to_nat_on_from_nat_into) auto
have a: "⋀i. i ∈ {..<n} ⟹ prob_space ((M ∘ ?q) i)"
unfolding comp_def by (intro assms(2) bij_betw_apply[OF q])
have b:"PiM I M = PiM I (λi. (M ∘ ?q) (?r i))" by (intro PiM_cong) (simp_all add:comp_def)
also have "... = distr (PiM {..<n} (M ∘ ?q)) (PiM I (λi. (M ∘ ?q) (?r i))) (λω. λn∈I. ω (?r n))"
using r unfolding bij_betw_def by (intro distr_PiM_reindex[symmetric] a) auto
finally have c: "PiM I M = distr (PiM{..<n}(M∘?q)) (PiM I (λi.(M∘?q)(?r i))) (λω. λn∈I. ω (?r n))"
by simp
have d: "(λn∈I. x (?r n)) ∈ space (Pi⇩M I M)" if 4:"x ∈ space (Pi⇩M {..<n} (M ∘ ?q))" for x
proof -
have "x (?r i) ∈ space (M i)" if "i ∈ I" for i
proof -
have "?r i ∈ {..<n}" using bij_betw_apply[OF r] that by simp
hence "x (?r i) ∈ space ((M ∘ ?q) (?r i))" using that 4 PiE_mem unfolding space_PiM by blast
thus ?thesis using that unfolding comp_def by simp
qed
thus ?thesis unfolding space_PiM PiE_def by auto
qed
have "?L = 𝒫(ω in PiM {..<n} (M ∘ ?q). ?f ω - (∫ξ. f ξ ∂PiM I M) ≥ ε)"
proof (subst c, subst measure_distr, goal_cases)
case 1 thus ?case
by (intro measurable_restrict measurable_component_singleton bij_betw_apply[OF r])
next
case 2 thus ?case unfolding b[symmetric] by (intro measurable_sets_Collect[OF f_meas]) auto
next
case 3 thus ?case using d by (intro arg_cong2[where f="measure"] refl) (auto simp:vimage_def)
qed
also have "... = 𝒫(ω in PiM {..<n} (M ∘ ?q). ?f ω - (∫ξ. ?f ξ ∂PiM {..<n} (M ∘ ?q)) ≥ ε)"
proof (subst c, subst integral_distr, goal_cases)
case (1 ω) thus ?case
by (intro measurable_restrict measurable_component_singleton bij_betw_apply[OF r])
next
case (2 ω) thus ?case unfolding b[symmetric] by (rule f_meas)
next
case 3 thus ?case by simp
qed
also have "... ≤ exp (-(2*ε^2)/(∑i<n. (c (?q i))^2))"
proof (intro mc_diarmid_inequality_aux ε_gt_0, goal_cases)
case (1 i) thus ?case by (intro a) auto
next
case (2 i x y)
have "x (?r j) = y (?r j)" if "j ∈ I - {?q i}" for j
proof -
have "?r j ∈ {..<n} - {i}" using that bij_betw_apply[OF r] by auto
thus ?thesis using 2 by simp
qed
hence "∀j∈I - {?q i}. (λi∈I. x (?r i)) j = (λi∈I. y (?r i)) j" by auto
thus ?case using 2 d by (intro assms(3) bij_betw_apply[OF q]) auto
next
case 3
have "(λx. x (?r i)) ∈ Pi⇩M {..<n} (M ∘ ?q) →⇩M M i" if "i ∈ I" for i
proof -
have 0:"M i = (M ∘ ?q) (?r i)" using that by (simp add: comp_def)
show ?thesis unfolding 0 by (intro measurable_component_singleton bij_betw_apply[OF r] that)
qed
thus ?case by (intro measurable_compose[OF _ f_meas] measurable_restrict)
qed
also have "... = ?R" by (subst sum.reindex_bij_betw[OF q]) simp
finally show ?thesis by simp
qed
lemma (in prob_space) mc_diarmid_inequality_classic:
fixes f :: "('i ⇒ 'a) ⇒ real"
assumes "finite I"
assumes "indep_vars N X I"
assumes "⋀i x y. i ∈ I ⟹ {x,y} ⊆ space (PiM I N) ⟹ (∀j∈I-{i}. x j=y j) ⟹ ¦f x-f y¦≤c i"
assumes f_meas: "f ∈ borel_measurable (PiM I N)" and ε_gt_0: "ε > 0"
shows "𝒫(ω in M. f (λi∈I. X i ω) - (∫ξ. f (λi∈I. X i ξ) ∂M) ≥ ε) ≤ exp (-(2*ε^2)/(∑i∈I. (c i)^2))"
(is "?L ≤ ?R")
proof -
note indep_imp = iffD1[OF indep_vars_iff_distr_eq_PiM'']
let ?O = "λi. distr M (N i) (X i)"
have a:"distr M (Pi⇩M I N) (λx. λi∈I. X i x) = Pi⇩M I ?O"
using assms(2) unfolding indep_vars_def by (intro indep_imp[OF _ assms(2)]) auto
have b: "space (PiM I ?O) = space (PiM I N)"
by (metis (no_types, lifting) a space_distr)
have "(λi∈I. X i ω) ∈ space (Pi⇩M I N)" if "ω ∈ space M" for ω
using assms(2) that unfolding indep_vars_def measurable_def space_PiM by auto
hence "?L = 𝒫(ω in M. (λi∈I. X i ω)∈ space (Pi⇩M I N)∧ f (λi∈I. X i ω)-(∫ξ. f (λi∈I. X i ξ) ∂M)≥ε)"
by (intro arg_cong2[where f="measure"] Collect_restr_cong refl) auto
also have "... = 𝒫(ω in distr M (Pi⇩M I N) (λx. λi∈I. X i x). f ω - (∫ξ. f (λi∈I. X i ξ) ∂M) ≥ ε)"
proof (subst measure_distr, goal_cases)
case 1 thus ?case using assms(2) unfolding indep_vars_def by (intro measurable_restrict) auto
next
case 2 thus ?case unfolding space_distr by (intro measurable_sets_Collect[OF f_meas]) auto
next
case 3 thus ?case by (simp_all add:Int_def conj_commute)
qed
also have "... = 𝒫(ω in PiM I ?O. f ω - (∫ξ. f (λi∈I. X i ξ) ∂M) ≥ ε)"
unfolding a by simp
also have "... = 𝒫(ω in PiM I ?O. f ω - (∫ξ. f ξ ∂ distr M (Pi⇩M I N) (λx. λi∈I. X i x)) ≥ ε)"
proof (subst integral_distr[OF _ f_meas], goal_cases)
case (1 ω) thus ?case using assms(2) unfolding indep_vars_def by (intro measurable_restrict)auto
next
case 2 thus ?case by simp
qed
also have "... = 𝒫(ω in PiM I ?O. f ω - (∫ξ. f ξ ∂ Pi⇩M I ?O) ≥ ε)" unfolding a by simp
also have "... ≤ ?R"
using f_meas assms(2) b unfolding indep_vars_def
by (intro mc_diarmid_inequality_distr prob_space_distr assms(1) ε_gt_0 assms(3)) auto
finally show ?thesis by simp
qed
end