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" unfolding indep_vars_def by (auto simp add: space_PiM indep_sets_def) (auto simp add:True) 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 by (simp add:indep_sets_def all_subset_image a c) (simp_all add:forall_Pi_to_PiE b) 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)" using assms(2) by (simp add:indep_vars_def2) 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