Theory Preliminaries

theory Preliminaries
  imports "HOL-Analysis.Analysis"

notation powr (infixr ".^" 80)

section ‹Preliminary Definitions and Lemmas›

lemma seq_part_multiple: fixes m n :: nat assumes "m  0" defines "A  λi::nat. {i*m ..< (i+1)*m}"
  shows "i j. i  j  A i  A j = {}" and "(i<n. A i) = {..< n*m}"
proof -
  { fix i j :: nat
    have "i  j  A i  A j = {}"
    proof (erule contrapos_np)
      assume "A i  A j  {}"
      then obtain k where "k  A i  A j" by blast
      hence "i*m < (j+1)*m  j*m < (i+1)*m" unfolding A_def by force
      hence "i < j+1  j < i+1" using mult_less_cancel2 by blast
      thus "i = j" by force
    qed }
  thus "i j. i  j  A i  A j = {}" by blast
  show "(i<n. A i) = {..< n*m}"
    show "(i<n. A i)  {..< n*m}"
      fix x::nat
      assume "x  (i<n. A i)"
      then obtain i where i_n: "i < n" and i_x: "x < (i+1)*m" unfolding A_def by force
      hence "i+1  n" by linarith
      hence "x < n*m" by (meson less_le_trans mult_le_cancel2 i_x)
      thus "x  {..< n*m}"
        using diff_mult_distrib mult_1 i_n by auto
    show "{..< n*m}  (i<n. A i)"
      fix x::nat
      let ?i = "x div m"
      assume "x  {..< n*m}"
      hence "?i < n" by (simp add: less_mult_imp_div_less)
      moreover have "?i*m  x  x < (?i+1)*m"
        using assms div_times_less_eq_dividend dividend_less_div_times by auto
      ultimately show "x  (i<n. A i)" unfolding A_def by force

lemma(in field) divide_mult_cancel[simp]: fixes a b assumes "b  0"
  shows "a / b * b = a"
  by (simp add: assms)

lemma inverse_powr: "(1/a).^b = a.^-b" if "a > 0" for a b :: real
  by (smt that powr_divide powr_minus_divide powr_one_eq_one)

lemma powr_eq_one_iff_gen[simp]: "a.^x = 1  x = 0" if "a > 0" "a  1" for a x :: real
  by (metis powr_eq_0_iff powr_inj powr_zero_eq_one that)

lemma powr_less_cancel2: "0 < a  0 < x  0 < y  x.^a < y.^a  x < y"
  for a x y ::real
proof -
  assume a_pos: "0 < a" and x_pos: "0 < x" and y_pos: "0 < y"
  show "x.^a < y.^a  x < y"
  proof (erule contrapos_pp)
    assume "¬ x < y"
    hence "x  y" by fastforce
    hence "x.^a  y.^a"
    proof (cases "x = y")
      case True
      thus ?thesis by simp
      case False
      hence "x.^a > y.^a"
        using x  y powr_less_mono2 a_pos y_pos by auto
      thus ?thesis by auto
    thus "¬ x.^a < y.^a" by fastforce

lemma geometric_increasing_sum_aux: "(1-r)^2 * (k<n. (k+1)*r^k) = 1 - (n+1)*r^n + n*r^(n+1)"
  for n::nat and r::real
proof (induct n)
  case 0
  thus ?case by simp
  case (Suc n)
  thus ?case
    by (simp add: distrib_left power2_diff field_simps power2_eq_square)

lemma geometric_increasing_sum: "(k<n. (k+1)*r^k) = (1 - (n+1)*r^n + n*r^(n+1)) / (1-r)^2"
  if "r  1" for n::nat and r::real
  by (subst geometric_increasing_sum_aux[THEN sym], simp add: that)

lemma Reals_UNIV[simp]: " = {x::real. True}"
  unfolding Reals_def by auto

lemma DERIV_fun_powr2:
  fixes a::real
  assumes a_pos: "a > 0"
    and f: "DERIV f x :> r"
  shows "DERIV (λx. a.^(f x)) x :> a.^(f x) * r * ln a"
proof -
  let ?g = "(λx. a)"
  have g: "DERIV ?g x :> 0" by simp
  have pos: "?g x > 0" by (simp add: a_pos)
  show ?thesis
    using DERIV_powr[OF g pos f] a_pos by (auto simp add: field_simps)

lemma has_real_derivative_powr2:
  assumes a_pos: "a > 0"
  shows "((λx. a.^x) has_real_derivative a.^x * ln a) (at x)"
proof -
  let ?f = "(λx. x::real)"
  have f: "DERIV ?f x :> 1" by simp
  thus ?thesis using DERIV_fun_powr2[OF a_pos f] by simp

lemma has_integral_powr2_from_0:
  fixes a c :: real
  assumes a_pos: "a > 0" and a_neq_1: "a  1" and c_nneg: "c  0"
  shows "((λx. a.^x) has_integral ((a.^c - 1) / (ln a))) {0..c}"
proof -
  have "((λx. a.^x) has_integral ((a.^c)/(ln a) - (a.^0)/(ln a))) {0..c}"
  proof (rule fundamental_theorem_of_calculus[OF c_nneg])
    fix x::real
    assume "x  {0..c}"
    show "((λy. a.^y / ln a) has_vector_derivative a.^x) (at x within {0..c})"
      using has_real_derivative_powr2[OF a_pos, of x]
      apply -
      apply (drule DERIV_cdivide[where c = "ln a"], simp add: assms)
      apply (rule has_vector_derivative_within_subset[where S=UNIV and T="{0..c}"], auto)
      by (rule iffD1[OF has_real_derivative_iff_has_vector_derivative])
  thus ?thesis
    using assms powr_zero_eq_one by (simp add: field_simps)

lemma integrable_on_powr2_from_0:
  fixes a c :: real
  assumes a_pos: "a > 0" and a_neq_1: "a  1" and c_nneg: "c  0"
  shows "(λx. a.^x) integrable_on {0..c}"
  using has_integral_powr2_from_0[OF assms] unfolding integrable_on_def by blast

lemma integrable_on_powr2_from_0_general:
  fixes a c :: real
  assumes a_pos: "a > 0" and c_nneg: "c  0"
  shows "(λx. a.^x) integrable_on {0..c}"
proof (cases "a = 1")
  case True
  thus ?thesis
    using has_integral_const_real by auto
  case False
  thus ?thesis
    using has_integral_powr2_from_0 False assms by auto

lemma has_integral_null_interval: fixes a b :: real and f::"real  real" assumes "a  b"
  shows "(f has_integral 0) {a..b}"
  using assms content_real_eq_0 by blast

lemma has_integral_interval_reverse: fixes f :: "real  real" and a b :: real
  assumes "a  b"
    and "continuous_on {a..b} f"
  shows "((λx. f (a+b-x)) has_integral (integral {a..b} f)) {a..b}"
proof -
  let ?g = "λx. a + b - x"
  let ?g' = "λx. -1"
  have g_C0: "continuous_on {a..b} ?g" using continuous_on_op_minus by simp
  have Dg_g': "x. x{a..b}  (?g has_field_derivative ?g' x) (at x within {a..b})"
    by (auto intro!: derivative_eq_intros)
  show ?thesis
    using has_integral_substitution_general
      [of "{}" a b ?g a b f, simplified, OF assms g_C0 Dg_g', simplified]
    apply (simp add: has_integral_null_interval[OF assms(1), THEN integral_unique])
    by (simp add: has_integral_neg_iff)