## Stream: maths

### Topic: log (a ^ n) = n * log a in mathlib?

#### Donald Sebastian Leung (Feb 25 2020 at 11:55):

I would like to rewrite based on log (a ^ n) = n * log a which should be a well-known log identity from high school; however, I can't seem to find it even after searching through the entire analysis.complex.exponential in mathlib. Is it not in mathlib yet or am I just not looking hard enough?

#### Mario Carneiro (Feb 25 2020 at 12:04):

I think you found a hole. For cpow and the complex log, it is more or less true by definition, but there is an off by 2 pi i problem

#### Mario Carneiro (Feb 25 2020 at 12:04):

The real number version follows from that

#### Kevin Buzzard (Feb 25 2020 at 12:32):

It would not surprise me if this were false for complex a, perhaps this is why it's not there

#### Donald Sebastian Leung (Feb 25 2020 at 13:32):

Kevin Buzzard said:

It would not surprise me if this were false for complex a, perhaps this is why it's not there

Interesting ...
Mario Carneiro said:

I think you found a hole. For cpow and the complex log, it is more or less true by definition, but there is an off by 2 pi i problem

I see, I guess I will prove it by induction on n then

#### Kevin Buzzard (Feb 25 2020 at 13:41):

For induction you'll need log(ab)=log(a)+log(b) which might also be false for complex numbers.

#### Donald Sebastian Leung (Feb 25 2020 at 13:43):

Kevin Buzzard said:

For induction you'll need log(ab)=log(a)+log(b) which might also be false for complex numbers.

Is that result (for a b : ℝ) in mathlib?

#### Kevin Buzzard (Feb 25 2020 at 13:44):

aah but log_mul does indeed exist for reals :-)

#### Mario Carneiro (Feb 25 2020 at 22:57):

You shouldn't prove this by induction. For a theorem like this it generalizes to positive reals at least

#### Jalex Stark (Mar 03 2020 at 07:21):

import tactic
import analysis.complex.exponential

lemma log_pow_nat (x : ℝ ) (n : ℕ ) (hx : x > 0) : real.log (x^n) = n * real.log x :=
begin
induction n with d hd,
simp only [pow_zero, real.log_one, nat.nat_zero_eq_zero, nat.cast_zero, zero_mul],
rw pow_succ,
rw real.log_mul,
swap, assumption,
swap, exact pow_pos hx d,
ring,
rw mul_comm, refl,
end

lemma puzzle_2 (a b c : ℝ) (h : c * a = c * b) (hc : c ≠ 0) : (a = b) :=
begin
have q := inv_mul_cancel hc,
apply_fun (λ x, c⁻¹ * x) at h,
repeat {rw ← mul_assoc at h,rw q at h,},
revert h, simp only [one_mul, imp_self],
end

lemma puzzle_3 (x : ℝ ) (h: x ≠ 0): 1/x * x = 1 :=
begin
rw one_div_eq_inv, revert h,
exact inv_mul_cancel,
end

lemma puzzle_4 (x : ℝ ) : x = x^(1:ℝ ) :=
begin
simp only [real.rpow_one],
end

lemma pow_mul_nat (b x : ℝ) (n : ℕ ) (hb : b > 0) : b^(x * n) = (b^x)^n :=
begin
induction n with d hd,
norm_num,
have t : x * ↑(d + 1) = x * ↑d + x := by ring, rw t,
rw hd,
rw mul_comm,
exact hb,
end

lemma puzzle_5 (x : ℝ ) (n : ℕ ) (hn : n≠ 0) (hx : x > 0) : (x ^ ((1 : ℝ) / n))^n = x :=
begin
rw ←  pow_mul_nat _ _ n,
simp only [one_div_eq_inv],
rw inv_mul_cancel,
simp only [real.rpow_one],
norm_cast, exact hn, exact hx,
end

lemma puzzle_6 (a n : ℝ) (hn:n ≠ 0) :(a = n * (1 / n * a)) :=
begin
have key := puzzle_3 n hn,
rw one_div_eq_inv,
rw ← mul_assoc,
rw mul_inv_cancel,
simp only [one_mul],
exact hn,
end

lemma log_pow_nat_inv (x : ℝ ) (n : ℕ ) (hn : n ≠ 0) (hx : x > 0) : real.log (x^((1 : ℝ)  / n)) = (1/n) * real.log x :=
begin
have hn_ : ( (n:ℝ) ≠ 0) := by norm_cast; exact hn,
set x_inv := x ^ ((1 : ℝ) / n),
set a := real.log x_inv,
set b := real.log x,
have q1 : b = real.log (x ^ ( (1:ℝ ) / n * n)),
rw puzzle_3,
suffices q1a: x = x^(1:ℝ ), rw ←  q1a,
exact puzzle_4 x,
exact hn_,
apply puzzle_2 _ _ n _ , simp [hn],
have q := log_pow_nat (x_inv) n _,
swap, exact real.rpow_pos_of_pos hx (1 / ↑n),
rw ← q,
have q2 := puzzle_5 x n hn,
rw q2,
apply puzzle_6 b n,
exact hn_, exact hx,
end

theorem log_pow_nat_pair (x : ℝ ) (a b : ℕ ) (ha : a ≠ 0) (hb : b≠ 0) (hx : x > 0) : real.log (x^( (a : ℝ)  / b )) = (a : ℝ)  / b  * real.log x :=
begin
have q1 : (a : ℝ) / b = (1 / b) * (a:ℝ ) := by ring,
rw q1, rw pow_mul_nat x _ a,
rw [log_pow_nat, log_pow_nat_inv],
ring,
repeat {assumption},
exact real.rpow_pos_of_pos hx (1 / ↑b),
end


#### Johan Commelin (Mar 03 2020 at 07:56):

Note that puzzle 3 is false if x = 0.

#### Johan Commelin (Mar 03 2020 at 07:56):

Some of these puzzles might be solvable by library_search

#### Johan Commelin (Mar 03 2020 at 07:57):

@Jalex Stark We know that continuous functions are determined by their values on dense subsets. But I don't know the theorem name from the top of my head.

#### Jalex Stark (Mar 03 2020 at 07:57):

just finished clearing the sorries, indeed library_search and squeeze_simp were useful

#### Kevin Buzzard (Mar 03 2020 at 08:02):

In puzzle 3 you can probably just write exact inv_mul_cancel h after the rewrite. revert hardly ever gets used, in my experience

#### Jalex Stark (Mar 03 2020 at 08:03):

ah that makes sense. I think revert was what I needed for squeeze_simp to give me a useful response

#### Jalex Stark (Mar 03 2020 at 08:04):

Some form of this theorem should end up in mathlib, right? Does that mean I should make a pull request or something?

#### Mario Carneiro (Mar 03 2020 at 08:06):

Sure. Note however that mathlib has a style guide, and a lot of cleanup would be needed to get that proof mathlib ready

#### Jalex Stark (Mar 03 2020 at 08:07):

Where do i find the style guide?

#### Mario Carneiro (Mar 03 2020 at 08:07):

https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/style.md

#### Mario Carneiro (Mar 03 2020 at 08:08):

You can also just browse mathlib sources to get a feel for the style

#### Mario Carneiro (Mar 03 2020 at 08:14):

Here's a restyling of log_pow_nat_inv. I probably haven't got the brackets quite right because I wrote this without lean, but the two exacts at the end indicate that something doesn't add up

lemma log_pow_nat_inv (x : ℝ) (n : ℕ) (hn : n ≠ 0) (hx : x > 0) :
real.log (x ^ ((1 : ℝ) / n)) = (1 / n) * real.log x :=
begin
have hn_ : (n : ℝ) ≠ 0, {norm_cast, exact hn},
set x_inv := x ^ ((1 : ℝ) / n),
set a := real.log x_inv,
set b := real.log x,
have q1 : b = real.log (x ^ ((1 : ℝ) / n * n)),
{ rw puzzle_3,
suffices q1a: x = x ^ (1 : ℝ), rw ← q1a,
{ exact puzzle_4 x },
exact hn_ },
apply puzzle_2 _ _ n _, simp [hn],
have q := log_pow_nat (x_inv) n _,
swap, exact real.rpow_pos_of_pos hx (1 / ↑n),
rw ← q,
rw puzzle_5 x n hn,
apply puzzle_6 b n,
exact hn_, exact hx,
end


#### Jalex Stark (Mar 03 2020 at 08:20):

I think you did in fact get the brackets right, it just compiles for me

#### Mario Carneiro (Mar 03 2020 at 08:20):

The question isn't whether it compiles, it is whether there are ever multiple goals in flight

#### Johan Commelin (Mar 03 2020 at 08:20):

@Jalex Stark Have you considered applying exp_injective?

#### Mario Carneiro (Mar 03 2020 at 08:21):

The point of the brackets is to organize the goals so that the structure of the proof is clearer

#### Jalex Stark (Mar 03 2020 at 08:22):

@Johan Commelin
that sounds like the kind of thing that would pull a lot of weight but I don't know where to apply it

#### Jalex Stark (Mar 03 2020 at 08:22):

@Mario Carneiro oh i see

#### Johan Commelin (Mar 03 2020 at 08:22):

Start your proof with apply exp_injective

which proof?

#### Jalex Stark (Mar 03 2020 at 08:24):

also i don't know where exp_injective lives, right now Im just trying to find it by typing it and pressing ctrl+space

#### Johan Commelin (Mar 03 2020 at 08:24):

https://github.com/leanprover-community/mathlib/blob/b42e5687d8b45e47de69e64e944637a6a7b03e1c/src/data/complex/exponential.lean#L879

#### Johan Commelin (Mar 03 2020 at 08:25):

In VScode, there is also the magnifying glass on the left. That might help as well.

#### Johan Commelin (Mar 03 2020 at 08:25):

But I assume that you've imported analysis.complex.exponential?

#### Johan Commelin (Mar 03 2020 at 08:26):

@Jalex Stark What's the final statement that you want to prove?

#### Johan Commelin (Mar 03 2020 at 08:26):

I guess something like

lemma log_pow (x : ℝ) (n : ℝ) (hx : 0 < x) :
real.log (x ^ n) = n * real.log x := sorry


yes

#### Johan Commelin (Mar 03 2020 at 08:28):

So I would start that proof immediately with apply exp_injective

#### Mario Carneiro (Mar 03 2020 at 08:28):

If you apply exp_injective, then the rhs is x ^ n in the reals by definition

#### Johan Commelin (Mar 03 2020 at 08:28):

And the lhs is equal to that by exp_log hx

okay

#### Jalex Stark (Mar 03 2020 at 08:29):

i have import analysis.complex.exponential at the top of my file

#### Johan Commelin (Mar 03 2020 at 08:29):

It's weird that this lemma isn't in mathlib yet.

#### Jalex Stark (Mar 03 2020 at 08:29):

unknown identifier 'exp_injective'

#### Johan Commelin (Mar 03 2020 at 08:29):

real.exp_injective?

that works

#### Mario Carneiro (Mar 03 2020 at 08:29):

I think the proof is as simple as rw [rpow_def_of_pos, log_exp]

#### Johan Commelin (Mar 03 2020 at 08:30):

Aha, then you don't even need exp_injective (-;

#### Jalex Stark (Mar 03 2020 at 08:30):

woah so if you have a theorem that f_injective, then apply f_injective is the thing that applies f to both sides of an equation

#### Johan Commelin (Mar 03 2020 at 08:31):

Which is just because of the general way apply works.
hf : injective f is really just a function that turns f x = f y into a proof that x = y.

#### Jalex Stark (Mar 03 2020 at 08:32):

cool i have spent a lot of time finding circuitous ways to apply f to both sides of an equation

#### Johan Commelin (Mar 03 2020 at 08:32):

So if you apply hf, then Lean says, okay, you need to prove x = y, but by hf it suffices to give me a proof of f x = f y

#### Johan Commelin (Mar 03 2020 at 08:32):

If you have a hypothesis h : x = y, and you want h' : f x = f y, then you should use congr_arg f h.

#### Mario Carneiro (Mar 03 2020 at 08:33):

or congr' 1

#### Jalex Stark (Mar 03 2020 at 08:33):

so should the code block

#### Jalex Stark (Mar 03 2020 at 08:33):

lemma log_pow (x : ℝ) (n : ℝ) (hx : 0 < x) :
real.log (x ^ n) = n * real.log x := begin
rw [real.rpow_def_of_pos, real.log_exp],
rw mul_comm, exact hx,
end


go into mathlib?

#### Johan Commelin (Mar 03 2020 at 08:34):

Yes, more or less

#### Mario Carneiro (Mar 03 2020 at 08:34):

lemma log_pow (x : ℝ) (n : ℝ) (hx : 0 < x) : real.log (x ^ n) = n * real.log x :=
by rw [real.rpow_def_of_pos hx, real.log_exp, mul_comm]


#### Johan Commelin (Mar 03 2020 at 08:34):

I would change n to y, put begin on a new line, and maybe turn the statement into real.log x * y to preserve the order of x and y and golf the proof.

#### Johan Commelin (Mar 03 2020 at 08:35):

@Mario Carneiro Do you prefer the version with or without mul_comm?

#### Mario Carneiro (Mar 03 2020 at 08:35):

they are both conceivably useful, but for consistency it's probably best to have the y on the right

lemma log_pow {x : ℝ} (y : ℝ) (hx : 0 < x) : real.log (x ^ y) = real.log x * y :=
by rw [real.rpow_def_of_pos hx, real.log_exp]


#### Johan Commelin (Mar 03 2020 at 08:36):

Also, maybe the name should be log_pow_of_pos?

#### Mario Carneiro (Mar 03 2020 at 08:36):

the real. is not necessary because this will be in the real namespace

#### Mario Carneiro (Mar 03 2020 at 08:37):

Is there a log_pow_of_neg?

#### Johan Commelin (Mar 03 2020 at 08:37):

It's probably bananas

#### Mario Carneiro (Mar 03 2020 at 08:37):

If not, I wouldn't bother

#### Johan Commelin (Mar 03 2020 at 08:37):

We have very bad powers of negative numbers

#### Mario Carneiro (Mar 03 2020 at 08:38):

I think when it comes to real.log you should just assume the argument is always positive

#### Johan Commelin (Mar 03 2020 at 08:38):

Which can happen, if x < 0 and y is an even natural number...

#### Mario Carneiro (Mar 03 2020 at 08:39):

I don't think rpow will give you that though

#### Johan Commelin (Mar 03 2020 at 08:39):

But of course the real.log x on the right would fail.

#### Johan Commelin (Mar 03 2020 at 08:39):

(-1 : ℝ) ^ (1/3 : ℝ) also doesn't seem to be what I would hope.

#### Mario Carneiro (Mar 03 2020 at 08:40):

What I would hope is a complex number

#### Mario Carneiro (Mar 03 2020 at 08:40):

the odd power thing is nuts

#### Johan Commelin (Mar 03 2020 at 08:40):

We probably need a has_pow ℝ ℚ?

Just say no

#### Mario Carneiro (Mar 03 2020 at 08:41):

use abs and - and build it from the positive version when necessary

#### Johan Commelin (Mar 03 2020 at 08:41):

So how would you express the inverse of λ x, x^3?

#### Mario Carneiro (Mar 03 2020 at 08:41):

x^(1/3), and argue negative numbers by wlog

I don't follow

#### Mario Carneiro (Mar 03 2020 at 08:42):

x^3 is invertible. that's all you need to know

#### Johan Commelin (Mar 03 2020 at 08:43):

Ok, but you don't care about having a formula for the inverse?

#### Mario Carneiro (Mar 03 2020 at 08:43):

The function, if you want to write it down, is if x >= 0 then x^(1/3) else -(-x)^(1/3)

#### Johan Commelin (Mar 03 2020 at 08:44):

Would it make sense to have a nth_root 3 : ℝ → ℝ?

#### Mario Carneiro (Mar 03 2020 at 08:44):

but I reject the idea that this is "the" x^(1/3) function

#### Johan Commelin (Mar 03 2020 at 08:45):

You just don't like the fact that the absolute Galois group of ℝ has order 2...

#### Johan Commelin (Mar 03 2020 at 08:45):

It's a real closed field man... shouldn't we celebrate?

#### Mario Carneiro (Mar 03 2020 at 08:45):

I think that when you start talking about 3rd roots you should go complex

#### Johan Commelin (Mar 03 2020 at 08:46):

I would argue that when you start talking about 2nd roots you should go complex.

#### Kevin Buzzard (Mar 03 2020 at 08:46):

So you want to define x^y with x a negative real and y a rational with non-negative 2-adic valuation?

#### Kevin Buzzard (Mar 03 2020 at 08:47):

We can put it on the pile, with x a positive real and y complex, and with x a non-zero complex and y an integer, as another random region of $\mathbb{C}^2$ where the power operation happens to give a unique sensible answer.

#### Mario Carneiro (Mar 03 2020 at 08:51):

Unlike the first two, it is not continuous on that region

#### Kevin Buzzard (Mar 03 2020 at 08:51):

It's not hard to check that you can't define ^ on all of $\mathbb{C}^2$ and expect all the "standard" facts $(ab)^c=a^cb^c$ and $(a^b)^c=a^{bc}$ and $1^a=1$ to hold (because $(-1)^{1/2}$ has got square $(-1)^1$ and also $1^{1/2}$), but then there seem to be these random regions where you can get away with it.

#### Kevin Buzzard (Mar 03 2020 at 08:52):

Mario Carneiro said:

Unlike the first two, it is not continuous on that region

Is that really true?

#### Mario Carneiro (Mar 03 2020 at 08:52):

It's continuous for fixed y

#### Kevin Buzzard (Mar 03 2020 at 08:53):

Isn't it just $-((-x)^y)$?

#### Mario Carneiro (Mar 03 2020 at 08:53):

but y is in a dense region and it's discontinuous in that direction

#### Mario Carneiro (Mar 03 2020 at 08:54):

$x^{2/3}$ is positive for negative $x$

ha!

#### Mario Carneiro (Mar 03 2020 at 08:55):

let me repeat: nuts

#### Johan Commelin (Mar 03 2020 at 09:06):

@Jalex Stark All these discussions shouldn't discourage you from creating a PR for that 2-liner. You found a hole in the libs! Well done.

#### Patrick Massot (Mar 03 2020 at 09:25):

Jalex Stark said:

woah so if you have a theorem that f_injective, then apply f_injective is the thing that applies f to both sides of an equation

In this case you don't need it, but for feature reference : apply_fun f at hyp would do that for you.

#### Kevin Buzzard (Mar 03 2020 at 11:46):

"applying f to an equation" can mean two things. If the goal is x = y then to "apply f" to it you apply h where h is the proof that f is injective. If you have a hypothesis hyp : x = y then you can "apply f" to it without injectivity, using apply_fun f at hyp.

#### Kevin Buzzard (Mar 03 2020 at 11:47):

I think Donald found the hole :-)

Last updated: May 06 2021 at 17:38 UTC