Theory Combinatorial_Q_Analogues.Q_Library

theory Q_Library
  imports "HOL-Analysis.Analysis" "HOL-Computational_Algebra.Computational_Algebra"
begin

subsection ‹Miscellanea›

(* simple generic stuff about finite products *)
lemma prod_uminus: "(∏x∈A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (∏x∈A. f x)"
  by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps)

lemma prod_diff_swap:
  fixes f :: "'a ⇒ 'b :: comm_ring_1"
  shows "prod (λx. f x - g x) A = (-1) ^ card A * prod (λx. g x - f x) A"
  using prod.distrib[of "λ_. -1" "λx. f x - g x" A] by simp

lemma prod_diff:
  fixes f :: "'a ⇒ 'b :: field"
  assumes "finite A" "B ⊆ A" "⋀x. x ∈ B ⟹ f x ≠ 0"
  shows   "prod f (A - B) = prod f A / prod f B"
proof -
  from assms have [intro, simp]: "finite B"
    using finite_subset by blast
  have "prod f A = prod f ((A - B) ∪ B)"
    using assms by (intro prod.cong) auto
  also have "… = prod f (A - B) * prod f B"
    using assms by (subst prod.union_disjoint) (auto intro: finite_subset)
  also have "… / prod f B = prod f (A - B)"
    using assms by simp
  finally show ?thesis ..
qed


lemma power_inject_exp':
  assumes "a ≠ 1" "a > (0 :: 'a :: linordered_semidom)"
  shows   "a ^ m = a ^ n ⟷ m = n"
proof (cases "a > 1")
  case True
  thus ?thesis by simp
next
  case False
  have "a ^ m > a ^ n" if "m < n" for m n
    by (rule power_strict_decreasing) (use that assms False in auto)
  from this[of m n] this[of n m] show ?thesis
    by (cases m n rule: linorder_cases) auto
qed

lemma q_power_neq_1:
  assumes "norm (q :: 'a :: real_normed_div_algebra) < 1" "n > 0"
  shows   "q ^ n ≠ 1"
proof (cases "q = 0")
  case False
  thus ?thesis
    using power_inject_exp'[of "norm q" n 0] assms
    by (auto simp flip: norm_power)
qed (use assms in ‹auto simp: power_0_left›)  


lemma fls_nth_sum: "fls_nth (∑x∈A. f x) n = (∑x∈A. fls_nth (f x) n)"
  by (induction A rule: infinite_finite_induct) auto

lemma one_plus_fls_X_powi_eq:
  "(1 + fls_X) powi n = fps_to_fls (fps_binomial (of_int n :: 'a :: field_char_0))"
proof (cases "n ≥ 0")
  case True
  thus ?thesis
    using fps_binomial_of_nat[of "nat n", where ?'a = 'a]
    by (simp add: power_int_def fps_to_fls_power)
next
  case False
  thus ?thesis
    using fps_binomial_minus_of_nat[of "nat (-n)", where ?'a = 'a]
    by (simp add: power_int_def fps_to_fls_power fps_inverse_power flip: fls_inverse_fps_to_fls)
qed



lemma bij_betw_imp_empty_iff: "bij_betw f A B ⟹ A = {} ⟷ B = {}"
  unfolding bij_betw_def by blast

lemma bij_betw_imp_Ex_iff: "bij_betw f {x. P x} {x. Q x} ⟹ (∃x. P x) ⟷ (∃x. Q x)"
  unfolding bij_betw_def by blast

lemma bij_betw_imp_Bex_iff: "bij_betw f {x∈A. P x} {x∈B. Q x} ⟹ (∃x∈A. P x) ⟷ (∃x∈B. Q x)"
  unfolding bij_betw_def by blast


(* TODO: needlessly weak version in library; should be replaced *)
lemmas [derivative_intros del] = Deriv.DERIV_power_int
lemma DERIV_power_int [derivative_intros]:
  assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)"
  and "n ≥ 0 ∨ f x ≠ 0"
  shows   "((λx. power_int (f x) n) has_field_derivative
             (of_int n * power_int (f x) (n - 1) * d)) (at x within s)"
proof (cases n rule: int_cases4)
  case (nonneg n)
  thus ?thesis 
    by (cases "n = 0"; cases "f x = 0")
       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff 
                     power_diff power_int_0_left_If)
next
  case (neg n)
  thus ?thesis using assms(2)
    by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
             simp flip: power_Suc power_Suc2 power_add)
qed


(* stuff about uniform limits, swapping limits, etc. *)
lemma uniform_limit_compose':
  assumes "uniform_limit B (λx y. f x y) (λy. f' y) F" "⋀y. y ∈ A ⟹ g y ∈ B"
  shows   "uniform_limit A (λx y. f x (g y)) (λy. f' (g y)) F"
proof -
  have "uniform_limit (g ` A) (λx y. f x y) (λy. f' y) F"
    using assms(1) by (rule uniform_limit_on_subset) (use assms(2) in blast)
  thus "uniform_limit A (λx y. f x (g y)) (λy. f' (g y)) F"
    unfolding uniform_limit_iff by auto
qed

lemma eventually_eventually_prod_filter1:
  assumes "eventually P (F ×⇩F G)"
  shows   "eventually (λx. eventually (λy. P (x, y)) G) F"
proof -
  from assms obtain Pf Pg where
    *: "eventually Pf F" "eventually Pg G" "⋀x y. Pf x ⟹ Pg y ⟹ P (x, y)"
    unfolding eventually_prod_filter by auto
  show ?thesis
    using *(1)
  proof eventually_elim
    case x: (elim x)
    show ?case
      using *(2) by eventually_elim (use x *(3) in auto)
  qed
qed

lemma eventually_eventually_prod_filter2:
  assumes "eventually P (F ×⇩F G)"
  shows   "eventually (λy. eventually (λx. P (x, y)) F) G"
proof -
  from assms obtain Pf Pg where
    *: "eventually Pf F" "eventually Pg G" "⋀x y. Pf x ⟹ Pg y ⟹ P (x, y)"
    unfolding eventually_prod_filter by auto
  show ?thesis
    using *(2)
  proof eventually_elim
    case y: (elim y)
    show ?case
      using *(1) by eventually_elim (use y *(3) in auto)
  qed
qed

(* TODO: this is more general than the version in the library *)
proposition swap_uniform_limit':
  assumes f: "∀⇩F n in F. (f n ⤏ g n) G"
  assumes g: "(g ⤏ l) F"
  assumes uc: "uniform_limit S f h F"
  assumes ev: "∀⇩F x in G. x ∈ S"
  assumes "¬trivial_limit F"
  shows "(h ⤏ l) G"
proof (rule tendstoI)
  fix e :: real
  define e' where "e' = e/3"
  assume "0 < e"
  then have "0 < e'" by (simp add: e'_def)
  from uniform_limitD[OF uc ‹0 < e'›]
  have "∀⇩F n in F. ∀x∈S. dist (h x) (f n x) < e'"
    by (simp add: dist_commute)
  moreover
  from f
  have "∀⇩F n in F. ∀⇩F x in G. dist (g n) (f n x) < e'"
    by eventually_elim (auto dest!: tendstoD[OF _ ‹0 < e'›] simp: dist_commute)
  moreover
  from tendstoD[OF g ‹0 < e'›] have "∀⇩F x in F. dist l (g x) < e'"
    by (simp add: dist_commute)
  ultimately
  have "∀⇩F _ in F. ∀⇩F x in G. dist (h x) l < e"
  proof eventually_elim
    case (elim n)
    note fh = elim(1)
    note gl = elim(3)
    show ?case
      using elim(2) ev
    proof eventually_elim
      case (elim x)
      from fh[rule_format, OF ‹x ∈ S›] elim(1)
      have "dist (h x) (g n) < e' + e'"
        by (rule dist_triangle_lt[OF add_strict_mono])
      from dist_triangle_lt[OF add_strict_mono, OF this gl]
      show ?case by (simp add: e'_def)
    qed
  qed
  thus "∀⇩F x in G. dist (h x) l < e"
    using eventually_happens by (metis ‹¬trivial_limit F›)
qed

(* TODO: reproved theorem in the library using the more general one above *)
proposition swap_uniform_limit:
  assumes f: "∀⇩F n in F. (f n ⤏ g n) (at x within S)"
  assumes g: "(g ⤏ l) F"
  assumes uc: "uniform_limit S f h F"
  assumes nt: "¬trivial_limit F"
  shows "(h ⤏ l) (at x within S)"
proof -
  have ev: "eventually (λx. x ∈ S) (at x within S)"
    using eventually_at_topological by blast
  show ?thesis
    by (rule swap_uniform_limit'[OF f g uc ev nt])
qed

text ‹
  Tannery's Theorem proves that, under certain boundedness conditions:
  \[ \lim_{x\to\bar x} \sum_{k=0}^\infty f(k,n) = \sum_{k=0}^\infty \lim_{x\to\bar x} f(k,n) \]
›
lemma tannerys_theorem:
  fixes a :: "nat ⇒ _ ⇒ 'a :: {real_normed_algebra, banach}"
  assumes limit: "⋀k. ((λn. a k n) ⤏ b k) F"
  assumes bound: "eventually (λ(k,n). norm (a k n) ≤ M k) (at_top ×⇩F F)"
  assumes "summable M"
  assumes [simp]: "F ≠ bot"
  shows   "eventually (λn. summable (λk. norm (a k n))) F ∧
           summable (λn. norm (b n)) ∧
           ((λn. suminf (λk. a k n)) ⤏ suminf b) F"
proof (intro conjI allI)
  show "eventually (λn. summable (λk. norm (a k n))) F"
  proof -
    have "eventually (λn. eventually (λk. norm (a k n) ≤ M k) at_top) F"
      using eventually_eventually_prod_filter2[OF bound] by simp
    thus ?thesis
    proof eventually_elim
      case (elim n)
      show "summable (λk. norm (a k n))"
      proof (rule summable_comparison_test_ev)
        show "eventually (λk. norm (norm (a k n)) ≤ M k) at_top"
          using elim by auto
      qed fact
    qed
  qed

  have bound': "eventually (λk. norm (b k) ≤ M k) at_top"
  proof -
    have "eventually (λk. eventually (λn. norm (a k n) ≤ M k) F) at_top"
      using eventually_eventually_prod_filter1[OF bound] by simp
    thus ?thesis
    proof eventually_elim
      case (elim k)
      show "norm (b k) ≤ M k"
      proof (rule tendsto_upperbound)
        show "((λn. norm (a k n)) ⤏ norm (b k)) F"
          by (intro tendsto_intros limit)
      qed (use elim in auto)
    qed
  qed
  show "summable (λn. norm (b n))"
    by (rule summable_comparison_test_ev[OF _ ‹summable M›]) (use bound' in auto)

  from bound obtain Pf Pg where
    *: "eventually Pf at_top" "eventually Pg F" "⋀k n. Pf k ⟹ Pg n ⟹ norm (a k n) ≤ M k"
    unfolding eventually_prod_filter by auto

  show "((λn. ∑k. a k n) ⤏ (∑k. b k)) F"
  proof (rule swap_uniform_limit')
    show "(λK. (∑k<K. b k)) ⇢ (∑k. b k)"
      using ‹summable (λn. norm (b n))›
      by (intro summable_LIMSEQ) (auto dest: summable_norm_cancel)
    show "∀⇩F K in sequentially. ((λn. ∑k<K. a k n) ⤏ (∑k<K. b k)) F"
      by (intro tendsto_intros always_eventually allI limit)
    show "∀⇩F x in F. x ∈ {n. Pg n}"
      using *(2) by simp
    show "uniform_limit {n. Pg n} (λK n. ∑k<K. a k n) (λn. ∑k. a k n) sequentially"
    proof (rule Weierstrass_m_test_ev)
      show "∀⇩F k in at_top. ∀n∈{n. Pg n}. norm (a k n) ≤ M k"
        using *(1) by eventually_elim (use *(3) in auto)
      show "summable M"
        by fact
    qed
  qed auto
qed

end