Theory Prob_Space_Lemmas

section‹Auxiliary probability space results›

(*
  Session : Balog_Szemeredi_Gowers
  Title:   Prob_Space_Lemmas.thy
  Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
  Affiliation: University of Cambridge
  Date: August 2022.
*)

theory Prob_Space_Lemmas
  imports 
    Random_Graph_Subgraph_Threshold.Prob_Lemmas
begin

context prob_space

begin

lemma expectation_uniform_count:
  assumes "M = uniform_count_measure X" and "finite X"
  shows "expectation f = (∑ x ∈ X. f x) / card X"

proof-
  have "expectation f = (∑ x ∈ X. (1 / (card X)) * f x)" 
    using assms uniform_count_measure_def bot_nat_0.extremum of_nat_0 of_nat_le_iff real_scaleR_def
    lebesgue_integral_point_measure_finite[of _ "(λ x. 1 / card X)" "f"]
    scaleR_sum_right sum_distrib_left zero_le_divide_1_iff by metis
  then show ?thesis using sum_left_div_distrib by fastforce
qed

text ‹A lemma to obtain a value for x where the inequality is satisfied ›
lemma expectation_obtains_ge: 
  fixes f :: "'a ⇒ real"
  assumes "M = uniform_count_measure X" and "finite X"
  assumes "expectation f ≥ c"
  obtains x where "x ∈ X" and "f x ≥ c"

proof -
  have ne: "X ≠ {}"
    using assms(1) subprob_not_empty by auto 
  then have ne0: "card X > 0"
    by (simp add: assms(2) card_gt_0_iff) 
  have "∃ x ∈ X . f x ≥ c"
  proof (rule ccontr)
    assume "¬ (∃x∈X. c ≤ f x)"
    then have "∀x∈X. c > f x" by auto 
    then have "(∑ x ∈ X. f x) < (∑ x ∈ X. c)"
      by (meson assms(2) ne sum_strict_mono) 
    then have lt: "(∑ x ∈ X. f x) < (card X) * c" by simp 
    have "expectation f = (∑ x ∈ X. f x) / card X" using expectation_uniform_count assms by auto
    then have "(∑ x ∈ X. f x) ≥ (card X) * c" using ne0 assms
      by (simp add: le_divide_eq mult_of_nat_commute)
    then show False using lt by auto
  qed
  then show ?thesis using that by auto
qed

text ‹The following is the variation on the Cauchy-Schwarz inequality presented in Gowers's notes 
before Lemma 2.13 \cite{Gowersnotes}.›

lemma cauchy_schwarz_ineq_var:
  fixes X :: "'a ⇒ real"
  assumes "integrable M (λx. (X x)^2)" and "X ∈ borel_measurable M"
  shows "expectation (λ x. (X x)^2) ≥ (expectation (λ x . (X x)))^2"

proof -
  have "expectation (λ x. (X x)^2) - (expectation (λ x . (X x)))^2 = expectation (λx. (X x - expectation X)^2)"
    using variance_expectation assms(1) assms(2) by presburger 
  then have "expectation (λ x. (X x)^2) - (expectation (λ x . (X x)))^2 ≥ 0" by simp
  thus ?thesis by simp 
qed

lemma integrable_uniform_count_measure_finite: 
  fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}" 
  shows "finite A ⟹ integrable (uniform_count_measure A) g"
  unfolding uniform_count_measure_def by (simp add: integrable_point_measure_finite)

lemma cauchy_schwarz_ineq_var_uniform:
  fixes X :: "'a ⇒ real"
  assumes "M = uniform_count_measure S"
  assumes "finite S"
  shows "expectation (λ x. (X x)^2) ≥ (expectation (λ x . (X x)))^2"

proof -
  have borel: "X ∈ borel_measurable M" using assms by (simp) 
  have "integrable M X" using assms by (simp add: integrable_uniform_count_measure_finite)
  then have "integrable M (λ x. (X x)^2)" using assms by (simp add: integrable_uniform_count_measure_finite)
  thus ?thesis using cauchy_schwarz_ineq_var borel by simp 
qed

text ‹An equation for expectation over a discrete random variables distribution: ›

lemma expectation_finite_uniform_space: 
  assumes "M = uniform_count_measure S" and "finite S"
  fixes X :: "'a ⇒ real"
  shows "expectation X = (∑ y ∈ X ` S . prob {x ∈ S . X x = y} * y)"

proof -
  have "Bochner_Integration.simple_bochner_integrable M X"
  proof (safe intro!: Bochner_Integration.simple_bochner_integrable.intros)
    show "simple_function M X" unfolding simple_function_def using assms 
      by (auto simp add: space_uniform_count_measure)
    show "emeasure M {y ∈ space M. X y ≠ 0} = ∞ ⟹ False"
      using emeasure_subprob_space_less_top by (auto)
  qed
  then have "expectation X = Bochner_Integration.simple_bochner_integral M X" 
    using simple_bochner_integrable_eq_integral by fastforce
  thus ?thesis using Bochner_Integration.simple_bochner_integral_def space_uniform_count_measure
    by (metis (no_types, lifting) Collect_cong assms(1) real_scaleR_def sum.cong) 
qed

lemma expectation_finite_uniform_indicator: 
  assumes "M = uniform_count_measure S" and "finite S"
  shows "expectation (λ x. indicator (T x) y) = prob {x ∈ S . indicator (T x) y = 1}" (is "expectation ?X = _")

proof -
  have ss: "?X ` S ⊆ {0, 1}"  
    by (intro subsetI, auto simp add: indicator_eq_1_iff)
  have diff: "⋀ y'. y' ∈ ({0, 1} - ?X ` S) ⟹ prob {x ∈ S . ?X x = y'} = 0"
    by (metis (mono_tags, lifting) DiffD2 empty_Collect_eq image_eqI measure_empty)
  have "expectation ?X = (∑ y ∈ ?X ` S . prob {x ∈ S . ?X x = y} * y)" 
    using expectation_finite_uniform_space assms by auto
  also have "... = (∑ y ∈ ?X ` S . prob {x ∈ S . ?X x = y} * y) + 
    (∑ y ∈ ({0, 1} - ?X ` S) . prob {x ∈ S . ?X x = y} * y)"
    using diff by auto
  also have "... = (∑ y ∈ {0, 1} . prob {x ∈ S . ?X x = y} * y)"
    using sum.subset_diff[of "?X ` S" "{0, 1}" "λ y. prob {x ∈ S . ?X x = y} * y"] ss by fastforce 
  also have "... = prob {x ∈ S . ?X x = 0} * 0 + prob {x ∈ S. ?X x = 1} * 1" by auto
  finally have "expectation ?X = prob {x ∈ S. ?X x = 1}*1" by auto
  thus ?thesis by (smt (verit) Collect_cong indicator_eq_1_iff) 
qed

end
end