# Theory Log

```(*  Title:      RealPower/Log.thy
Authors:    Jacques D. Fleuriot
University of Edinburgh, 2021
*)

section‹Real Logarithms (Redefined)›

theory Log
imports RealPower
begin

text‹We can now directly define real logarithm of @{term x} to base @{term a}.›

definition
Log  :: "[real,real] ⇒ real" where
"Log a x = (THE y. a pow⇩ℝ y = x)"

lemma IVT_simple:
"⟦f (a::real) ≤ (y::real); y ≤ f b; a ≤ b;
∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x⟧
⟹ ∃x. f x = y"
by (frule IVT [of f]) auto

lemma inj_on_powreal:
"0 < a ⟹ a ≠ 1 ⟹ inj_on (λx. a pow⇩ℝ x) UNIV"

lemma LIMSEQ_powreal_minus_nat:
"a > 1 ⟹ (λn. a pow⇩ℝ (-real n)) ⇢ 0"
LIMSEQ_inverse_realpow_zero)

lemma LIMSEQ_less_Ex:
"⟦ X ⇢ (x::real); x < y ⟧ ⟹ ∃n. X n < y"
by (meson LIMSEQ_le_const not_less)

lemma powreal_IVT_upper_lemma:
assumes "a > (1::real)" and "x > 0"
shows "∃n::nat. a pow⇩ℝ (-real n) < x"
proof -
have "(λn. a pow⇩ℝ - real n) ⇢ 0"
then show ?thesis
using LIMSEQ_less_Ex assms(2) by blast
qed

lemma powreal_IVT_lower_lemma:
assumes "a > (1::real)"
and "x > 0"
shows "∃n::nat. x < a pow⇩ℝ (real n)"
proof -
have invx0: "0 < inverse x"
then have "∃n. a pow⇩ℝ - real n < inverse x"
using assms(1) powreal_IVT_upper_lemma by blast
then show ?thesis
using assms(1)
by (auto dest: inverse_less_imp_less
qed

lemma powreal_surj:
assumes "a > 1"
and "x > 0"
shows "∃y. a pow⇩ℝ y = x"
proof -
obtain n where "a pow⇩ℝ - real n < x"
using assms powreal_IVT_upper_lemma by blast
moreover obtain na where "x < a pow⇩ℝ real na"
using assms powreal_IVT_lower_lemma by blast
moreover have "∀x. - real n ≤ x ∧ x ≤ real na ⟶ isCont ((pow⇩ℝ) a) x"
using assms(1) isCont_powreal_exponent_gt_one by blast
ultimately show ?thesis
using IVT_simple [of _ "-real n" _ "real na"] by force
qed

lemma powreal_surj2:
"⟦ 0 < a; a < 1; x > 0 ⟧ ⟹ ∃y. a pow⇩ℝ y = x"
using powreal_minus_base_ge_one powreal_surj real_inverse_gt_one_lemma
by blast

lemma powreal_ex1_eq:
assumes "a > 0"
and "a ≠ 1"
and "x > 0"
shows "∃! y. a pow⇩ℝ y = x"
proof (cases "a < 1")
case True
then show ?thesis
using assms powreal_inject powreal_surj2 by blast
next
case False
then show ?thesis
using assms(2) assms(3) powreal_surj by auto
qed

lemma powreal_Log_cancel [simp]:
"⟦ a > 0; a ≠ 1; x > 0 ⟧ ⟹ a pow⇩ℝ (Log a x) = x"
by (auto intro: the1I2 [OF powreal_ex1_eq] simp add: Log_def)

lemma Log_powreal_cancel [simp]:
"⟦ 0 < a; a ≠ 1 ⟧ ⟹ Log a (a pow⇩ℝ y) = y"
by (metis powreal_ex1_eq powreal_gt_zero powreal_Log_cancel)

lemma Log_mult:
"⟦ 0 < a; a ≠ 1; 0 < x; 0 < y ⟧
⟹ Log a (x * y) = Log a x + Log a y"

lemma Log_one [simp]: "⟦ 0 < a; a ≠ 1 ⟧ ⟹ Log a 1 = 0"
by (metis Log_powreal_cancel powreal_zero_eq_one)

lemma Log_eq_one [simp]: "⟦ 0 < a; a ≠ 1 ⟧ ⟹ Log a a = 1"
using powreal_inject by fastforce

lemma Log_inverse:
"⟦ a > 0; a ≠ 1; x > 0 ⟧ ⟹ Log a (inverse x) = - Log a x"
by (metis Log_powreal_cancel powreal_Log_cancel powreal_minus)

lemma Log_divide:
"⟦ 0 < a; a ≠ 1; 0 < x; 0 < y ⟧
⟹ Log a (x/y) = Log a x - Log a y"
by (metis Log_inverse Log_mult divide_real_def
inverse_positive_iff_positive minus_real_def)

lemma Log_less_cancel_iff [simp]:
assumes "1 < a"
and "0 < x"
and "0 < y"
shows "(Log a x < Log a y) = (x < y)"
proof
assume "Log a x < Log a y"
then show "x < y" using powreal_Log_cancel assms powreal_less_cancel_iff
by (metis less_irrefl real_inverse_bet_one_one_lemma
inverse_positive_iff_positive)
next
assume "x < y"
then show "Log a x < Log a y"
using assms(1) assms(2) powreal_less_cancel_iff by fastforce
qed

lemma Log_inj: assumes "1 < b" shows "inj_on (Log b) {0 <..}"
proof (rule inj_onI, simp)
fix x y assume pos: "0 < x" "0 < y" and *: "Log b x = Log b y"
show "x = y"
proof (cases rule: linorder_cases)
assume "x < y" hence "Log b x < Log b y"
using Log_less_cancel_iff[OF ‹1 < b›] pos by simp
thus ?thesis using * by simp
next
assume "y < x" hence "Log b y < Log b x"
using Log_less_cancel_iff[OF ‹1 < b›] pos by simp
thus ?thesis using * by simp
qed simp
qed

lemma Log_le_cancel_iff [simp]:
"⟦ 1 < a; 0 < x; 0 < y ⟧ ⟹ (Log a x ≤ Log a y) = (x ≤ y)"

lemma zero_less_Log_cancel_iff [simp]:
"1 < a ⟹ 0 < x ⟹ 0 < Log a x ⟷ 1 < x"
using Log_less_cancel_iff[of a 1 x] by simp

lemma zero_le_Log_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ 0 ≤ Log a x ⟷ 1 ≤ x"
using Log_le_cancel_iff[of a 1 x] by simp

lemma Log_less_zero_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ Log a x < 0 ⟷ x < 1"
using Log_less_cancel_iff[of a x 1] by simp

lemma Log_le_zero_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ Log a x ≤ 0 ⟷ x ≤ 1"
using Log_le_cancel_iff[of a x 1] by simp

lemma one_less_Log_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ 1 < Log a x ⟷ a < x"
using Log_less_cancel_iff[of a a x] by simp

lemma one_le_Log_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ 1 ≤ Log a x ⟷ a ≤ x"
using Log_le_cancel_iff[of a a x] by simp

lemma Log_less_one_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ Log a x < 1 ⟷ x < a"
using Log_less_cancel_iff[of a x a] by simp

lemma Log_le_one_cancel_iff[simp]:
"1 < a ⟹ 0 < x ⟹ Log a x ≤ 1 ⟷ x ≤ a"
using Log_le_cancel_iff[of a x a] by simp

lemma Log_powreal:
assumes "0 < x"
and "1 < b"
and "b ≠ 1"
shows "Log b (x pow⇩ℝ y) = y * Log b x"
proof -
have "b pow⇩ℝ (Log b x * y) = x pow⇩ℝ y"
using assms powreal_mult [symmetric] by simp
moreover have "0 < x pow⇩ℝ y"
ultimately have "b pow⇩ℝ (y * Log b x) = b pow⇩ℝ Log b (x pow⇩ℝ y)"
using powreal_Log_cancel assms powreal_Log_cancel
then show ?thesis
using assms(2) powreal_inject_exp1 by blast
qed

lemma Log_nat_power:
assumes "0 < x"
and "1 < b" and "b ≠ 1"
shows " Log b (x ^ n) = real n * Log b x"
proof -
have "Log b (x pow⇩ℝ real n) = real n * Log b x"