Theory Lower_Bounds

theory Lower_Bounds
  imports Coding_Theorem_Definitions "../Coding/Lemma_1_8_Coding" "Digit_Expansions.Bits_Digits"
          "HOL-Library.Rewrite" "../Coding/Suitable_For_Coding"
begin

subsection ‹Lower bounds on the defined variables›

lemma (in coding_variables) defs_non_negative: 
  fixes g :: int
  assumes "a ≥ 0"
  assumes "f > 0"
  assumes "g ≥ 0"
  assumes "δ > 0"
  assumes "P_coeff (replicate (ν+1) 0) > 0"
  shows "ℬ > 0" and "N ≥ 2" and "R g > 0" and "S g ≥ 0" and "T ≥ 0" and "N0 ≥ 1"
proof -
  note simps = eval_def insertion_simps comp_def

  have "β > 0"
    unfolding β_def by auto
  hence "β ≥ 0"
    by auto
  have b: "b > 2"
    unfolding b_def apply (simp add: assms)
    using assms(1-2) by (smt (verit) mult_le_cancel_right2)
  moreover have "ℬ ≥ b"
    unfolding ℬ_def
    using ‹δ > 0› ‹β > 0›
    by (smt (verit, del_insts) calculation comp_apply mult_le_cancel_right1 
        of_nat_0_less_iff self_le_power)
  ultimately have "ℬ > 2"
    by auto
  then show BB: "ℬ > 0"
    by auto
  show N0: "N0 ≥ 1"
    unfolding N0_def
    using ‹ℬ > 0›
    by (simp add: int_one_le_iff_zero_less)
  show N: "N ≥ 2"
    using ‹N0 ≥ 1› ‹ℬ > 0›
    unfolding N_def N1_def eval_def
    by simp (smt (z3) mult_pos_pos zero_less_power)
  have m: "(m j) ≥ 0" for j
    unfolding m_def
    using ‹ℬ ≥ b› ‹ℬ > 2›
    by (auto simp: eval_def)
  have M: "M ≥ 0"
    unfolding M_def
    using m BB by (simp add: sum_nonneg)
  show "T ≥ 0"
    unfolding T_def
    using N0 M BB ‹2 < ℬ› by force

  have "K g ≥ 0"
  proof - 
    have "2 ≤ int (Suc δ)"
      using ‹δ > 0› by auto
    have "1 < nat ℬ"
      using ‹ℬ > 2›
      unfolding ℬ_def eval_def by auto
    hence "ℬ ≥ 2"
      by auto

    have "even β"
      by (simp add: β_def r_pos[OF ‹δ > 0›])
    have "even ℬ"
      unfolding ℬ_def simps β_def
      using r_pos[OF ‹δ > 0›]
      by simp

    have c_bound: "c g > 0"
      unfolding c_def using BB
      by (simp add: add_strict_increasing assms(1) assms(3))

    (* This follows from the definition of β and r. *)
    have δ_ℒ_bound: "fact δ * ℒ < ℬ - 1"
    proof - 
      have "fact δ * ℒ < fact δ * ℒ * (ν + 3) ^ δ * b ^ δ"
        using ‹δ > 0› ℒ_pos[OF ‹δ > 0›] 
        by simp (smt (verit) b eval_def less_1_mult o_apply of_nat_less_0_iff one_less_power)
      hence "fact δ * ℒ < 2 * fact δ * ℒ * (ν + 3) ^ δ * b ^ δ - 1"
        by linarith
      moreover have "2 * fact δ * ℒ * (ν + 3) ^ δ * b ^ δ < 4 ^ r * b ^ δ"
        using β_lower_bound[unfolded β_def]
        by (smt (z3) b fact_2 int_eq_iff_numeral less_imp_of_nat_less mult_of_nat_commute 
            numeral_Bit0 of_nat_fact of_nat_power zero_less_power zmult_zless_mono2)
      ultimately show ?thesis
        unfolding ℬ_def β_def
        by auto
    qed

    have D_bound: "D > 0"
    proof -
      let ?i0 = "replicate (ν+1) 0"
      let ?a0 = "P_coeff ?i0"

      have "?a0 > 0"
        using assms by auto

      have h0: "i∈δ_tuples - {replicate (ν+1) 0} ⟹ sum_list i > 0" for i
        apply (rule ccontr)
        unfolding δ_tuples_def using replicate_eqI by fastforce

      have h1: "(∑r=0..(δ+1)^(ν+1)-1. ℬ ^ r) > 0"
        apply (subst sum_pos)
        using ℬ_def BB eval_def by (auto)

      have h2: "D_precoeff ?i0 * P_coeff ?i0 * ℬ ^ D_exponent ?i0
                = fact δ * ?a0 * ℬ ^ ((δ+1)^(ν+1))"
      proof -
        have "(∑s≤ν. ?i0 ! s * Suc δ ^ s) = 0"
          by auto (metis List.nth_replicate le_imp_less_Suc replicate_Suc)
        thus ?thesis
          unfolding D_precoeff_def D_exponent_def
          using ‹?a0 > 0› apply (simp add: sum_list_replicate)
          by (simp add: mfact_def ℬ_def n_def)
      qed

      have h3: "?i0 ∈ δ_tuples"
        by (simp add: sum_list_replicate δ_tuples_def)

      have h4: "(∑i∈δ_tuples - {?i0}. ℬ ^ D_exponent i) ≤ (∑r=0..(δ+1)^(ν+1)-1. ℬ ^ r)"
      proof -
        have h41: "D_exponent ` (δ_tuples - {?i0}) ⊆ {0..(δ+1)^(ν+1)-1}"
        proof -
          {
            fix x
            assume asm: "x ∈ (δ_tuples - {?i0})"
            hence "length x = Suc ν"
              unfolding δ_tuples_def by simp
            have x_nonzero: "∃s≤ν. x ! s > 0"
              apply (rule ccontr)
              using h0[OF asm]
              by (simp add: sum_list_sum_nth ‹length x = Suc ν›)
            then obtain i where i: "i ≤ ν ∧ x ! i > 0"
              by auto
            have "(∑s≤ν. x ! s * Suc δ ^ s) > 0"
                using x_nonzero by (subst sum_pos2[of _ i], auto simp: i)
          } note a = this

          from a show ?thesis
            unfolding D_exponent_def
            apply (simp add: n_def)
            using diff_le_mono2 by fastforce
        qed

        have "(∑i∈δ_tuples - {?i0}. ℬ ^ D_exponent i) 
              = sum ((^) ℬ ∘ D_exponent) (δ_tuples - {?i0})"
          by auto
        also have "... = sum ((^) ℬ) (D_exponent ` (δ_tuples - {?i0}))"
          apply (subst sum.reindex)
          using D_exponent_injective'[OF ‹δ > 0›] by auto
        also have "... ≤ sum ((^) ℬ) {0..(δ+1)^(ν+1)-1}"
          apply (subst sum_mono2)
          using h41 ‹ℬ ≥ 2› by auto
        finally show ?thesis
          by auto
      qed

      have "¦D - fact δ * ?a0 * ℬ ^ ((δ+1)^(ν+1))¦
            = ¦(∑i∈δ_tuples - {?i0}. D_precoeff i * P_coeff i * ℬ ^ D_exponent i)¦"
        apply (subst abs_eq_iff, rule disjI1)
        unfolding D_def eval_def apply simp
        apply (subst sum.remove[of "δ_tuples" "?i0"])
        using h2 h3  ‹?a0 > 0› by auto
      also have "... ≤ (∑i∈δ_tuples - {?i0}. ¦D_precoeff i * P_coeff i *
                                              ℬ ^ D_exponent i¦)"
        by auto
      also have "... ≤ (∑i∈δ_tuples - {?i0}. ¦D_precoeff i¦ * ¦P_coeff i¦ *
                                              ¦ℬ¦ ^ D_exponent i)"
        apply (rule sum_mono)
        by (auto simp: abs_mult power_abs)
      also have "... ≤ (∑i∈δ_tuples - {?i0}. fact δ * ¦P_coeff i¦ * ¦ℬ¦ ^ D_exponent i)"
        apply (rule sum_mono)
        apply (frule h0)
        unfolding δ_tuples_def
        by auto (smt (verit, best) ℬ_def D_precoeff_bound mult_right_mono zero_le_power)
      also have "... ≤ (∑i∈δ_tuples - {?i0}. fact δ * ℒ * ℬ ^ D_exponent i)"
        apply (rule sum_mono)
        using ℬ_def BB eval_def
        by (simp add: ℒ_ge_P_coeff mult_right_mono)
      also have "... = fact δ * ℒ * (∑i∈δ_tuples - {?i0}. ℬ ^ D_exponent i)"
        by (simp add: sum_distrib_left)
      also have "... ≤ fact δ * ℒ * (∑r=0..(δ+1)^(ν+1)-1. ℬ ^ r)"
        using h4 by (simp add: ℒ_pos[OF ‹δ > 0›])
      also have "... = (∑r=0..(δ+1)^(ν+1)-1. fact δ * ℒ * ℬ ^ r)"
        by (simp add: sum_distrib_left)
      also have "... ≤ (∑r=0..(δ+1)^(ν+1)-1. (ℬ - 1) * ℬ ^ r)"
        apply (rule sum_mono)
        using δ_ℒ_bound h1 ‹1 < nat ℬ› by fastforce
      also have "... < ℬ ^ ((δ+1)^(ν+1))"
        using series_bound[OF ‹ℬ ≥ 2›, of "(δ + 1) ^ (ν + 1) - 1" "λx. ℬ - 1"] by auto
      finally have "¦D - fact δ * ?a0 * ℬ ^ ((δ+1)^(ν+1))¦ < ℬ ^ ((δ+1)^(ν+1))"
        by auto

      hence "fact δ * ?a0 * ℬ ^ ((δ+1)^(ν+1)) - D < ℬ ^ ((δ+1)^(ν+1))"
        by auto
      hence "D > (fact δ * ?a0 - 1) * ℬ ^ ((δ+1)^(ν+1))"
        by (simp add: int_distrib(3))

      thus ?thesis
        using ‹?a0 > 0› BB
        unfolding ℬ_def eval_def
        by (smt (verit, ccfv_SIG) fact_gt_zero mult_le_0_iff mult_nonneg_nonneg o_apply zero_le_power)
    qed

    moreover have "(∑i = 0..(2 * δ + 1) * n ν. of_nat (β div 2) * b ^ δ * ℬ ^ i) ≥ 0"
      using BB ‹β ≥ 0› b
      unfolding eval_def
      apply simp
      by (rule sum_nonneg, simp)

    ultimately show ?thesis
      using ‹δ > 0› c_bound D_bound
      unfolding K_def eval_def
      by auto
  qed

  show "S g ≥ 0"
    unfolding S_def using N0
    by (simp add: ‹0 ≤ K g› assms(3))
  
  show "R g > 0"
    unfolding R_def
    using ‹T ≥ 0› ‹S g ≥ 0› ‹N ≥ 2› by auto
qed

lemma (in coding_variables) lower_bounds: 
  fixes g :: int
  assumes "a ≥ 0"
  assumes "f > 0"
  assumes "g ≥ 0"
  assumes "δ > 0"
  assumes p0: "P_coeff (replicate (ν+1) 0) > 0"
  shows "X g ≥ 3 * b" and "Y ≥ 2^8" and "Y ≥ b"
proof -
  note nonneg = defs_non_negative[OF assms(1-4)]
  note simps = eval_def insertion_simps comp_def

  have "β > 0"
    unfolding β_def by auto
  have "b ≤ ℬ"
    unfolding ℬ_def
    using nonneg[OF p0] ‹δ > 0› ‹β > 0›
    by (smt (verit, del_insts) ℬ_def comp_apply insertion_mult insertion_of_nat insertion_pow
            mult_le_cancel_right1 of_nat_0_less_iff self_le_power)

  from ‹b ≤ ℬ› have "3 * b ≤ 4 * ℬ"
    using nonneg(1)[OF p0] by auto
  also have "... ≤ N1"
    unfolding N1_def 
    using nonneg[OF p0] by auto
  also have "... ≤ N"
    unfolding N_def 
    using nonneg(2,6)[OF p0] N_def mult_le_cancel_right1 by force
  also have "... ≤ R g"
    unfolding R_def 
    using nonneg(2,4,5)[OF p0]
    using comp_apply mult_le_cancel_right1
    by (smt (verit) insertion_of_int of_int_1)
  also have "... ≤ X g"
    unfolding X_def 
    using nonneg[OF p0] by auto
  finally show "X g ≥ 3 * b" .

  have "b ≥ 2"
    unfolding b_def apply (simp add: assms)
    using assms(1-2) by (smt (verit) mult_le_cancel_right2)
  with ‹b ≤ ℬ› have "ℬ ≥ 2"
    by auto
  hence "N0 ≥ 2"
    unfolding N0_def 
    using ‹δ > 0›
    by auto (smt (verit, del_insts) mult_le_cancel_right2 zero_less_power)
  moreover from ‹ℬ ≥ 2› have "N1 ≥ 2^3"
    unfolding N1_def 
    using ‹δ > 0›
    by auto (smt (verit, del_insts) mult_le_cancel_right2 zero_less_power)
  ultimately have "N ≥ 2^4"
    unfolding N_def 
    by (smt (verit, del_insts) mult_left_mono mult_right_mono not_exp_less_eq_0_int
            power3_eq_cube power4_eq_xxxx power_commuting_commutes)
  hence "Y ≥ (2^4)^2"
    unfolding Y_def 
    unfolding power2_eq_square
    using mult_mono' by fastforce
  then show "Y ≥ 2^8"
    by auto

  from ‹b ≤ ℬ› have "b ≤ N0"
    unfolding N0_def 
    using nonneg[OF p0]
    by (smt (verit) add_gr_0 comp_apply self_le_power zero_less_one)
  also have "... ≤ N"
    unfolding N_def 
    using nonneg(6)[OF p0] ‹2 ^ 3 ≤ N1› by auto
  also have "... ≤ Y"
    unfolding Y_def 
    by (smt (verit) pos2 power2_less_0 self_le_power)
  finally show "Y ≥ b" .
qed

end