## Stream: maths

### Topic: fastest approach to proving equation iffs

#### Belisarius Cawl (Mar 25 2021 at 17:27):

I want to prove the following:

(EDIT: mwe + backticks)

import data.real.basic
import tactic.suggest
import analysis.special_functions.pow
import tactic.rewrite_search.frontend

lemma delta_A
(A T ΔA ΔT a t : ℝ)
(posA : A > 0)
(posT : T > 0)
(posA' : A + ΔA > 0)
(posT' : T + ΔT > 0)
(mina : 0 < a)
(mint : 0 < t)
(maxa : a < 1)
(maxt : t < 1)
:
A^a * T^t  = (A + ΔA)^a * (T + ΔT)^t
↔
ΔA = A * ((T/(T+ΔT)) ^ (t/a) - 1)

:=
begin
rewrite_search,
end


how would be the best way to go about this? rewrite_search says "search failed: all vertices explored". Also I feel I have to tell LEAN about the assumptions somehow - in the numbers game I would use cases but not sure what it does with reals.

(I guess I could manually invoke all the lemmas but doubt this is the fastest approach)

#### Kevin Buzzard (Mar 25 2021 at 17:28):

right now that's pretty easy to prove because maxt is a false assumption. Why not set this up as a #mwe and post code in triple backticks?

#### Belisarius Cawl (Mar 25 2021 at 17:31):

ah, right. Typo, also did not know about the mwe rule. brb.

#### Kevin Buzzard (Mar 25 2021 at 17:31):

I'm not sure your goal is true even if you fix the maxt issue -- if Delta A is large and negative then you're going to be taking the a'th power of a negative number, which will give meaningless results.

#### Belisarius Cawl (Mar 25 2021 at 17:32):

another oversight, thanks

#### Kevin Buzzard (Mar 25 2021 at 17:32):

Once you've got it straight, the way to do it would be to rewrite lemmas which will use assumptions as input hypotheses.

#### Sebastien Gouezel (Mar 25 2021 at 19:43):

Here is a way to do it . The first two lemmas should probably be added to mathlib.

import data.real.basic
import tactic.suggest
import analysis.special_functions.pow
import tactic.rewrite_search.frontend

lemma real.rpow_inj_on {a : ℝ} (ha : a ≠ 0) :
set.inj_on (λ (x : ℝ), x ^ a) (set.Ici 0) :=
begin
assume x hx y hy h,
dsimp at h,
have A : ∀ (z : ℝ), 0 ≤ z → z = (z ^ a) ^ (a ⁻¹) :=
λ z hz, by rw [← real.rpow_mul hz, mul_inv_cancel ha, real.rpow_one],
rw [A x hx, A y hy, h],
end

lemma real.rpow_eq_rpow_iff {a x y : ℝ} (ha : a ≠ 0) (hx : 0 ≤ x) (hy : 0 ≤ y) :
x ^ a = y ^ a ↔ x = y :=
(real.rpow_inj_on ha).eq_iff hx hy

lemma delta_A
(A T ΔA ΔT a t : ℝ)
(posA : 0 < A)
(posT : 0 < T)
(posA' : 0 < A + ΔA)
(posT' : 0 < T + ΔT)
(mina : 0 < a)
(mint : 0 < t)
(maxa : a < 1)
(maxt : t < 1)
:
A^a * T^t  = (A + ΔA)^a * (T + ΔT)^t
↔
ΔA = A * ((T/(T+ΔT)) ^ (t/a) - 1)

:=
begin
-- first, get rid of the denominators in the second equation
rw real.div_rpow posT.le posT'.le,
have : (T + ΔT)^(t/a) ≠ 0,
by simp [posT'.ne', real.rpow_eq_zero_iff_of_nonneg posT'.le],
field_simp only,
conv_rhs { rw [← sub_eq_zero_iff_eq] },
-- then, remove the power a in the first equation
have H : ∀ {z : ℝ}, 0 < z → z ^ t = (z ^ (t/a))^a,
{ assume z hz, rw ← real.rpow_mul hz.le, simp [mina.ne'] },
have H' : ∀ {z : ℝ}, 0 < z → 0 ≤ z ^ (t/a),
{ assume z hz, exact real.rpow_nonneg_of_nonneg hz.le _ },
rw [H posT, H posT', ← real.mul_rpow posA.le (H' posT), ← real.mul_rpow posA'.le (H' posT'),
real.rpow_eq_rpow_iff mina.ne' (mul_nonneg posA.le (H' posT))
(mul_nonneg posA'.le (H' posT')), eq_comm, ← sub_eq_zero_iff_eq],
-- check that we have brought both equations to the same form
congr' 2,
ring,
end

#lint


#### Sebastien Gouezel (Mar 25 2021 at 19:45):

As you can see, this is pretty painful. What I do is massage the two equations to make them the same up to algebraic manipulations, and then ask ring to check that indeed I have got to the same expressions. To massage the first one, I cancel out the exponent a using the lemma real.rpow_eq_rpow_iff that I prove above. To massage the second one, I remove the denominators by calling field_simp (but first I need to check that the denominator is nonzero).

#### Sebastien Gouezel (Mar 25 2021 at 19:47):

Note that the call to lint at the end is to let you see which assumptions of your lemmas I ended up not using. Also, many of your assumptions that are strict inequalities can be weakened to large inequalities without harm. Note that you formulated your inequalities like A > 0, but instead you should use 0 < A (which is mathematically the same, but most of our lemmas are designed to work with the second form, so it is good practice to only use this one).

#### Belisarius Cawl (Mar 26 2021 at 07:50):

Just saw it thanks to you pointing it out in the other thread. Thanks again - there is a lot to unpack. Having a look now.

#### Belisarius Cawl (Mar 26 2021 at 08:38):

ok - I think I managed to understand the first two lemmas (I like the approach by the way), except for the following:
the lemma real.rpow_inj_on shows that exponentiation is injective on set.Ici 0 which I understand to be the strictly positive numbers - but what about negative exponents?

LEAN accepts lemma real.rpow_eq_rpow_iff too which I think it should not (EDIT because real.rpow_inj_on talks only about positive exponents). Where is my error?

#### Ruben Van de Velde (Mar 26 2021 at 08:40):

Why do you think it shouldn't work?

#### Belisarius Cawl (Mar 26 2021 at 08:48):

well because the first lemma only talks about positive exponents but a can be negative too, no?

#### Ruben Van de Velde (Mar 26 2021 at 08:50):

This one?

lemma real.rpow_inj_on {a : ℝ} (ha : a ≠ 0) :
set.inj_on (λ (x : ℝ), x ^ a) (set.Ici 0)


That talks about non-zero exponents and non-negative base

#### Sebastien Gouezel (Mar 26 2021 at 08:50):

The first lemma talks about nonzero exponents (that's what the assumption ha says). The Ici 0 is the set on which the function is injective.

#### Belisarius Cawl (Mar 26 2021 at 08:58):

aah I think I get it. The Ici 0 is the codomain. Was assuming it to be the domain.

#### Sebastien Gouezel (Mar 26 2021 at 08:59):

No, it is the domain, but of the function $x \mapsto x^a$. I.e., we are requiring $x$ to be nonnegative, but this doesn't say anything about a (which is just required to be nonzero).

#### Belisarius Cawl (Mar 26 2021 at 09:00):

Right. That was my error. Thanks!

#### Bryan Gin-ge Chen (Mar 26 2021 at 13:18):

There's a (long and most likely golfable) proof that rpow with an odd natural exponent is strictly monotonic on all the reals in this thread. It'd be good for someone to PR a bunch of lemmas from that thread too.

Last updated: May 10 2021 at 07:15 UTC