Theory Distributed_Distinct_Elements_Preliminary

section ‹Preliminary Results›

text ‹This section contains various short preliminary results used in the sections below.›

theory Distributed_Distinct_Elements_Preliminary
  imports
    Frequency_Moments.Frequency_Moments_Preliminary_Results
    Frequency_Moments.Product_PMF_Ext
    Median_Method.Median
    Expander_Graphs.Extra_Congruence_Method
    Expander_Graphs.Constructive_Chernoff_Bound
    Frequency_Moments.Landau_Ext
    Stirling_Formula.Stirling_Formula
begin

unbundle intro_cong_syntax

text ‹Simplified versions of measure theoretic results for pmfs:›

lemma measure_pmf_cong:
  assumes "⋀x. x ∈ set_pmf p ⟹ x ∈ P ⟷ x ∈ Q"
  shows "measure (measure_pmf p) P = measure (measure_pmf p)  Q"
  using assms
  by (intro finite_measure.finite_measure_eq_AE AE_pmfI) auto

lemma pmf_mono:
  assumes "⋀x. x ∈ set_pmf p ⟹ x ∈ P ⟹ x ∈ Q"
  shows "measure (measure_pmf p) P ≤ measure (measure_pmf p) Q"
proof -
  have "measure (measure_pmf p) P = measure (measure_pmf p) (P ∩ (set_pmf p))"
    by (intro measure_pmf_cong) auto
  also have "... ≤ measure (measure_pmf p) Q"
    using assms by (intro finite_measure.finite_measure_mono) auto
  finally show ?thesis by simp
qed

lemma pmf_rev_mono:
  assumes "⋀x. x ∈ set_pmf p ⟹ x ∉ Q ⟹ x ∉ P"
  shows "measure p P ≤ measure p Q"
  using assms by (intro pmf_mono) blast

lemma pmf_exp_mono:
  fixes f g :: "'a ⇒ real"
  assumes "integrable (measure_pmf p) f" "integrable (measure_pmf p) g"
  assumes "⋀x. x ∈ set_pmf p ⟹ f x ≤ g x"
  shows "integral⇧L (measure_pmf p) f ≤ integral⇧L (measure_pmf p) g"
  using assms  by (intro integral_mono_AE AE_pmfI) auto

lemma pmf_markov:
  assumes "integrable (measure_pmf p) f" "c > 0"
  assumes "⋀x. x ∈ set_pmf p ⟹ f x ≥ 0"
  shows "measure p {ω. f ω ≥ c} ≤ (∫ω. f ω ∂p)/ c" (is "?L ≤ ?R")
proof -
  have a:"AE ω in (measure_pmf p). 0 ≤ f ω"
    by (intro AE_pmfI assms(3))
  have b:"{} ∈ measure_pmf.events p"
    unfolding assms(1) by simp

  have "?L = 𝒫(ω in (measure_pmf p). f ω ≥ c)"
    using assms(1) by simp
  also have "... ≤  ?R"
    by (intro  integral_Markov_inequality_measure[OF _ b] assms a)
  finally show ?thesis by simp
qed

lemma pmf_add:
  assumes  "⋀x. x ∈ P ⟹ x ∈ set_pmf p ⟹ x ∈ Q ∨ x ∈ R"
  shows "measure p P ≤ measure p Q + measure p R"
proof -
  have "measure p P ≤ measure p (Q ∪ R)"
    using assms by (intro pmf_mono) blast
  also have "... ≤ measure p Q + measure p R"
    by (rule measure_subadditive, auto)
  finally show ?thesis by simp
qed

lemma pair_pmf_prob_left:
  "measure_pmf.prob (pair_pmf A B) {ω. P (fst ω)} = measure_pmf.prob A {ω. P ω}" (is "?L = ?R")
proof -
  have "?L = measure_pmf.prob (map_pmf fst (pair_pmf A B)) {ω. P ω}"
    by (subst measure_map_pmf) simp
  also have "... = ?R"
    by (subst map_fst_pair_pmf) simp
  finally show ?thesis by simp
qed

lemma pmf_exp_of_fin_function:
  assumes "finite A" "g ` set_pmf p ⊆ A"
  shows "(∫ω. f (g ω) ∂p) = (∑y ∈ A. f y * measure p {ω. g ω = y})"
    (is "?L = ?R")
proof -
  have "?L = integral⇧L (map_pmf g p) f"
    using integral_map_pmf assms by simp
  also have "... = (∑a∈A. f a * pmf (map_pmf g p) a)"
    using assms
    by (intro integral_measure_pmf_real) auto
  also have " ... = (∑y ∈ A. f y * measure p (g -` {y}))"
    unfolding assms(1) by (intro_cong "[σ⇩2 (*)]" more:sum.cong pmf_map)
  also have "... = ?R"
    by (intro sum.cong) (auto simp add: vimage_def)
  finally show ?thesis by simp
qed

text ‹Cardinality rules for distinct/ordered pairs of a set without the finiteness constraint - to
use in simplification:›

lemma card_distinct_pairs:
  "card {x ∈ B × B. fst x ≠ snd x} = card B^2 - card B" (is "card ?L = ?R")
proof (cases "finite B")
  case True
  include intro_cong_syntax
  have "card ?L = card (B × B - (λx. (x,x)) ` B)"
    by (intro arg_cong[where f="card"]) auto
  also have "... = card (B × B) - card ((λx. (x,x)) ` B)"
    by (intro card_Diff_subset finite_imageI True image_subsetI) auto
  also have "... = ?R"
    using True by (intro_cong "[σ⇩2 (-)]" more: card_image)
      (auto simp add:power2_eq_square inj_on_def)
  finally show ?thesis by simp
next
  case False
  then obtain p where p_in: "p ∈ B" by fastforce
  have "False" if "finite ?L"
  proof -
    have "(λx. (p,x)) ` (B - {p}) ⊆ ?L"
      using p_in by (intro image_subsetI) auto
    hence "finite ((λx. (p,x)) ` (B - {p}))"
      using finite_subset that by auto
    hence "finite (B - {p})"
      by (rule finite_imageD) (simp add:inj_on_def)
    hence "finite B"
      by simp
    thus "False" using False by simp
  qed
  hence "infinite ?L" by auto
  hence "card ?L = 0" by simp
  also have "... = ?R"
    using False by simp
  finally show ?thesis by simp
qed

lemma card_ordered_pairs':
  fixes M :: "('a ::linorder) set"
  shows "card {(x,y) ∈ M × M. x < y} = card M * (card M - 1) / 2"
proof (cases "finite M")
  case True
  show ?thesis using card_ordered_pairs[OF True] by linarith
next
  case False
  then obtain p where p_in: "p ∈ M" by fastforce
  let ?f= "(λx. if x < p then (x,p) else (p,x))"
  have "False" if "finite {(x,y) ∈ M × M. x < y}" (is "finite ?X")
  proof -
    have "?f ` (M-{p}) ⊆ ?X"
      using p_in by (intro image_subsetI) auto
    hence "finite (?f ` (M-{p}))" using that finite_subset by auto
    moreover have "inj_on ?f (M-{p})"
      by (intro inj_onI) (metis Pair_inject)
    ultimately have "finite (M - {p})"
      using finite_imageD by blast
    hence "finite M"
      using finite_insert[where a="p" and A="M-{p}"] by simp
    thus "False" using False by simp
  qed
  hence "infinite ?X" by auto
  then show ?thesis using False by simp
qed

text ‹The following are versions of the mean value theorem, where the interval endpoints may be
reversed.›

lemma MVT_symmetric:
  assumes "⋀x. ⟦min a b ≤ x; x ≤ max a b⟧ ⟹ DERIV f x :> f' x"
  shows "∃z::real. min a b ≤ z ∧ z ≤ max a b ∧ (f b - f a = (b - a) * f' z)"
proof -
  consider (a) "a < b" | (b) "a = b" | (c) "a > b"
    by argo
  then show ?thesis
  proof (cases)
    case a
    then obtain z :: real where r: "a < z" "z < b" "f b - f a = (b - a) * f' z"
      using assms MVT2[where a="a" and b="b" and f="f" and f'="f'"] by auto
    have "a ≤ z" "z ≤ b" using r(1,2) by auto
    thus ?thesis using a r(3) by auto
  next
    case b
    then show ?thesis by auto
  next
    case c
    then obtain z :: real where r: "b < z" "z < a" "f a - f b = (a - b) * f' z"
      using assms MVT2[where a="b" and b="a" and f="f" and f'="f'"] by auto
    have "f b - f a = (b-a) * f' z" using r by argo
    moreover have "b ≤ z" "z ≤ a" using r(1,2) by auto
    ultimately show ?thesis using c by auto
  qed
qed

lemma MVT_interval:
  fixes I :: "real set"
  assumes "interval I" "a ∈ I" "b ∈ I"
  assumes "⋀x. x ∈ I ⟹ DERIV f x :> f' x"
  shows "∃z. z ∈ I ∧ (f b - f a = (b - a) * f' z)"
proof -
  have a:"min a b ∈ I"
    using assms(2,3) by (cases "a < b") auto
  have b:"max a b ∈ I"
    using assms(2,3) by (cases "a < b") auto
  have c:"x ∈ {min a b..max a b} ⟹ x ∈ I" for x
    using interval_def assms(1) a b by auto
  have "⟦min a b ≤ x; x ≤ max a b⟧ ⟹ DERIV f x :> f' x" for x
    using c assms(4) by auto
  then obtain z where z:"z ≥ min a b" "z ≤ max a b" "f b - f a = (b-a) * f' z"
    using MVT_symmetric by blast
  have "z ∈ I"
    using c z(1,2) by auto
  thus ?thesis using z(3) by auto
qed

text ‹Ln is monotone on the positive numbers and thus commutes with min and max:›
lemma ln_min_swap:
  "x > (0::real) ⟹ (y > 0) ⟹ ln (min x y) = min (ln x) (ln y)"
  using ln_less_cancel_iff by fastforce

lemma ln_max_swap:
  "x > (0::real) ⟹ (y > 0) ⟹ ln (max x y) = max (ln x) (ln y)"
  using ln_le_cancel_iff by fastforce

text ‹Loose lower bounds for the factorial fuction:.›

lemma fact_lower_bound:
  "sqrt(2*pi*n)*(n/exp(1))^n ≤ fact n" (is "?L ≤ ?R")
proof (cases "n > 0")
  case True
  have "ln ?L = ln (2*pi*n)/2 + n * ln n - n"
    using True by (simp add: ln_mult ln_sqrt ln_realpow ln_div algebra_simps)
  also have "... ≤ ln ?R"
    by (intro Stirling_Formula.ln_fact_bounds True)
  finally show ?thesis
    using iffD1[OF ln_le_cancel_iff] True by simp
next
  case False
  then show ?thesis by simp
qed

lemma fact_lower_bound_1:
  assumes "n > 0"
  shows "(n/exp 1)^n ≤ fact n" (is "?L ≤ ?R")
proof -
  have "2 * pi ≥ 1" using pi_ge_two by auto
  moreover have "n ≥ 1" using assms by simp
  ultimately have "2 * pi * n ≥ 1*1"
    by (intro mult_mono) auto
  hence a:"2 * pi * n ≥ 1" by simp

  have "?L = 1 * ?L" by simp
  also have "... ≤ sqrt(2 * pi * n) * ?L"
    using a by (intro mult_right_mono) auto
  also have "... ≤ ?R"
    using fact_lower_bound by simp
  finally show ?thesis by simp
qed

text ‹Rules to handle O-notation with multiple variables, where some filters may be towards zero:›

lemma real_inv_at_right_0_inf:
  "∀⇩F x in at_right (0::real). c ≤ 1 / x"
proof -
  have "c ≤ 1 /  x" if b:" x ∈ {0<..<1 / (max c 1)}" for x
  proof -
    have "c * x ≤ (max c 1) * x"
      using b by (intro mult_right_mono, linarith, auto)
    also have "... ≤ (max c 1)  * (1 / (max c 1))"
      using b by (intro mult_left_mono) auto
    also have "... ≤ 1"
      by (simp add:of_rat_divide)
    finally have "c * x ≤ 1" by simp
    moreover have "0 < x"
      using b by simp
    ultimately show ?thesis by (subst pos_le_divide_eq, auto)
  qed
  thus ?thesis
    by (intro eventually_at_rightI[where b="1/(max c 1)"], simp_all)
qed

lemma bigo_prod_1:
  assumes "(λx. f x) ∈ O[F](λx. g x)" "G ≠ bot"
  shows "(λx. f (fst x)) ∈ O[F ×⇩F G](λx. g (fst x))"
proof -
  obtain c where a: "∀⇩F x in F. norm (f x) ≤ c * norm (g x)" and c_gt_0: "c > 0"
    using assms unfolding bigo_def by auto

  have "∃c>0. ∀⇩F x in F ×⇩F G. norm (f (fst x)) ≤ c * norm (g (fst x))"
    by (intro exI[where x="c"] conjI c_gt_0  eventually_prod1' a assms(2))
  thus ?thesis
    unfolding bigo_def by simp
qed

lemma bigo_prod_2:
  assumes "(λx. f x) ∈ O[G](λx. g x)" "F ≠ bot"
  shows "(λx. f (snd x)) ∈ O[F ×⇩F G](λx. g (snd x))"
proof -
  obtain c where a: "∀⇩F x in G. norm (f x) ≤ c * norm (g x)" and c_gt_0: "c > 0"
    using assms unfolding bigo_def by auto

  have "∃c>0. ∀⇩F x in F ×⇩F G. norm (f (snd x)) ≤ c * norm (g (snd x))"
    by (intro exI[where x="c"] conjI c_gt_0  eventually_prod2' a assms(2))
  thus ?thesis
    unfolding bigo_def by simp
qed

lemma eventually_inv:
  fixes P :: "real ⇒ bool"
  assumes "eventually (λx. P (1/x)) at_top "
  shows "eventually (λx. P x) (at_right 0)"
proof -
  obtain N where c:"n ≥ N ⟹ P (1/n)" for n
    using assms unfolding eventually_at_top_linorder by auto

  define q where "q = max 1 N"
  have d: "0 < 1 / q" "q > 0"
    unfolding q_def by auto

  have "P x" if "x ∈ {0<..<1 / q}" for x
  proof -
    define n where "n = 1/x"
    have x_eq: "x = 1 / n"
      unfolding n_def using that by simp

    have "N ≤ q" unfolding q_def by simp
    also have "... ≤ n"
      unfolding n_def using that d by (simp add:divide_simps ac_simps)
    finally have "N ≤ n" by simp
    thus ?thesis
      unfolding x_eq by (intro c)
  qed

  thus ?thesis
    by (intro eventually_at_rightI[where b="1/q"] d)
qed

lemma bigo_inv:
  fixes f g :: "real ⇒ real"
  assumes "(λx. f (1/x)) ∈ O(λx. g (1/x))"
  shows "f ∈ O[at_right 0](g)"
  using assms eventually_inv unfolding bigo_def by auto

unbundle no_intro_cong_syntax

end