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