# Theory Concentration_Inequalities.Concentration_Inequalities_Preliminary

```section ‹Preliminary results›

theory Concentration_Inequalities_Preliminary
imports Lp.Lp
begin

text ‹Version of Cauchy-Schwartz for the Lebesgue integral:›
lemma cauchy_schwartz:
fixes f g :: "_ ⇒ real"
assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M"
assumes "integrable M (λx. (f x) ^2)" "integrable M (λx. (g x) ^2)"
shows "integrable M (λx. f x * g x)" (is "?A")
"(∫x. f x * g x ∂M) ≤ (∫x. (f x)^2 ∂M) powr (1/2) * (∫x. (g x)^ 2 ∂M) powr (1/2)"
(is "?L ≤ ?R")
proof -
show 0:"?A"
using assms by (intro Holder_inequality(1)[where p="2" and q="2"]) auto

have "?L ≤ (∫x. ¦f x * g x¦ ∂M)"
using 0 by (intro integral_mono) auto
also have "... ≤ (∫x. ¦f x¦ powr 2 ∂M) powr (1/2) * (∫x. ¦g x¦ powr 2 ∂M) powr (1/2)"
using assms by (intro Holder_inequality(2)) auto
also have "... = ?R" by simp
finally show "?L ≤ ?R" by simp
qed

text ‹Generalization of @{thm [source] prob_space.indep_vars_iff_distr_eq_PiM'}:›

lemma (in prob_space) indep_vars_iff_distr_eq_PiM'':
fixes I :: "'i set" and X :: "'i ⇒ 'a ⇒ 'b"
assumes rv: "⋀i. i ∈ I ⟹ random_variable (M' i) (X i)"
shows "indep_vars M' X I ⟷
distr M (Π⇩M i∈I. M' i) (λx. λi∈I. X i x) = (Π⇩M i∈I. distr M (M' i) (X i))"
proof (cases "I = {}")
case True
have 0: " indicator A (λ_. undefined) = emeasure (count_space {λ_. undefined}) A" (is "?L = ?R")
if "A ⊆ {λ_. undefined}" for A :: "('i ⇒ 'b) set"
proof -
have 1:"A ≠ {} ⟹ A = {λ_. undefined}"
using that by auto

have "?R = of_nat (card A)"
using finite_subset that by (intro emeasure_count_space_finite that) auto
also have "... = ?L"
using 1 by (cases "A = {}") auto
finally show ?thesis by simp
qed

have "distr M (Π⇩M i∈I. M' i) (λx. λi∈I. X i x) =
distr M (count_space {λ_. undefined}) (λ_. (λ_. undefined))"
unfolding True PiM_empty by (intro distr_cong) (auto simp:restrict_def)
also have "... = return (count_space {λ_. undefined}) (λ_. undefined)"
by (intro distr_const) auto
also have "... = count_space ({λ_. undefined} :: ('i ⇒ 'b) set) "
by (intro measure_eqI) (auto simp:0)
also have "... = (Π⇩M i∈I. distr M (M' i) (X i))"
unfolding True PiM_empty by simp
finally have "distr M (Π⇩M i∈I. M' i) (λx. λi∈I. X i x)=(Π⇩M i∈I. distr M (M' i) (X i)) ⟷ True"
by simp
also have "... ⟷ indep_vars M' X I"
finally show ?thesis by simp
next
case False
thus ?thesis
by (intro indep_vars_iff_distr_eq_PiM' assms) auto
qed

lemma proj_indep:
assumes "⋀i. i ∈ I ⟹ prob_space (M i)"
shows "prob_space.indep_vars (PiM I M) M (λi ω. ω i) I"
proof -
interpret prob_space "(PiM I M)"
by (intro prob_space_PiM assms)

have "distr (Pi⇩M I M) (Pi⇩M I M) (λx. restrict x I) = PiM I M"
by (intro distr_PiM_reindex assms) auto
also have "... =  Pi⇩M I (λi. distr (Pi⇩M I M) (M i) (λω. ω i))"
by (intro PiM_cong refl distr_PiM_component[symmetric] assms)
finally have
"distr (Pi⇩M I M) (Pi⇩M I M) (λx. restrict x I) = Pi⇩M I (λi. distr (Pi⇩M I M) (M i) (λω. ω i))"
by simp
thus "indep_vars M (λi ω. ω i) I"
by (intro iffD2[OF indep_vars_iff_distr_eq_PiM'']) simp_all
qed

lemma forall_Pi_to_PiE:
assumes "⋀x. P x = P (restrict x I)"
shows "(∀x ∈ Pi I A. P x) = (∀x ∈ PiE I A. P x)"
using assms by (simp add:PiE_def Pi_def set_eq_iff, force)

lemma PiE_reindex:
assumes "inj_on f I"
shows "PiE I (A ∘ f) = (λa. restrict (a ∘ f) I) ` PiE (f ` I) A" (is "?lhs = ?g ` ?rhs")
proof -
have "?lhs ⊆ ?g` ?rhs"
proof (rule subsetI)
fix x
assume a:"x ∈ Pi⇩E I (A ∘ f)"
define y where y_def: "y = (λk. if k ∈ f ` I then x (the_inv_into I f k) else undefined)"
have b:"y ∈ PiE (f ` I) A"
using a assms the_inv_into_f_eq[OF assms]
by (simp add: y_def PiE_iff extensional_def)
have c: "x = (λa. restrict (a ∘ f) I) y"
using a assms the_inv_into_f_eq extensional_arb
by (intro ext, simp add:y_def PiE_iff, fastforce)
show "x ∈ ?g ` ?rhs" using b c by blast
qed
moreover have "?g ` ?rhs ⊆ ?lhs"
by (rule image_subsetI, simp add:Pi_def PiE_def)
ultimately show ?thesis by blast
qed

context prob_space
begin

lemma indep_sets_reindex:
assumes "inj_on f I"
shows "indep_sets A (f ` I) = indep_sets (λi. A (f i)) I"
proof -
have a: "⋀J g. J ⊆ I ⟹ (∏j ∈ f ` J. g j) = (∏j ∈ J. g (f j))"
by (metis assms prod.reindex_cong subset_inj_on)

have b:"J ⊆ I ⟹ (Π⇩E i ∈ J. A (f i)) = (λa. restrict (a ∘ f) J) ` PiE (f ` J) A" for J
using assms inj_on_subset
by (subst PiE_reindex[symmetric]) auto

have c:"⋀J. J ⊆ I ⟹ finite (f ` J) = finite J"
by (meson assms finite_image_iff inj_on_subset)

show ?thesis
qed

lemma indep_vars_reindex:
assumes "inj_on f I"
assumes "indep_vars M' X' (f ` I)"
shows "indep_vars (M' ∘ f) (λk ω. X' (f k) ω) I"
using assms by (simp add:indep_vars_def2 indep_sets_reindex)

lemma indep_vars_cong_AE:
assumes "AE x in M. (∀i ∈ I. X' i x = Y' i x)"
assumes "indep_vars M' X' I"
assumes "⋀i. i ∈ I ⟹ random_variable (M' i) (Y' i)"
shows "indep_vars M' Y' I"
proof -
have a: "AE x in M. (λi∈I. Y' i x) = (λi∈I. X' i x)"
by (rule AE_mp[OF assms(1)], rule AE_I2, simp cong:restrict_cong)
have b: "⋀i. i ∈ I ⟹ random_variable (M' i) (X' i)"
have c: "⋀x. x ∈ I ⟹ AE xa in M. X' x xa = Y' x xa"
by (rule AE_mp[OF assms(1)], rule AE_I2, simp)

have "distr M (Pi⇩M I M') (λx. λi∈I. Y' i x) = distr M (Pi⇩M I M') (λx. λi∈I. X' i x)"
by (intro distr_cong_AE measurable_restrict a b assms(3)) auto
also have "... =  Pi⇩M I (λi. distr M (M' i) (X' i))"
using assms b by (subst indep_vars_iff_distr_eq_PiM''[symmetric]) auto
also have "... =  Pi⇩M I (λi. distr M (M' i) (Y' i))"
by (intro PiM_cong distr_cong_AE c assms(3) b) auto
finally have "distr M (Pi⇩M I M') (λx. λi∈I. Y' i x) = Pi⇩M I (λi. distr M (M' i) (Y' i))"
by simp

thus ?thesis
using assms(3)
by (subst indep_vars_iff_distr_eq_PiM'') auto
qed

end

text ‹Integrability of bounded functions on finite measure spaces:›

lemma bounded_const: "bounded ((λx. (c::real)) ` T)"
by (intro boundedI[where B="norm c"]) auto

lemma bounded_exp:
fixes f :: "'a ⇒ real"
assumes "bounded ((λx. f x) ` T)"
shows "bounded ((λx. exp (f x)) ` T)"
proof -
obtain m where "norm (f x) ≤ m" if "x ∈ T" for x
using assms unfolding bounded_iff by auto

thus ?thesis
by (intro boundedI[where B="exp m"]) fastforce
qed

lemma bounded_mult_comp:
fixes f :: "'a ⇒ real"
assumes "bounded (f ` T)" "bounded (g ` T)"
shows "bounded ((λx. (f x) * (g x)) ` T)"
proof -
obtain m1 where "norm (f x) ≤ m1" "m1 ≥0" if "x ∈ T" for x
using assms unfolding bounded_iff by fastforce
moreover obtain m2 where "norm (g x) ≤ m2" "m2 ≥0" if "x ∈ T" for x
using assms unfolding bounded_iff by fastforce

ultimately show ?thesis
by (intro boundedI[where B="m1 * m2"]) (auto intro!: mult_mono simp:abs_mult)
qed

lemma bounded_sum:
fixes f :: "'i ⇒ 'a ⇒ real"
assumes "finite I"
assumes "⋀i. i ∈ I ⟹ bounded (f i ` T)"
shows "bounded ((λx. (∑i ∈ I. f i x)) ` T)"
using assms by (induction I) (auto intro:bounded_plus_comp bounded_const)

lemma bounded_pow:
fixes f :: "'a ⇒ real"
assumes "bounded ((λx. f x) ` T)"
shows "bounded ((λx. (f x)^n) ` T)"
proof -
obtain m where "norm (f x) ≤ m" if "x ∈ T" for x
using assms unfolding bounded_iff by auto
hence "norm ((f x)^n) ≤ m^n" if "x ∈ T" for x
using that unfolding norm_power by (intro power_mono) auto
thus ?thesis by (intro boundedI[where B="m^n"]) auto
qed

lemma bounded_sum_list:
fixes f :: "'i ⇒ 'a ⇒ real"
assumes "⋀y. y ∈ set ys ⟹ bounded (f y ` T)"
shows "bounded ((λx. (∑y ← ys. f y x)) ` T)"
using assms by (induction ys) (auto intro:bounded_plus_comp bounded_const)

lemma (in finite_measure) bounded_int:
fixes f :: "'i ⇒ 'a ⇒ real"
assumes "bounded ((λ x. f (fst x) (snd x)) ` (T × space M))"
shows "bounded ((λx. (∫ω. (f x ω) ∂M)) ` T)"
proof -
obtain m where "⋀x y. x ∈ T ⟹ y ∈ space M ⟹ norm (f x y) ≤ m"
using assms unfolding bounded_iff by auto
hence m:"⋀x y. x ∈ T ⟹ y ∈ space M ⟹ norm (f x y) ≤ max m 0"
by fastforce

have "norm (∫ω. (f x ω) ∂M) ≤ max m 0 * measure M (space M)" (is "?L ≤ ?R") if "x ∈ T" for x
proof -
have "?L ≤ (∫ω. norm (f x ω) ∂M)" by simp
also have "... ≤ (∫ω. max m 0 ∂M)"
using that m by (intro integral_mono') auto
also have "... = ?R"
by simp
finally show ?thesis by simp
qed
thus ?thesis
by (intro boundedI[where B="max m 0 * measure M (space M)"]) auto
qed

lemmas bounded_intros =
bounded_minus_comp bounded_plus_comp bounded_mult_comp bounded_sum finite_measure.bounded_int
bounded_const bounded_exp bounded_pow bounded_sum_list

lemma (in prob_space) integrable_bounded:
fixes f :: "_ ⇒ ('b :: {banach,second_countable_topology})"
assumes "bounded (f ` space M)"
assumes "f ∈ M →⇩M borel"
shows "integrable M f"
proof -
obtain m where "norm (f x) ≤ m" if "x ∈ space M" for x
using assms(1) unfolding bounded_iff by auto
thus ?thesis
by (intro integrable_const_bound[where B="m"] AE_I2 assms(2))
qed

lemma integrable_bounded_pmf:
fixes f :: "_ ⇒ ('b :: {banach,second_countable_topology})"
assumes "bounded (f ` set_pmf M)"
shows "integrable (measure_pmf M) f"
proof -
obtain m where "norm (f x) ≤ m" if "x ∈ set_pmf M" for x
using assms(1) unfolding bounded_iff by auto
thus ?thesis by (intro measure_pmf.integrable_const_bound[where B="m"] AE_pmfI) auto
qed

end```