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 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