Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 25 2020 at 12:04):

The real number version follows from that

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 13:44):

aah but log_mul does indeed exist for reals :-)

view this post on Zulip 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

view this post on Zulip 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,
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

view this post on Zulip Johan Commelin (Mar 03 2020 at 07:56):

Note that puzzle 3 is false if x = 0.

view this post on Zulip Johan Commelin (Mar 03 2020 at 07:56):

Some of these puzzles might be solvable by library_search

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Mar 03 2020 at 07:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:07):

Where do i find the style guide?

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:07):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:08):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:20):

@Jalex Stark Have you considered applying exp_injective?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:22):

@Mario Carneiro oh i see

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:22):

Start your proof with apply exp_injective

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:22):

which proof?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:24):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:25):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:25):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:26):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:27):

yes

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:28):

So I would start that proof immediately with apply exp_injective

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:28):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:28):

And the lhs is equal to that by exp_log hx

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:28):

okay

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:29):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:29):

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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:29):

unknown identifier 'exp_injective'

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:29):

real.exp_injective?

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:29):

that works

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:29):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:30):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:33):

or congr' 1

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:33):

so should the code block

view this post on Zulip 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

view this post on Zulip Jalex Stark (Mar 03 2020 at 08:33):

go into mathlib?

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:34):

Yes, more or less

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:35):

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

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:36):

Also, maybe the name should be log_pow_of_pos?

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:36):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:37):

Is there a log_pow_of_neg?

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:37):

It's probably bananas

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:37):

If not, I wouldn't bother

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:37):

We have very bad powers of negative numbers

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:38):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:39):

I don't think rpow will give you that though

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:39):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:39):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:40):

What I would hope is a complex number

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:40):

the odd power thing is nuts

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:40):

We probably need a has_pow ℝ ℚ?

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:40):

Just say no

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:41):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:41):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:41):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:42):

I don't follow

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:42):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:43):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:44):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:44):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:45):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:45):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:45):

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

view this post on Zulip Johan Commelin (Mar 03 2020 at 08:46):

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

view this post on Zulip 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?

view this post on Zulip 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 C2\mathbb{C}^2 where the power operation happens to give a unique sensible answer.

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:51):

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

view this post on Zulip Kevin Buzzard (Mar 03 2020 at 08:51):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:52):

It's continuous for fixed y

view this post on Zulip Kevin Buzzard (Mar 03 2020 at 08:53):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:53):

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

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:54):

x2/3x^{2/3} is positive for negative xx

view this post on Zulip Kevin Buzzard (Mar 03 2020 at 08:55):

ha!

view this post on Zulip Mario Carneiro (Mar 03 2020 at 08:55):

let me repeat: nuts

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 03 2020 at 11:47):

I think Donald found the hole :-)


Last updated: May 06 2021 at 17:38 UTC