Zulip Chat Archive

Stream: maths

Topic: fastest approach to proving equation iffs


view this post on Zulip 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/(TT)) ^ (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)

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

view this post on Zulip Belisarius Cawl (Mar 25 2021 at 17:31):

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

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

view this post on Zulip Belisarius Cawl (Mar 25 2021 at 17:32):

another oversight, thanks

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

view this post on Zulip 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/(TT)) ^ (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

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

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

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

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

view this post on Zulip Ruben Van de Velde (Mar 26 2021 at 08:40):

Why do you think it shouldn't work?

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

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

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

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

view this post on Zulip Sebastien Gouezel (Mar 26 2021 at 08:59):

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

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:00):

Right. That was my error. Thanks!

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