log (a ^ n) = n * log a in mathlib?

Stream: maths

[Donald Sebastian Leung]

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]

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]

The real number version follows from that

[Kevin Buzzard]

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

[Donald Sebastian Leung]

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]

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

[Donald Sebastian Leung]

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]

aah but log_mul does indeed exist for reals :-)

[Mario Carneiro]

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

[Jalex Stark]

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,
rw hd, rw nat.succ_eq_add_one,
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,
rw pow_succ, rw nat.succ_eq_add_one,
have t : x * ↑(d + 1) = x * ↑d + x := by ring, rw t,
rw real.rpow_add _ x _,
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]

Note that puzzle 3 is false if x = 0.

[Johan Commelin]

Some of these puzzles might be solvable by library_search

[Johan Commelin]

@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]

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

[Kevin Buzzard]

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]

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

[Jalex Stark]

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

[Mario Carneiro]

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]

Where do i find the style guide?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

@Jalex Stark Have you considered applying exp_injective?

[Mario Carneiro]

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

[Jalex Stark]

@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]

@Mario Carneiro oh i see

[Johan Commelin]

Start your proof with apply exp_injective

[Jalex Stark]

which proof?

[Jalex Stark]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I guess something like

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

[Jalex Stark]

yes

[Johan Commelin]

So I would start that proof immediately with apply exp_injective

[Mario Carneiro]

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

[Johan Commelin]

And the lhs is equal to that by exp_log hx

[Jalex Stark]

okay

[Jalex Stark]

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

[Johan Commelin]

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

[Jalex Stark]

unknown identifier 'exp_injective'

[Johan Commelin]

real.exp_injective?

[Jalex Stark]

that works

[Mario Carneiro]

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

[Johan Commelin]

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

[Jalex Stark]

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]

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]

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

[Johan Commelin]

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]

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]

or congr' 1

[Jalex Stark]

so should the code block

[Jalex Stark]

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

[Jalex Stark]

go into mathlib?

[Johan Commelin]

Yes, more or less

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

Also, maybe the name should be log_pow_of_pos?

[Mario Carneiro]

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

[Mario Carneiro]

Is there a log_pow_of_neg?

[Johan Commelin]

It's probably bananas

[Mario Carneiro]

If not, I wouldn't bother

[Johan Commelin]

We have very bad powers of negative numbers

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

I don't think rpow will give you that though

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

What I would hope is a complex number

[Mario Carneiro]

the odd power thing is nuts

[Johan Commelin]

We probably need a has_pow ℝ ℚ?

[Mario Carneiro]

Just say no

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

I don't follow

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Mario Carneiro said:

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

Is that really true?

[Mario Carneiro]

It's continuous for fixed y

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

ha!

[Mario Carneiro]

let me repeat: nuts

[Johan Commelin]

@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]

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]

"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]

I think Donald found the hole :-)