Theory RealPower
section ‹Real Exponents via Limits›
theory RealPower
imports RatPower
begin
instance rat :: ab_group_add
by intro_classes
instance rat :: field
by intro_classes
instance rat :: comm_ring_1
by intro_classes
instantiation rat :: dist
begin
definition rat_dist_def:
"dist x y = of_rat (abs(y - x))"
instance ..
end
instantiation rat :: dist_norm
begin
definition rat_norm_def:
"norm (q::rat) = of_rat ¦q¦"
instance
by intro_classes (simp add: rat_dist_def rat_norm_def)
end
instantiation rat :: metric_space
begin
definition uniformity_rat_def [code del]:
"(uniformity :: (rat × rat) filter) =
(INF e∈{0 <..}. principal {((x::rat), y). dist x y < e})"
definition open_rat_def [code del]:
"open (U :: rat set) ⟷
(∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"
instance
proof
show "uniformity =
(INF e∈{0<..}. principal {(x::rat, y). dist x y < e})"
using uniformity_rat_def by blast
next
fix U
show "open U =
(∀x∈U. ∀⇩F (x', y::rat) in uniformity. x' = x ⟶ y ∈ U)"
using open_rat_def by blast
next
fix x y show "(dist x y = 0) = (x = (y::rat))"
by (force simp add: rat_dist_def)
next
fix x y z show "dist x y ≤ dist x z + dist y (z::rat)"
by (force simp add: rat_dist_def of_rat_add [symmetric] of_rat_less_eq)
qed
end
instance rat :: topological_space
by intro_classes
lemma LIMSEQ_squeeze:
assumes abc: "∀n. a n ≤ b n ∧ b n ≤ c n"
and alim: "a ⇢ (L::real)"
and clim: "c ⇢ L" shows "b ⇢ L"
proof -
{fix r
assume r0: "(r::real) > 0"
then have "∃no. ∀n≥no. ¦a n - L¦ < r"
by (metis LIMSEQ_def alim dist_real_def)
then obtain p where 1: "∀n≥p. ¦a n - L¦ < r" by blast
have "∃no. ∀n≥no. ¦c n - L¦ < r"
by (metis LIMSEQ_def r0 clim dist_real_def)
then obtain k where 2: "∀n≥k. ¦c n - L¦ < r" by blast
have "∃m. ∀n≥m. ¦b n - L¦ < r"
proof -
{fix n
assume n_max: "max p k ≤ n"
then have a_n: "¦a n - L¦ < r" using 1 by simp
have c_n: "¦c n - L¦ < r" using n_max 2 by simp
have "a n ≤ b n ∧ b n ≤ c n" using abc by simp
then have "¦b n - L¦ < r"
using a_n c_n by linarith
}
then have "∀n≥max p k. ¦b n - L¦ < r"
by blast
then show ?thesis by blast
qed
}
then have "∀r>0. ∃m. ∀n≥m. ¦b n - L¦ < r"
by blast
then show ?thesis
by (simp add: dist_real_def lim_sequentially)
qed
primrec incratseq :: "real ⇒ nat ⇒ rat" where
"incratseq x 0 = (ϵq. x - 1 < of_rat q ∧ of_rat q < x)"
| "incratseq x (Suc n) =
(ϵq. max (of_rat(incratseq x n)) (x - 1/(n + 2)) < of_rat q ∧
of_rat q < x)"
lemma incratseq_0_gt [simp]: "x - 1 < of_rat(incratseq x 0)"
proof -
have "x - 1 < x" by simp
then have "∃q. x - 1 < real_of_rat q ∧ real_of_rat q < x"
using of_rat_dense
by blast
then obtain q where " x - 1 < real_of_rat q ∧ real_of_rat q < x"
by force
then show ?thesis
by (auto intro: someI2)
qed
lemma incratseq_0_less [simp]: "of_rat(incratseq x 0) < x"
proof -
have "x - 1 < x" by simp
then have "∃q. x - 1 < real_of_rat q ∧ real_of_rat q < x"
using of_rat_dense
by blast
then obtain q where " x - 1 < real_of_rat q ∧ real_of_rat q < x"
by force
then show ?thesis
by (auto intro: someI2)
qed
declare incratseq.simps [simp del]
lemma incratseq_ub [simp]:
"real_of_rat (incratseq x n) < x"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
proof (cases "real_of_rat (incratseq x n) ≤ x - 1/(n + 2)")
case True
then have "x - 1/(Suc(Suc n)) < x" by simp
then have "∃q. x - 1 / real (Suc (Suc n))
< real_of_rat q ∧
real_of_rat q < x"
using of_rat_dense by blast
then have "∃a. (if True then x - 1 / real (n + 2)
else real_of_rat
(incratseq x n))
< real_of_rat a ∧
real_of_rat a < x"
by auto
then have "real_of_rat
(SOME q.
(if real_of_rat
(incratseq x n)
≤ x - 1 / real (n + 2)
then x - 1 / real (n + 2)
else real_of_rat
(incratseq x n))
< real_of_rat q ∧
real_of_rat q < x)
< x"
using True by (fastforce intro: someI2_ex)
then show ?thesis
by (auto simp only: incratseq.simps max_def)
next
case False
then have "∃a. real_of_rat (incratseq x n)
< real_of_rat a ∧
real_of_rat a < x"
using Suc of_rat_dense by auto
then have "real_of_rat
(SOME q.
(if real_of_rat
(incratseq x n)
≤ x - 1 / real (n + 2)
then x - 1 / real (n + 2)
else real_of_rat
(incratseq x n))
< real_of_rat q ∧
real_of_rat q < x)
< x"
using False by (fastforce intro: someI2_ex)
then show ?thesis
by (simp only: incratseq.simps max_def)
qed
qed
lemma incratseq_incseq [simp]:
"incratseq x n < incratseq x (Suc n)"
proof -
have "max (real_of_rat (incratseq x n)) (x - 1 / real (n + 2)) < x"
by simp
then have "∃q. max (real_of_rat (incratseq x n))
(x - 1 / real (n + 2))
< real_of_rat q ∧
real_of_rat q < x"
using of_rat_dense by blast
then have "incratseq x n
< (SOME q.
max (real_of_rat (incratseq x n))
(x - 1 / real (n + 2))
< real_of_rat q ∧
real_of_rat q < x)"
by (fastforce intro: someI2_ex simp add: of_rat_less)
then show ?thesis
by (simp only: incratseq.simps)
qed
lemma incratseq_lb [simp]: "x - 1/(Suc n) < real_of_rat (incratseq x n)"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
proof (cases "real_of_rat (incratseq x n) ≤ x - 1/Suc(Suc n)")
case True
then have " 1 / Suc(Suc n) < 1 / Suc n"
using Suc.IH by auto
have "x - 1/Suc(Suc n) < x"
by simp
then have "∃a. x - 1 /Suc(Suc n) < real_of_rat a ∧ real_of_rat a < x"
using of_rat_dense by blast
then have "x - 1 / real (Suc (Suc n))
< real_of_rat
(SOME q.
(if real_of_rat (incratseq x n) ≤ x - 1 / Suc(Suc n)
then x - 1 / Suc(Suc n) else real_of_rat (incratseq x n))
< real_of_rat q ∧
real_of_rat q < x)"
using True by (auto intro: someI2_ex)
then show ?thesis using True
by (auto simp add: incratseq.simps(2) max_def)
next
case False
then show ?thesis
using incratseq_incseq
by (meson less_trans not_less of_rat_less)
qed
qed
lemma incseq_incratseq [simp]:
"incseq (incratseq x)"
by (auto intro!: incseq_SucI less_imp_le)
lemma LIMSEQ_rat_real_ex:
"∃r. incseq r ∧ (λn. of_rat (r n)) ⇢ (x::real)"
proof -
have squeeze_left:
"∀n. x - 1 / real (Suc n)
≤ real_of_rat (incratseq x n) ∧ real_of_rat (incratseq x n) ≤ x"
using incratseq_lb less_imp_le
by (simp add: less_imp_le)
moreover have "(λn. x - 1 / real (Suc n)) ⇢ x"
by (simp only: minus_real_def LIMSEQ_inverse_real_of_nat_add_minus
inverse_eq_divide [symmetric])
ultimately have "(λn. real_of_rat (incratseq x n)) ⇢ x"
using LIMSEQ_squeeze tendsto_const by fastforce
then show ?thesis
using incseq_incratseq by blast
qed
lemma incseq_incseq_powrat:
"⟦ 1 ≤ a; incseq r ⟧ ⟹ incseq (λn. a pow⇩ℚ (r n))"
by (metis (lifting) incseq_def powrat_le_mono)
lemma ex_less_of_rat: "∃r. (x :: 'a :: archimedean_field) < of_rat r"
using ex_less_of_int of_rat_of_int_eq by metis
lemma powrat_incseq_bounded:
"⟦ 1 ≤ a; ∀n. r n < of_rat q; incseq r ⟧ ⟹ a pow⇩ℚ (r n) ≤ a pow⇩ℚ q"
by (simp add: less_imp_le powrat_le_mono)
lemma Bseq_powrat_incseq:
assumes "1 ≤ a"
and "incseq r"
and "∀n. of_rat(r n) ≤ (x :: 'a :: archimedean_field)"
shows "Bseq (λn. a pow⇩ℚ (r n))"
proof -
from ex_less_of_rat
obtain q where xq: "x < of_rat q" by blast
then have "∀n. 0 ≤ a pow⇩ℚ r n ∧ a pow⇩ℚ r n ≤ a pow⇩ℚ of_rat q"
proof -
{fix m
have " r m < q"
using assms(3) le_less_trans of_rat_less xq by blast
then have "a pow⇩ℚ r m ≤ a pow⇩ℚ of_rat q"
by (simp add: assms(1) powrat_le_mono)}
then show ?thesis using less_imp_le [OF powrat_gt_zero]
using assms(1) by auto
qed
then show ?thesis
by (metis BseqI2' abs_of_nonneg real_norm_def)
qed
lemma convergent_powrat_incseq:
"⟦ 1 ≤ a; incseq r; ∀n. r n ≤ x ⟧ ⟹ convergent (λn. a pow⇩ℚ (r n))"
by (auto intro!: Bseq_monoseq_convergent
intro: incseq_imp_monoseq incseq_incseq_powrat Bseq_powrat_incseq [of _ _ x])
definition
incseq_of :: "real ⇒ (nat ⇒ rat)" where
"incseq_of x = (SOME r. incseq r ∧ (λn. of_rat (r n)) ⇢ x)"
lemma LIMSEQ_incseq_of [simp]:
"(λn. of_rat (incseq_of x n)) ⇢ x"
by (auto intro: someI2_ex [OF LIMSEQ_rat_real_ex] simp add: incseq_of_def)
lemma incseq_incseq_of [simp]:
"incseq (incseq_of x)"
by (auto intro: someI2_ex [OF LIMSEQ_rat_real_ex] simp add: incseq_of_def)
lemma incseq_of_Suc [simp]:
"incseq_of x n ≤ incseq_of x (Suc n)"
by (metis incseq_def incseq_incseq_of le_SucI le_refl)
lemma incseq_of_rat_incseq_of:
"incseq (λn. of_rat(incseq_of x n) :: 'a::linordered_field)"
by (meson incseq_def incseq_incseq_of of_rat_less_eq)
lemma incseq_of_rat:
"incseq s ⟹ incseq (λn. of_rat(s n) :: 'a :: linordered_field)"
by (auto simp add: incseq_def of_rat_less_eq)
lemma incseq_rat_le_real:
"⟦ incseq s; (λn. of_rat (s n)) ⇢ x ⟧ ⟹ of_rat (s n) ≤ (x::real)"
by (auto intro: incseq_le incseq_of_rat)
lemma incseq_of_le_self: "of_rat(incseq_of x n) ≤ x"
by (auto intro!: incseq_rat_le_real LIMSEQ_incseq_of)
lemma powrat_incseq_of_bounded:
"⟦ 1 ≤ a; x < of_rat r ⟧ ⟹ a pow⇩ℚ (incseq_of x n) ≤ a pow⇩ℚ r"
by (meson incseq_of_le_self le_less le_less_trans of_rat_less powrat_le_mono)
lemma incseq_powrat_insec_of:
"1 ≤ a ⟹ incseq (λn. a pow⇩ℚ (incseq_of x n))"
by (auto intro: incseq_incseq_powrat)
lemma Bseq_powrat_incseq_of: "1 ≤ a ⟹ Bseq (λn. a pow⇩ℚ (incseq_of x n))"
by (auto intro!: Bseq_powrat_incseq incseq_of_le_self)
lemma convergent_powrat_incseq_of: "1 ≤ a ⟹ convergent (λn. a pow⇩ℚ (incseq_of x n))"
by (blast intro: Bseq_monoseq_convergent Bseq_powrat_incseq_of incseq_imp_monoseq
incseq_powrat_insec_of)
text‹We're now ready to define real exponentation.›
definition
powa :: "[real,real] ⇒ real" (infixr ‹powa› 80) where
"a powa x = (THE y. (λn. a pow⇩ℚ (incseq_of x n)) ⇢ y)"
text ‹real exponents.›
definition
powreal :: "[real,real] ⇒ real" (infixr ‹pow⇩ℝ› 80) where
"a pow⇩ℝ x = (if 0 < a ∧ a < 1 then (inverse a) powa (-x)
else if a ≥ 1 then a powa x else 0)"
lemma powreal_eq_powa:
"a ≥ 1 ⟹ a pow⇩ℝ x = a powa x"
by (simp add: powreal_def)
lemma LIMSEQ_powrat_incseq_of_ex1:
"1 ≤ a ⟹ ∃!y. (λn. a pow⇩ℚ (incseq_of x n))⇢ y"
by (metis LIMSEQ_unique convergentD convergent_powrat_incseq_of)
lemma LIMSEQ_powa:
"1 ≤ a ⟹ (λn. a pow⇩ℚ (incseq_of x n)) ⇢ a powa x"
unfolding powa_def by (erule theI' [OF LIMSEQ_powrat_incseq_of_ex1])
lemma lemma_incseq_incseq_diff_inverse:
"incseq s ⟹ incseq (λn. (s n :: rat) - 1/of_nat(Suc n))"
by (auto intro: diff_mono simp add: divide_inverse incseq_def)
lemma lemma_incseq_diff_inverse_ub:
assumes "incseq s"
and "(λn. of_rat (s n)) ⇢ x"
shows "of_rat(s n - 1/of_nat(Suc n)) < (x::real)"
proof -
have "real_of_rat (s n - 1 / rat_of_nat (Suc n)) < real_of_rat (s n)"
by (simp add: of_rat_diff)
then show ?thesis
by (meson assms incseq_rat_le_real linorder_not_less order_trans)
qed
lemma lemma_LIMSEQ_incseq_diff_inverse:
assumes "(λn. of_rat (s n)) ⇢ x"
shows " (λn. of_rat(s n - 1/of_nat(Suc n))) ⇢ (x::real)"
proof -
have "(λx. real_of_rat (s x) - inverse (real (Suc x))) ⇢ x"
using assms tendsto_diff [OF _ LIMSEQ_inverse_real_of_nat]
by simp
then show ?thesis
by (simp add: divide_inverse of_rat_diff of_rat_inverse of_rat_add)
qed
lemma lemma_LIMSEQ_powrat_diff_inverse:
assumes "1 ≤ a"
and "(λn. a pow⇩ℚ (s n))⇢ y"
shows "(λn. a pow⇩ℚ (s n - 1/of_nat(Suc n))) ⇢ y"
proof -
have "(λx. a pow⇩ℚ (1 / rat_of_nat (Suc x))) ⇢ 1"
using assms(1) LIMSEQ_powrat_inverse_of_nat
by (auto intro!: LIMSEQ_Suc simp only: divide_inverse mult_1_left)
then have " (λn. a pow⇩ℚ s n / a pow⇩ℚ (1 / rat_of_nat (Suc n))) ⇢ y"
using assms(2) tendsto_divide by fastforce
then show ?thesis using powrat_diff assms(1) by auto
qed
lemma lemma_LIMSEQ_powrat_diff_inverse2:
assumes "1 ≤ a"
and "(λn. a pow⇩ℚ (s n - 1/of_nat(Suc n)))⇢ y"
shows "(λn. a pow⇩ℚ (s n)) ⇢ y"
proof -
have "(λx. a pow⇩ℚ (1 / rat_of_nat (Suc x))) ⇢ 1"
using assms(1) LIMSEQ_powrat_inverse_of_nat
by (auto intro!: LIMSEQ_Suc simp only: divide_inverse mult_1_left)
then have "(λx. a pow⇩ℚ inverse (rat_of_nat (Suc x)) *
a pow⇩ℚ (s x - inverse(rat_of_nat (Suc x))))
⇢ 1 * y"
using assms(2) by (auto intro!: tendsto_mult simp only: inverse_eq_divide)
then show ?thesis using assms(1)
by (auto simp add: powrat_add [symmetric] )
qed
lemma lemma_seq_point_gt_ex:
"⟦ (λn. of_rat (r n)) ⇢ (x::real); y < x ⟧
⟹ ∃(m::nat). y < of_rat(r m)"
by (metis convergent_def limI lim_le not_less)
lemma lemma_seq_point_gt_ex2:
"⟦ (λn. of_rat (r n)) ⇢ (x::real); of_rat y < x ⟧
⟹ (∃m. y < r m)"
by (force dest: lemma_seq_point_gt_ex simp add: of_rat_less)
primrec interlaced_index :: "(nat ⇒ rat) ⇒ (nat ⇒ rat) ⇒ nat ⇒ nat" where
"interlaced_index r s 0 = 0"
| "interlaced_index r s (Suc n) =
(LEAST m. if odd n then r (interlaced_index r s n) < s m
else s (interlaced_index r s n) < r m)"
definition interlaced_seq :: "(nat ⇒ rat) ⇒ (nat ⇒ rat) ⇒ nat ⇒ rat" where
"interlaced_seq r s n = (if odd n then r (interlaced_index r s n)
else s (interlaced_index r s n))"
lemma incseq_interlaced_seq:
assumes "(λn. of_rat (r n)) ⇢ (x::real)"
and "(λn. of_rat (s n)) ⇢ (x::real)"
and "∀n. of_rat (r n) < x"
and "∀n. of_rat (s n) < x"
shows "incseq (interlaced_seq r s)"
proof -
{fix n
have "interlaced_seq r s n ≤ interlaced_seq r s (Suc n)"
using assms
by (auto intro: LeastI2_ex [OF lemma_seq_point_gt_ex2]
simp add: interlaced_seq_def)}
then show ?thesis
by (simp add: incseq_SucI)
qed
lemma incseq_of_rat_interlaced_seq:
"⟦ (λn. of_rat (r n)) ⇢ (x::real);
(λn. of_rat (s n)) ⇢ (x::real);
∀n. of_rat (r n) < x; ∀n. of_rat (s n) < x ⟧
⟹ incseq (λn. real_of_rat (interlaced_seq r s n))"
using incseq_interlaced_seq incseq_of_rat by blast
lemma interlaced_seq_bounded:
"⟦ ∀n. of_rat (r n) < x; ∀n. of_rat (s n) < x⟧
⟹ of_rat (interlaced_seq r s n) < x"
unfolding interlaced_seq_def by auto
lemma convergent_interlaced_seq:
assumes "(λn. of_rat (r n)) ⇢ (x::real)"
and "(λn. of_rat (s n)) ⇢ (x::real)"
and "∀n. of_rat (r n) < x"
and "∀n. of_rat (s n) < x"
shows "convergent (λn. real_of_rat (interlaced_seq r s n))"
proof -
have mono: "monoseq (λn. real_of_rat (interlaced_seq r s n))"
using assms incseq_interlaced_seq incseq_of_rat monoseq_iff by blast
{fix n
have "interlaced_seq r s 0 ≤ interlaced_seq r s n"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
using assms incseq_def incseq_interlaced_seq by blast
qed}
moreover
{fix n
have "real_of_rat (interlaced_seq r s n) ≤ x"
by (simp add: assms(3,4) interlaced_seq_bounded le_less)}
ultimately have "Bseq (λn. real_of_rat (interlaced_seq r s n))"
by (metis decseq_bounded incseq_bounded mono monoseq_iff of_rat_less_eq)
then show ?thesis using mono
by (simp add: Bseq_monoseq_convergent)
qed
lemma convergent_powrat_interlaced_seq:
"⟦ 1 ≤ a; (λn. of_rat (r n)) ⇢ (x::real);
(λn. of_rat (s n)) ⇢ (x::real);
∀n. of_rat (r n) < x; ∀n. of_rat (s n) < x ⟧
⟹ convergent (λn. a pow⇩ℚ (interlaced_seq r s n))"
by (auto intro: Bseq_monoseq_convergent incseq_interlaced_seq
interlaced_seq_bounded less_imp_le incseq_imp_monoseq
incseq_incseq_powrat Bseq_powrat_incseq [of _ _ x])
lemma LIMSEQ_even_odd_subseq_LIMSEQ:
assumes "(λn. (X (2 *n))) ⇢ a" "(λn. (X (Suc(2 *n)))) ⇢ a"
shows "X ⇢ (a :: 'a::real_normed_vector)"
proof (auto simp add: LIMSEQ_iff)
fix r::real
assume e0: "r > 0"
obtain p where evenx: "∀n≥p. norm (X (2 * n) - a) < r"
using e0 assms(1) by (metis LIMSEQ_iff)
obtain q where oddx: "∀n≥q. norm (X (Suc (2 * n)) - a) < r"
using e0 assms(2) by (metis LIMSEQ_iff)
{fix n
assume max: "max (2 * p) (2 * q) ≤ n"
have "norm (X n - a) < r"
proof (cases "even n")
case True
then show ?thesis
using dvd_def evenx max
by auto
next
case False
then show ?thesis using oddx max
by (auto elim: oddE)
qed}
then show "∃no. ∀n≥no. norm (X n - a) < r"
by blast
qed
lemma incseqD2: "incseq r ⟹ r m < r n ⟹ m < n"
by (metis le_less mono_def not_le order.asym)
lemma subseq_interlaced_index_even:
assumes "incseq r"
and "incseq s"
and "(λn. of_rat (r n)) ⇢ (x::real)"
and "(λn. of_rat (s n)) ⇢ (x::real)"
and "∀n. of_rat (r n) < x"
and "∀n. of_rat (s n) < x"
shows "strict_mono (λn. interlaced_index r s (2 * n))"
proof -
{fix n
have "interlaced_index r s (2 * n)
< (LEAST m. r (LEAST m. s (interlaced_index r s (2 * n)) < r m) < s m)"
proof (rule LeastI2_ex [of "λ m. s (interlaced_index r s (2 * n)) < r m"])
show "∃a. s (interlaced_index r s (2 * n)) < r a"
using assms(3) assms(6) lemma_seq_point_gt_ex2 by blast
next
fix m
assume inter_s: "s (interlaced_index r s (2 * n)) < r m"
show "interlaced_index r s (2 * n) < (LEAST ma. r m < s ma) "
proof (rule LeastI2_ex)
show "∃a. r m < s a"
using assms(4) assms(5) lemma_seq_point_gt_ex2 by blast
next
fix k
assume "r m < s k"
then show "interlaced_index r s (2 * n) < k"
using inter_s assms(2) incseqD2 less_trans by blast
qed
qed}
then show ?thesis
by (simp add: strict_mono_Suc_iff)
qed
lemma subseq_interlaced_index_odd:
assumes "incseq r"
and "incseq s"
and "(λn. of_rat (r n)) ⇢ (x::real)"
and "(λn. of_rat (s n)) ⇢ (x::real)"
and "∀n. of_rat (r n) < x"
and "∀n. of_rat (s n) < x"
shows "strict_mono (λn. interlaced_index r s (Suc (2 * n)))"
proof -
{fix n
have "(LEAST m. s (interlaced_index r s (2 * n)) < r m)
< (LEAST m.
s (LEAST m. r (LEAST m. s (interlaced_index r s (2 * n)) < r m) < s m)
< r m)"
proof (rule LeastI2_ex [of "(λ m. s (interlaced_index r s (2 * n)) < r m)"])
show "∃a. s (interlaced_index r s (2 * n)) < r a"
using assms(3) assms(6) lemma_seq_point_gt_ex2 by blast
next
fix m
assume inter_s: "s (interlaced_index r s (2 * n)) < r m"
show "m < (LEAST ma. s (LEAST ma. r m < s ma) < r ma)"
proof (rule LeastI2_ex [of "λma. r m < s ma"])
show "∃a. r m < s a"
using assms(4) assms(5) lemma_seq_point_gt_ex2 by blast
next
fix k
assume rs: "r m < s k"
show "m < (LEAST ma. s k < r ma)"
proof (rule LeastI2_ex)
show "∃a. s k < r a"
using assms(3) assms(6) lemma_seq_point_gt_ex2 by blast
next
fix l
assume "s k < r l"
then show "m < l" using rs
using assms(1) incseqD2 less_trans by blast
qed
qed
qed}
then show ?thesis
by (simp add: strict_mono_Suc_iff)
qed
lemma interlaced_seq_even:
"interlaced_seq r s (2*n) = s (interlaced_index r s (2*n))"
by (simp add: interlaced_seq_def)
lemma interlaced_seq_odd:
"interlaced_seq r s (Suc (2*n)) = r (interlaced_index r s (Suc (2*n)))"
by (simp add: interlaced_seq_def)
lemma powa_indep_incseq_of:
assumes "1 ≤ a"
and "incseq r"
and "incseq s"
and "(λn. real_of_rat (r n)) ⇢ x"
and "(λn. real_of_rat (s n)) ⇢ x"
and "(λn. a pow⇩ℚ (r n)) ⇢ y"
and "(λn. a pow⇩ℚ (s n)) ⇢ z"
shows "y = z"
proof -
have rx: "(λn. real_of_rat (r n - 1 / rat_of_nat (Suc n))) ⇢ x"
using assms(4) lemma_LIMSEQ_incseq_diff_inverse by blast
have sx: "(λn. real_of_rat (s n - 1 / rat_of_nat (Suc n))) ⇢ x"
using assms(5) lemma_LIMSEQ_incseq_diff_inverse by blast
have "convergent
(λn. a pow⇩ℚ
interlaced_seq (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) n)"
using convergent_powrat_interlaced_seq
[of _ "(λn. r n - 1 / rat_of_nat (Suc n))"
_ "(λn. s n - 1 / rat_of_nat (Suc n))"]
assms(1,2,3,4,5) lemma_incseq_diff_inverse_ub
lemma_LIMSEQ_incseq_diff_inverse by blast
then obtain L
where converge: "(λn. a pow⇩ℚ
interlaced_seq (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) n) ⇢ L"
using convergent_def by force
then have "((λn. a pow⇩ℚ
interlaced_seq (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) n) ∘ (λn. 2 * n)) ⇢ L"
by (simp add: LIMSEQ_subseq_LIMSEQ strict_mono_Suc_iff)
moreover have "((λn. a pow⇩ℚ
interlaced_seq (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) n) ∘ (λn. Suc (2 * n))) ⇢ L"
using converge by (simp add: LIMSEQ_subseq_LIMSEQ strict_mono_Suc_iff)
moreover have "((λn. a pow⇩ℚ (r n - 1 / rat_of_nat (Suc n))) ∘
(λn. interlaced_index (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) (Suc (2 * n)))) ⇢ y"
proof -
from rx sx
have "strict_mono
(λn. interlaced_index (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) (Suc (2 * n)))"
using subseq_interlaced_index_odd lemma_incseq_incseq_diff_inverse
lemma_incseq_diff_inverse_ub assms by blast
moreover have "(λn. a pow⇩ℚ (r n - 1 / rat_of_nat (Suc n))) ⇢ y"
using assms(1) assms(6) lemma_LIMSEQ_powrat_diff_inverse by blast
ultimately show ?thesis
using LIMSEQ_subseq_LIMSEQ by blast
qed
moreover have "((λn. a pow⇩ℚ (s n - 1 / rat_of_nat (Suc n))) ∘
(λn. interlaced_index (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) (2 * n)))
⇢ z"
proof -
from rx sx
have "strict_mono
(λn. interlaced_index (λn. r n - 1 / rat_of_nat (Suc n))
(λn. s n - 1 / rat_of_nat (Suc n)) (2 * n))"
using subseq_interlaced_index_even lemma_incseq_incseq_diff_inverse
lemma_incseq_diff_inverse_ub assms by blast
moreover have "(λn. a pow⇩ℚ (s n - 1 / rat_of_nat (Suc n))) ⇢ z"
using assms(1) assms(7) lemma_LIMSEQ_powrat_diff_inverse by blast
ultimately show ?thesis
using LIMSEQ_subseq_LIMSEQ by blast
qed
ultimately show ?thesis
by (force dest: LIMSEQ_unique simp only: o_def interlaced_seq_even interlaced_seq_odd)
qed
lemma powa_indep_incseq_of':
"⟦ 1 ≤ a; incseq r;
(λn. real_of_rat (r n)) ⇢ x;
(λn. a pow⇩ℚ (r n)) ⇢ y ⟧
⟹ (λn. a pow⇩ℚ (incseq_of x n)) ⇢ y"
using powa_indep_incseq_of [of a r "incseq_of x"] LIMSEQ_powa
by fastforce
lemma lemma_incseq_incseq_of_diff_inverse:
"incseq (λn. incseq_of x n - 1/of_nat(Suc n))"
by (blast intro: lemma_incseq_incseq_diff_inverse incseq_incseq_of)
lemma lemma_incseq_of_diff_inverse_ub:
"of_rat(incseq_of x n - 1/of_nat(Suc n)) < x"
by (blast intro: lemma_incseq_diff_inverse_ub incseq_incseq_of LIMSEQ_incseq_of)
lemma lemma_LIMSEQ_incseq_of_diff_inverse:
"(λn. of_rat(incseq_of x n - 1/of_nat(Suc n))) ⇢ x"
by (blast intro: lemma_LIMSEQ_incseq_diff_inverse incseq_incseq_of LIMSEQ_incseq_of)
lemma powa_add:
assumes "1 ≤ a"
shows "a powa (x + y) = a powa x * a powa y"
proof -
obtain k where 1: "(λn. a pow⇩ℚ incseq_of y n) ⇢ k"
using LIMSEQ_powrat_incseq_of_ex1 assms by blast
moreover obtain l where 2: "(λn. a pow⇩ℚ incseq_of x n) ⇢ l"
using LIMSEQ_powrat_incseq_of_ex1 assms by blast
ultimately have "(λn. a pow⇩ℚ (incseq_of x n + incseq_of y n)) ⇢ l * k"
using assms by (auto intro: tendsto_mult simp add: powrat_add )
moreover
have "incseq (λn. incseq_of x n + incseq_of y n)"
by (force intro: incseq_SucI add_mono)
moreover have "(λn. real_of_rat (incseq_of x n + incseq_of y n)) ⇢ x + y"
by (auto simp add: of_rat_add intro: tendsto_add LIMSEQ_incseq_of)
ultimately have "(λn. a pow⇩ℚ incseq_of (x + y) n) ⇢ l * k"
using assms powa_indep_incseq_of' by blast
then show ?thesis using powa_def 1 2
by (metis Lim_def limI)
qed
lemma real_inverse_ge_one_lemma:
"⟦ 0 < (a::real); a < 1 ⟧ ⟹ inverse a ≥ 1"
by (metis less_eq_real_def one_le_inverse_iff)
lemma real_inverse_gt_one_lemma:
"⟦ 0 < (a::real); a < 1 ⟧ ⟹ inverse a > 1"
by (metis one_less_inverse_iff)
lemma real_inverse_bet_one_one_lemma:
"1 < (a::real) ⟹ 0 < inverse a ∧ inverse a < 1"
by (metis inverse_less_1_iff inverse_positive_iff_positive
le_less_trans zero_le_one)
lemma powreal_add:
"a pow⇩ℝ (x + y) = a pow⇩ℝ x * a pow⇩ℝ y"
by (metis minus_add_distrib mult_zero_right powa_add
powreal_def real_inverse_ge_one_lemma)
lemma powa_one_eq_one [simp]: "1 powa a = 1"
proof -
have "(λn. 1 pow⇩ℚ incseq_of a n) ⇢ 1"
by simp
then show ?thesis
by (metis Lim_def limI powa_def)
qed
lemma powreal_one_eq_one [simp]: "1 pow⇩ℝ a = 1"
by (simp add: powreal_def)
lemma powa_zero_eq_one [simp]: "a ≥ 1 ⟹ a powa 0 = 1"
by (auto intro!: the1_equality LIMSEQ_powrat_incseq_of_ex1
intro: powa_indep_incseq_of' [of a "λn. 0"] incseq_SucI
simp add: powa_def)
lemma powreal_zero_eq_one [simp]: "a > 0 ⟹ a pow⇩ℝ 0 = 1"
by (auto dest: real_inverse_ge_one_lemma simp add: powreal_def)
lemma powr_zero_eq_one_iff [simp]: "x pow⇩ℝ 0 = (if x ≤ 0 then 0 else 1)"
using powreal_def powreal_zero_eq_one by force
lemma powa_one_gt_zero [simp]: "1 ≤ a ⟹ a powa 1 = a"
by (auto intro!: LIMSEQ_powrat_incseq_of_ex1 the1_equality
powa_indep_incseq_of' [of a "λn. 1"] incseq_SucI simp add: powa_def)
lemma powa_minus_one:
assumes "1 ≤ a" shows "a powa -1 = inverse a"
proof -
have "(λn. a pow⇩ℚ - 1) ⇢ inverse a" using assms
by (simp add: powrat_minus)
then have "(λn. a pow⇩ℚ incseq_of (- 1) n) ⇢ inverse a"
using powa_indep_incseq_of' [of a "λn. -1"] assms
by simp
then show ?thesis using powa_def
by (metis Lim_def limI)
qed
lemma powreal_minus_one: "0 ≤ a ⟹ a pow⇩ℝ -1 = inverse a"
by (simp add: powa_minus_one powreal_def real_inverse_ge_one_lemma)
lemma powreal_one [simp]: "a ≥ 0 ⟹ a pow⇩ℝ 1 = a"
by (simp add: powa_minus_one powreal_def real_inverse_ge_one_lemma)
lemma powa_gt_zero:
assumes "a ≥ 1"
shows "a powa x > 0"
proof -
obtain y where 1: "(λn. a pow⇩ℚ incseq_of x n) ⇢ y"
using LIMSEQ_powrat_incseq_of_ex1 assms by blast
moreover have "incseq (λn. a pow⇩ℚ incseq_of x n)"
by (simp add: assms incseq_powrat_insec_of)
ultimately have "y > 0"
using assms incseq_le powrat_gt_zero
by (metis less_le_trans zero_less_one)
then show ?thesis using powa_def 1
by (metis Lim_def limI)
qed
lemma powreal_gt_zero: "a > 0 ⟹ a pow⇩ℝ x > 0"
by (auto dest: powa_gt_zero real_inverse_ge_one_lemma
simp add: powreal_def not_less)
lemma powreal_not_zero: "a > 0 ⟹ a pow⇩ℝ x ≠ 0"
by (metis order_less_imp_not_eq powreal_gt_zero)
lemma powreal_minus:
"a pow⇩ℝ -x = inverse (a pow⇩ℝ x)"
proof (cases "a < 0")
case True
then show ?thesis
using powreal_def by force
next
case False
then have "a pow⇩ℝ (x + -x) = a pow⇩ℝ x * a pow⇩ℝ -x"
using powreal_add by presburger
then show ?thesis
using inverse_unique powreal_def powreal_zero_eq_one
by fastforce
qed
lemma powreal_minus_base_ge_one:
"a pow⇩ℝ (-x) = (inverse a) pow⇩ℝ x"
using one_le_inverse_iff powreal_def by auto
lemma powreal_inverse:
"inverse (a pow⇩ℝ x) = (inverse a) pow⇩ℝ x"
using powreal_minus powreal_minus_base_ge_one
by presburger
lemma powa_minus:"a ≥ 1 ⟹ a powa (-x) = inverse (a powa x)"
by (metis powreal_eq_powa powreal_minus)
lemma powa_mult_base:
assumes "1 ≤ a" and "1 ≤ b"
shows "(a * b) powa x = (a powa x) * (b powa x)"
proof -
obtain x' where lim_a: "(λn. a pow⇩ℚ incseq_of x n) ⇢ x'"
using LIMSEQ_powrat_incseq_of_ex1 assms(1) by blast
then have lim_a_eq: "(THE y. (λn. a pow⇩ℚ incseq_of x n) ⇢ y) = x'"
by (metis Lim_def limI)
obtain y' where lim_b: "(λn. b pow⇩ℚ incseq_of x n) ⇢ y'"
using LIMSEQ_powrat_incseq_of_ex1 assms(2) by blast
then have lim_b_eq: "(THE y. (λn. b pow⇩ℚ incseq_of x n) ⇢ y) = y'"
by (metis Lim_def limI)
have lim_ab: "(λn. (a * b) pow⇩ℚ incseq_of x n) ⇢ x' * y'"
using lim_a lim_b by (auto dest: tendsto_mult simp add: powrat_mult_base)
then have "(THE y. (λn. (a * b) pow⇩ℚ incseq_of x n) ⇢ y) = x' * y'"
by (metis Lim_def limI)
then show ?thesis
by (simp add: lim_a_eq lim_b_eq powa_def)
qed
lemma powreal_mult_base_lemma1:
"⟦ 1 ≤ a; 1 ≤ b ⟧
⟹ (a * b) pow⇩ℝ x = (a pow⇩ℝ x) * (b pow⇩ℝ x)"
by (metis mult.left_neutral mult_mono' powa_mult_base powreal_eq_powa zero_le_one)
lemma powreal_mult_base_lemma2:
assumes "1 ≤ a"
and "0 < b"
and "b < 1"
shows "(a * b) pow⇩ℝ x = (a pow⇩ℝ x) * (b pow⇩ℝ x)"
proof (cases "a * b < 1")
case True
assume ab1: "a * b < 1"
have "a * b > 0"
using assms(1) assms(2) by auto
then have inv_ab1: "1 ≤ inverse (a * b)"
using ab1 real_inverse_ge_one_lemma by blast
then have "(a * (inverse a * inverse b)) powa - x =
a powa - x * (inverse a * inverse b) powa - x"
by (simp add: assms(1) powa_mult_base)
then have "(inverse b) powa - x =
a powa - x * (inverse a * inverse b) powa - x"
using assms(1) by (simp add: mult.assoc [symmetric])
then have "(inverse a * inverse b) powa - x = a powa x * inverse b powa - x"
by (simp add: mult.assoc [symmetric] powa_add [symmetric] assms(1))
then show ?thesis
using ab1 assms powreal_def by auto
next
case False
have inv_b: "inverse b ≥ 1"
by (simp add: assms real_inverse_ge_one_lemma)
assume "¬ a * b < 1"
then have "a * b ≥ 1" by simp
then have "(a * b * inverse b) powa x = (a * b) powa x * inverse b powa x"
by (simp add: assms(2) assms(3) powa_mult_base real_inverse_ge_one_lemma)
then have "a powa x = (a * b) powa x * inverse b powa x"
using assms(2) by (auto simp add: mult.assoc)
then have "(a * b) powa x = a powa x * inverse b powa - x"
by (simp add: mult.assoc powa_add [symmetric] assms inv_b)
then show ?thesis
using False assms powreal_def by auto
qed
lemma powreal_mult_base_lemma3:
assumes "0 < a"
and "a < 1"
and "0 < b"
and "b < 1"
shows "(a * b) pow⇩ℝ x = (a pow⇩ℝ x) * (b pow⇩ℝ x)"
proof -
have "a * b < 1" using assms
by (metis less_trans mult.left_neutral mult_less_cancel_right_disj)
moreover have "(inverse a * inverse b) powa - x =
inverse a powa - x * inverse b powa - x"
by (simp add: assms powa_mult_base real_inverse_ge_one_lemma)
ultimately show ?thesis using powreal_def assms by simp
qed
lemma powreal_mult_base:
assumes "0 ≤ a" and "0 ≤ b"
shows "(a * b) pow⇩ℝ x = (a pow⇩ℝ x) * (b pow⇩ℝ x)"
proof (cases "a ≥ 1 ∧ b ≥ 1")
case True
then show ?thesis
by (simp add: powreal_mult_base_lemma1)
next
case False
then show ?thesis
using powreal_mult_base_lemma3 powreal_mult_base_lemma2 assms
by (smt (verit) mult.commute mult_minus_left powreal_def)
qed
lemma incseq_le_all: "incseq X ⟹ X ⇢ L ⟹ ∀n. X n ≤ (L::real)"
by (metis incseq_le)
lemma powa_powrat_eq:
assumes "a ≥ 1" shows "a powa (of_rat q) = a pow⇩ℚ q"
proof -
have "(λn. a pow⇩ℚ incseq_of (real_of_rat q) n) ⇢ a pow⇩ℚ q"
using powa_indep_incseq_of' assms by fastforce
then show ?thesis using powa_def
by (metis Lim_def limI)
qed
lemma realpow_powrat_eq: "a > 0 ⟹ a pow⇩ℝ (of_rat q) = a pow⇩ℚ q"
proof -
assume a1: "0 < a"
then have "¬ a < 1 ∨ 1 ≤ inverse a"
using real_inverse_ge_one_lemma by blast
then show ?thesis
using a1
by (metis inverse_inverse_eq not_le powa_powrat_eq
powrat_inverse powreal_eq_powa powreal_inverse)
qed
lemma LIMSEQ_real_root:
"⟦ X ⇢ a; m > 0 ⟧ ⟹ (λn. root m (X n)) ⇢ (root m a)"
by (metis isCont_tendsto_compose [where g="λx. root m x"] isCont_real_root)
lemma powa_powrat_lemma1:
assumes "a ≥ 1" and "p ≥ 0"
shows "(a powa x) pow⇩ℚ p = (a powa (x * of_rat p))"
proof -
obtain y where lim_a: "(λn. a pow⇩ℚ incseq_of x n) ⇢ y"
using LIMSEQ_powrat_incseq_of_ex1 assms(1) by blast
then have the_lim: "(THE y. (λn. a pow⇩ℚ incseq_of x n) ⇢ y) = y"
by (metis Lim_def limI)
then have "(λn. (a pow⇩ℚ incseq_of x n) pow⇩ℚ p) ⇢ y pow⇩ℚ p"
using LIMSEQ_powrat_base assms(1) lim_a powa_def powa_gt_zero by auto
then have lim_ap: "(λn. a pow⇩ℚ (incseq_of x n * p)) ⇢ y pow⇩ℚ p"
using assms(1) powrat_mult by auto
then have "(λn. a pow⇩ℚ incseq_of (x * real_of_rat p) n) ⇢ y pow⇩ℚ p"
proof -
have "incseq (λn. incseq_of x n * p)"
by (simp add: assms(2) incseq_SucI mult_right_mono)
moreover have "(λn. real_of_rat (incseq_of x n * p)) ⇢ x * real_of_rat p"
by (auto intro!: tendsto_mult simp add: of_rat_mult)
ultimately show ?thesis
using assms(1) lim_ap powa_indep_incseq_of' by blast
qed
then show ?thesis using powa_def
by (metis Lim_def limI the_lim)
qed
lemma powa_powrat_lemma2:
assumes "a ≥ 1" and "p < 0"
shows "(a powa x) pow⇩ℚ p = (a powa (x * of_rat p))"
proof -
have "(a powa x) pow⇩ℚ - p = a powa (x * real_of_rat (- p))"
by (simp add: assms(1) assms(2) less_imp_le powa_powrat_lemma1)
then have "inverse ((a powa x) pow⇩ℚ p) = inverse (a powa (x * real_of_rat p))"
by (simp add: assms(1) of_rat_minus powa_minus powrat_minus)
then show ?thesis by simp
qed
lemma powa_powrat_lemma:
"a ≥ 1 ⟹ (a powa x) pow⇩ℚ p = (a powa (x * of_rat p))"
by (metis linorder_not_less powa_powrat_lemma1 powa_powrat_lemma2)
lemma LIMSEQ_iff2:
fixes L :: "'a::metric_space"
shows "(X ⇢ L) = (∀m::nat>0. ∃no. ∀n≥no. dist (X n) L < inverse m)"
proof
assume "X ⇢ L"
then show "∀m>0. ∃no. ∀n≥no. dist (X n) L < inverse (real m)"
by (auto simp add: LIMSEQ_def)
next
assume assm: "∀m>0. ∃no. ∀n≥no. dist (X n) L < inverse (real m)"
{fix r
assume "(r::real) > 0"
then have " ∃no. ∀n≥no. dist (X n) L < r"
using assm
by (metis ex_inverse_of_nat_less less_trans)
}
then show "X ⇢ L"
by (simp add: metric_LIMSEQ_I)
qed
lemma LIM_def2:
"f ─a→ L = (∀m::nat>0. ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < inverse m)"
for a :: "'a::metric_space" and L :: "'b::metric_space"
proof
assume "f ─a→ L"
then show "∀m::nat>0. ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < inverse m"
by (auto simp add: LIM_def)
next
assume assm: "∀m::nat>0. ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < inverse m"
{fix r
assume r0: "(r::real) > 0"
then obtain n where "inverse (real (Suc n)) < r"
using reals_Archimedean by blast
then have "∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r"
using assm r0 by (metis order_less_trans zero_less_Suc)
}
then show "f ─a→ L"
by (simp add: metric_LIM_I)
qed
lemma powa_ge_one:
assumes "a ≥ 1"
and "x ≥ 0"
shows "a powa x ≥ 1"
proof -
obtain y where lima: "(λn. a pow⇩ℚ incseq_of x n) ⇢ y"
using LIMSEQ_powrat_incseq_of_ex1 assms(1) by blast
moreover have "incseq (λn. a pow⇩ℚ incseq_of x n)"
using assms(1) incseq_powrat_insec_of by blast
moreover have "∀n. a pow⇩ℚ incseq_of x n ≤ y"
using incseq_le_all using calculation by blast
ultimately have "1 ≤ y"
using assms LIMSEQ_incseq_of LIMSEQ_powa LIMSEQ_powrat_incseq_of_ex1
lemma_seq_point_gt_ex2 powa_zero_eq_one powrat_ge_one
by (metis less_le of_rat_0 less_eq_real_def xt1(6))
then show ?thesis
using LIMSEQ_powa LIMSEQ_unique assms(1) lima by blast
qed
lemma powreal_ge_one: "a ≥ 1 ⟹ x ≥ 0 ⟹ a pow⇩ℝ x ≥ 1"
by (simp add: powreal_def powa_ge_one)
lemma powreal_ge_one2:
"⟦ 0 < a; a < 1; x ≤ 0 ⟧ ⟹ a pow⇩ℝ x ≥ 1"
by (simp add: powa_ge_one powreal_def real_inverse_ge_one_lemma)
lemma inverse_of_real_nat_of_rat_of_nat:
"inverse (real_of_nat n) = of_rat(inverse (of_nat n))"
by (metis Ratreal_def of_rat_of_nat_eq real_inverse_code)
lemma LIMSEQ_powa_inverse_of_nat:
"a ≥ 1 ⟹ (λn. a powa inverse (real_of_nat n)) ⇢ 1"
by (simp add: inverse_of_real_nat_of_rat_of_nat powa_powrat_eq
LIMSEQ_powrat_inverse_of_nat)
lemma incseq_of_le_mono:
assumes "r ≤ s"
shows "∃N. ∀n≥N. incseq_of r n ≤ incseq_of s n"
proof -
have "r = s ∨ r < s" using assms by force
then show ?thesis
proof
assume "r = s" then show ?thesis by simp
next
assume rs: "r < s"
then obtain m where less_incseq: "r < real_of_rat (incseq_of s m)"
using LIMSEQ_incseq_of lemma_seq_point_gt_ex by blast
moreover have "∀n. real_of_rat (incseq_of r n) ≤ r"
using incseq_of_le_self by simp
ultimately have "∀n. real_of_rat (incseq_of r n) < real_of_rat (incseq_of s m)"
using le_less_trans by blast
then have incrs: "∀n. incseq_of r n ≤ incseq_of s m"
by (simp add: less_imp_le of_rat_less)
then show ?thesis
by (meson incseq_def incseq_incseq_of order_trans)
qed
qed
lemma powa_le_mono:
assumes "r ≤ s"
and "a ≥ 1"
shows "a powa r ≤ a powa s"
proof -
obtain y where "(λn. a pow⇩ℚ incseq_of s n) ⇢ y"
using LIMSEQ_powrat_incseq_of_ex1 assms(2) by blast
moreover obtain x where "(λn. a pow⇩ℚ incseq_of r n) ⇢ x"
using LIMSEQ_powrat_incseq_of_ex1 assms(2) by blast
moreover have "∃N. ∀n≥N. a pow⇩ℚ incseq_of r n ≤ a pow⇩ℚ incseq_of s n"
by (meson assms(1) assms(2) incseq_of_le_mono powrat_le_mono)
moreover have "x ≤ y"
using LIMSEQ_le calculation by blast
ultimately show ?thesis
by (metis Lim_def limI powa_def)
qed
lemma powreal_le_mono:
"⟦ r ≤ s; a ≥ 1 ⟧ ⟹ a pow⇩ℝ r ≤ a pow⇩ℝ s"
by (metis powa_le_mono powreal_eq_powa)
lemma powreal_le_anti_mono:
"⟦ r ≤ s; 0 < a; a < 1 ⟧ ⟹ a pow⇩ℝ r ≥ a pow⇩ℝ s"
by (simp add: powa_le_mono powreal_def real_inverse_ge_one_lemma)
lemma powreal_less_cancel:
"⟦ a pow⇩ℝ r < a pow⇩ℝ s; a ≥ 1 ⟧ ⟹ r < s"
by (metis less_le_not_le linorder_not_less powreal_eq_powa powreal_le_mono)
lemma powa_less_mono:
assumes "r < s" and "a > 1"
shows "a powa r < a powa s"
proof -
obtain q where "r < real_of_rat q" "real_of_rat q < s"
using assms(1) of_rat_dense by blast
moreover obtain qa where "real_of_rat q < real_of_rat qa" "real_of_rat qa < s"
using of_rat_dense calculation(2) by blast
ultimately show ?thesis using assms
by (metis (full_types) antisym less_eq_real_def less_imp_not_eq2 powa_le_mono
powa_powrat_eq powrat_inject_exp)
qed
lemma powreal_less_anti_mono:
assumes "r < s"
and "0 < a"
and "a < 1"
shows "a pow⇩ℝ r > a pow⇩ℝ s"
proof -
have "inverse a > 1"
by (simp add: assms(2, 3) one_less_inverse_iff)
moreover have "inverse a powa r < inverse a powa s"
using assms(1) powa_less_mono
using calculation by blast
ultimately show ?thesis
using powreal_eq_powa powreal_inverse powreal_le_anti_mono powreal_less_cancel
by (metis assms(2,3) le_less less_irrefl)
qed
lemma powreal_less_mono:
"⟦ r < s; a > 1 ⟧ ⟹ a pow⇩ℝ r < a pow⇩ℝ s"
by (simp add: powreal_def powa_less_mono)
lemma powa_le_cancel:
"⟦ a powa r ≤ a powa s; a > 1 ⟧ ⟹ r ≤ s"
by (metis not_le powa_less_mono)
lemma powreal_le_cancel:
"⟦ a pow⇩ℝ r ≤ a pow⇩ℝ s; a > 1 ⟧ ⟹ r ≤ s"
by (metis not_le powreal_less_mono)
lemma powreal_less_cancel_iff [simp]:
"1 < a ⟹ (a pow⇩ℝ r < a pow⇩ℝ s) = (r < s)"
by (metis less_imp_le powreal_less_cancel powreal_less_mono)
lemma powreal_le_cancel_iff [simp]:
"1 < a ⟹ (a pow⇩ℝ r ≤ a pow⇩ℝ s) = (r ≤ s)"
by (simp add: linorder_not_less [symmetric])
lemma powreal_inject_exp1 [simp]:
"1 < a ⟹ (a pow⇩ℝ r = a pow⇩ℝ s) = (s = r)"
by (metis antisym_conv3 less_irrefl powreal_less_mono)
lemma powreal_eq_one_iff [simp]:
"a pow⇩ℝ x = 1 ⟷ x = 0" if "a > 1"
using powreal_inject_exp1 that by fastforce
lemma powreal_inject_base_less_one [simp]:
"0 < a ⟹ a < 1 ⟹ (a pow⇩ℝ r = a pow⇩ℝ s) = (s = r)"
by (metis linorder_neq_iff order_less_imp_not_eq2 powreal_less_anti_mono)
lemma powreal_inject [simp]:
"0 < a ⟹ a ≠ 1 ⟹ (a pow⇩ℝ r = a pow⇩ℝ s) = (s = r)"
using powreal_inject_base_less_one by fastforce
lemma powreal_gt_one: "a > 1 ⟹ x > 0 ⟹ a pow⇩ℝ x > 1"
by (metis less_eq_real_def powa_less_mono powa_zero_eq_one powreal_eq_powa)
lemma isCont_powa_exponent_at_zero:
assumes "a > 1" shows "isCont (λx. a powa x) 0"
proof -
{fix m
assume m0: "(m::nat) > 0"
have lim1: "(λn. a powa inverse (real n)) ⇢ 1"
by (simp add: LIMSEQ_powa_inverse_of_nat assms less_imp_le)
then have "∃no. ∀n≥no. ¦a powa inverse (real n) - 1¦ < inverse (real m)"
using lim1 LIMSEQ_iff2 dist_real_def m0 by metis
then obtain "no"
where pow1: "∀n≥no. ¦a powa inverse (real n) - 1¦ < inverse (real m)"
by blast
have lim2: "(λx. inverse (a powa inverse (real x))) ⇢ 1"
using tendsto_inverse lim1 by fastforce
then have "∃k. ∀n≥k. ¦inverse (a powa inverse (real n)) - 1¦ < inverse (real m)"
using LIMSEQ_iff2 dist_real_def m0 by metis
then obtain "k"
where pow2: "∀n≥k. ¦inverse (a powa inverse (real n)) - 1¦ < inverse (real m)"
by blast
have "∃s>0. ∀x. x ≠ 0 ∧ ¦x¦ < s ⟶ ¦(a powa x) - 1¦ < inverse (real m)"
proof -
let ?d = "min (inverse (Suc no)) (inverse (Suc k))"
{fix x
assume "abs x < ?d"
then have x_bounds: "- inverse (of_nat(Suc k)) < x" "x < inverse (of_nat(Suc no))"
by linarith+
then have "a powa - inverse (of_nat (Suc k)) < a powa x"
using assms powa_less_mono by blast
moreover have "- inverse (real m) < a powa - inverse (real (Suc k)) - 1"
using assms pow2 powa_minus
by (metis minus_diff_eq neg_less_iff_less abs_less_iff lessI less_imp_le)
ultimately have lo: "- inverse(real m) < a powa x - 1"
by linarith
have "a powa x < a powa inverse (of_nat(Suc no))"
using assms powa_less_mono x_bounds(2) by blast
moreover have "a powa inverse (real (Suc no)) - 1 < inverse (real m)"
using assms pow1 by (metis less_imp_le abs_less_iff lessI)
ultimately have "a powa x - 1 < inverse(real m)"
by linarith
then have "abs (a powa x - 1) < inverse(real m)"
using lo by linarith}
then show ?thesis
by (metis inverse_positive_iff_positive min_less_iff_conj of_nat_0_less_iff zero_less_Suc)
qed}
then have "∀m>0. ∃s>0. ∀x. x ≠ 0 ∧ ¦x¦ < s ⟶ ¦a powa x - 1¦ < inverse (real m)"
by blast
then show ?thesis
by (auto simp add: assms isCont_def LIM_def2 dist_real_def less_imp_le)
qed
lemma LIM_powa_exponent_at_zero: "1 < a ⟹ (λh. a powa h) ─0→ 1"
by (metis isCont_def isCont_powa_exponent_at_zero less_eq_real_def powa_zero_eq_one)
lemma isCont_powa_exponent_gt_one:
assumes "a > 1"
shows "isCont (λx. a powa x) x"
proof -
have "(λh. a powa x * a powa h) ─0→ a powa x"
using LIM_powa_exponent_at_zero assms tendsto_mult_left by fastforce
then have "(λh. a powa (x + h)) ─0→ a powa x"
using assms powa_add by auto
then have "(powa) a ─x→ a powa x"
using LIM_offset_zero_cancel by blast
then show ?thesis
using isCont_def by blast
qed
lemma isCont_powreal_exponent_gt_one:
"a > 1 ⟹ isCont (λx. a pow⇩ℝ x) x"
by (metis ext isCont_powa_exponent_gt_one less_eq_real_def powreal_eq_powa)
lemma isCont_powreal_exponent_less_one:
assumes "0 < a"
and "a < 1"
shows "isCont (λx. a pow⇩ℝ x) x"
proof -
have "1 < inverse a"
by (simp add: assms one_less_inverse)
then have "isCont ((pow⇩ℝ) (inverse a)) x"
by (simp add: isCont_powreal_exponent_gt_one)
then have "isCont (λx. inverse (inverse a pow⇩ℝ x)) x"
using assms(1) continuous_at_within_inverse powreal_not_zero by fastforce
then show ?thesis
using assms(1) powreal_inverse by auto
qed
lemma isCont_powreal_exponent:
assumes a_gt_0: "0 < a" shows "isCont (λx. a pow⇩ℝ x) x"
proof cases
assume "a > 1" then show ?thesis
using isCont_powreal_exponent_gt_one by blast
next
assume "¬ a > 1"
then have "a < 1 ∨ a = 1" by auto
then show ?thesis
proof
assume "a < 1" then show ?thesis
using a_gt_0 isCont_powreal_exponent_less_one by blast
next
assume "a =1" then show ?thesis by simp
qed
qed
lemma real_of_rat_abs:
"real_of_rat(abs a) = abs(of_rat a)"
by (simp add: abs_if of_rat_minus)
lemma isCont_powrat_exponent:
assumes "0 < a" shows "isCont (λx. a pow⇩ℚ x) x"
proof -
have isCont_of_rat: "isCont real_of_rat x" using isCont_def LIM_def dist_real_def
by (metis dist_commute of_rat_diff rat_dist_def real_of_rat_abs)
have "isCont ((pow⇩ℝ) a) (real_of_rat x)" using assms
by (simp add: isCont_powreal_exponent)
then have "isCont (λx. a pow⇩ℝ real_of_rat x) x" using isCont_of_rat
using isCont_o2 by blast
then show ?thesis using realpow_powrat_eq assms by simp
qed
lemma LIMSEQ_powrat_exponent:
"⟦ X ⇢ x; a > 0 ⟧ ⟹ (λn. a pow⇩ℚ (X n)) ⇢ a pow⇩ℚ x"
by (metis isCont_tendsto_compose isCont_powrat_exponent)
lemma powa_mult:
assumes "1 ≤ a" and "0 ≤ x"
shows "(a powa x) powa y = a powa (x * y)"
proof (cases)
assume "a ≠ 1"
then have a_gt_1: "a > 1" using assms(1) by simp
have "a powa x ≥ 1" using assms powa_ge_one by blast
then have lim1: "(λn. a powa (x * real_of_rat (incseq_of y n))) ⇢ (a powa x) powa y"
using LIMSEQ_powa [of "a powa x" y] powa_powrat_lemma assms(1) by simp
have "isCont ((powa) a) (x * y)" using isCont_powa_exponent_gt_one a_gt_1 by blast
moreover have "(λn. x * real_of_rat (incseq_of y n)) ⇢ x * y"
by (simp add: tendsto_mult_left)
ultimately have "(λn. a powa (x * real_of_rat (incseq_of y n))) ⇢ a powa (x * y)"
using isCont_tendsto_compose by blast
then show ?thesis
using LIMSEQ_unique lim1 by blast
next
assume "¬ a ≠ 1"
then show ?thesis
by auto
qed
lemma powreal_mult1:
"⟦ 1 ≤ a; 0 ≤ x ⟧ ⟹ (a pow⇩ℝ x) pow⇩ℝ y = a pow⇩ℝ (x * y)"
by (metis powa_mult powreal_eq_powa powreal_ge_one)
lemma powreal_mult2:
assumes "0 < a" and "a < 1" and "0 ≤ x"
shows "(a pow⇩ℝ x) pow⇩ℝ y = a pow⇩ℝ (x * y)"
proof -
have "1 ≤ inverse a" using assms using real_inverse_ge_one_lemma by simp
then have "(inverse a pow⇩ℝ x) pow⇩ℝ y = inverse a pow⇩ℝ (x * y)"
using powreal_mult1 assms(3) by blast
then have "inverse((inverse a pow⇩ℝ x) pow⇩ℝ y) = a pow⇩ℝ (x * y)"
by (simp add: assms(1) powreal_inverse)
then show ?thesis
using assms(1) powreal_gt_zero powreal_inverse by auto
qed
lemma powreal_mult3:
"⟦ 0 < a; 0 ≤ x ⟧ ⟹ (a pow⇩ℝ x) pow⇩ℝ y = a pow⇩ℝ (x * y)"
by (metis linorder_not_less powreal_mult1 powreal_mult2)
lemma powreal_mult4:
assumes a0: "0 < a" and x0: "x ≤ 0"
shows "(a pow⇩ℝ x) pow⇩ℝ y = a pow⇩ℝ (x * y)"
proof -
have minux0: "-x ≥ 0" using x0 by simp
then have "(a pow⇩ℝ -x) pow⇩ℝ y = a pow⇩ℝ (-x * y)"
using powreal_mult3 a0 by simp
then have "inverse (a pow⇩ℝ x) pow⇩ℝ y = inverse (a pow⇩ℝ (x * y))"
by (simp add: powreal_minus)
then have "inverse ((a pow⇩ℝ x) pow⇩ℝ y) = inverse (a pow⇩ℝ (x * y))"
by (simp add: a0 powreal_gt_zero powreal_inverse)
then show ?thesis
using inverse_eq_iff_eq by blast
qed
lemma powreal_mult:
"(a pow⇩ℝ x) pow⇩ℝ y = a pow⇩ℝ (x * y)"
by (smt (verit, best) powreal_def powreal_mult3 powreal_mult4)
lemma powreal_divide:
"⟦ 0 ≤ a; 0 ≤ b ⟧ ⟹ (a/b) pow⇩ℝ x = (a pow⇩ℝ x) / (b pow⇩ℝ x)"
by (simp add: divide_inverse powreal_inverse powreal_mult_base)
lemma powreal_divide2:
"0 ≤ a ⟹ a pow⇩ℝ (x - y) = (a pow⇩ℝ x) / (a pow⇩ℝ y)"
proof -
assume a1: "0 ≤ a"
have f2: "∀x0. - (x0::real) = - 1 * x0"
by auto
have "x - y = x + - 1 * y"
by auto
then show ?thesis
using f2 a1 by (metis field_class.field_divide_inverse powreal_add powreal_minus)
qed
lemma powreal_less_mono_base:
assumes r0: "r > 0" and a0: "0 < a" and ab: "a < b"
shows "a pow⇩ℝ r < b pow⇩ℝ r"
proof -
have "b/a > 1" using ab a0 by simp
then have "(b/a) pow⇩ℝ r > 1"
using powreal_gt_one r0 by simp
then have "b pow⇩ℝ r / a pow⇩ℝ r > 1"
using ab a0 powreal_divide by simp
also have "a pow⇩ℝ r > 0"
by (simp add: a0 powreal_gt_zero)
ultimately show ?thesis
using less_divide_eq_1_pos by blast
qed
lemma powreal_less_antimono_base:
assumes "r < 0" and "0 < a" and "a < b"
shows "a pow⇩ℝ r > b pow⇩ℝ r"
proof -
have "0 < -r" using assms(1) by simp
then have "a pow⇩ℝ - r < b pow⇩ℝ - r"
using assms(2) assms(3) powreal_less_mono_base by blast
then show ?thesis
using assms(2) assms(3) powreal_gt_zero powreal_minus by auto
qed
lemma powa_power_eq:
assumes "a ≥ 1" shows "a powa (of_nat n) = a ^ n"
proof -
have "incseq (λm. rat_of_nat n)" by simp
moreover have "(λna. real_of_rat (rat_of_nat n)) ⇢ real n" by simp
moreover have "(λna. a pow⇩ℚ rat_of_nat n) ⇢ a ^ n"
using powrat_power_eq assms by auto
ultimately have "(λna. a pow⇩ℚ incseq_of (real n) na) ⇢ a ^ n"
using powa_indep_incseq_of' assms by blast
then show ?thesis
by (metis Lim_def limI powa_def)
qed
lemma powreal_power_eq:
"a > 0 ⟹ a pow⇩ℝ (of_nat n) = a ^ n"
unfolding powreal_def
by (simp add: powa_minus powa_power_eq power_inverse real_inverse_ge_one_lemma)
lemma powreal_power_eq2:
"0 ≤ a ⟹ 0 < n ⟹ a ^ n = (if a = 0 then 0 else a pow⇩ℝ (real n))"
by (auto simp add: powreal_power_eq)
lemma powreal_mult_power: "a > 0 ⟹ a pow⇩ℝ (n * x) = (a pow⇩ℝ x) ^ n"
by (metis mult.commute powreal_gt_zero powreal_mult powreal_power_eq)
lemma powreal_int:
assumes "x > 0"
shows "x pow⇩ℝ i = (if i ≥ 0 then x ^ nat i else 1 / x ^ nat (-i))"
proof cases
assume "i < 0"
have r: "x pow⇩ℝ i = 1 / x pow⇩ℝ (-i)" by (simp add: assms powreal_minus divide_inverse)
show ?thesis using ‹i < 0› ‹x > 0› by (simp add: r field_simps powreal_power_eq [symmetric])
qed (simp add: assms powreal_power_eq[symmetric])
lemma powreal_numeral: "0 ≤ x ⟹ x pow⇩ℝ numeral n = x^numeral n"
using powreal_power_eq [of x "numeral n"] powreal_def
by fastforce
lemma root_powreal_inverse:
assumes "0 < n" and "0 ≤ x"
shows "root n x = x pow⇩ℝ (1/n)"
proof -
have "root n x = x pow⇩ℝ real_of_rat (inverse (rat_of_nat n))"
using assms real_root_eq_powrat_inverse realpow_powrat_eq [symmetric] powreal_def
by simp
then show ?thesis
by (metis inverse_eq_divide of_rat_inverse of_rat_of_nat_eq)
qed
lemma powreal_inverse_of_nat_gt_one:
"⟦ 1 < a; n ≠ 0⟧ ⟹ a pow⇩ℝ (inverse (of_nat n)) > 1"
by (metis inverse_positive_iff_positive neq0_conv of_nat_0_less_iff powreal_gt_one)
end