# Zulip Chat Archive

## 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, 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 (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`

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

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):

#### 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

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

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`

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

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`

?

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

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

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

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 ℝ ℚ`

?

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

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

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

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$

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

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