fastest approach to proving equation iffs

Stream: maths

[Belisarius Cawl]

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]

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]

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

[Kevin Buzzard]

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]

another oversight, thanks

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

Why do you think it shouldn't work?

[Belisarius Cawl]

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

[Ruben Van de Velde]

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]

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]

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

[Sebastien Gouezel]

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]

Right. That was my error. Thanks!

[Bryan Gin-ge Chen]

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.