Theory 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 iI. M' i) (λx. λiI. X i x) = (ΠM iI. 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 iI. M' i) (λx. λiI. 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 iI. distr M (M' i) (X i))"
    unfolding True PiM_empty by simp
  finally have "distr M (ΠM iI. M' i) (λx. λiI. X i x)=(ΠM iI. 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 (PiM I M) (PiM I M) (λx. restrict x I) = PiM I M"
    by (intro distr_PiM_reindex assms) auto
  also have "... =  PiM I (λi. distr (PiM I M) (M i) (λω. ω i))"
    by (intro PiM_cong refl distr_PiM_component[symmetric] assms)
  finally have
    "distr (PiM I M) (PiM I M) (λx. restrict x I) = PiM I (λi. distr (PiM 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  PiE 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. (λiI. Y' i x) = (λiI. 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 (PiM I M') (λx. λiI. Y' i x) = distr M (PiM I M') (λx. λiI. X' i x)"
    by (intro distr_cong_AE measurable_restrict a b assms(3)) auto
  also have "... =  PiM I (λi. distr M (M' i) (X' i))"
    using assms b by (subst indep_vars_iff_distr_eq_PiM''[symmetric]) auto
  also have "... =  PiM I (λi. distr M (M' i) (Y' i))"
    by (intro PiM_cong distr_cong_AE c assms(3) b) auto
  finally have "distr M (PiM I M') (λx. λiI. Y' i x) = PiM 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