Help with Basic Property of Real Exponents

Stream: new members

[Dave Jones]

Hello - complete amateur here, stumbling through verifying my first elementary proof.
I've made some good progress, and I'm really enjoying Lean so far, but I'm hung up on a basic property of real exponents.

I would like to be able to use the following theorem, but I'm not seeing it in mathlib and I'm not quite sure how to proceed with a proof.

import analysis.special_functions.pow
theorem rpow_eq_one_iff {x : nnreal} {y : ℝ} : x ^ y = 1 ↔ x = 1 ∨ y = 0 := by sorry

The statement I need in my proof is the following, so any direct solution for the below example would suffice.

import analysis.special_functions.pow
example (a : ℝ) (ha₁ : 0 < a) (ha₂ : a < 1) : (2:ℝ)^(1 - a) - 1 ≠ 0 := by sorry

Thank you for any help!

[Yaël Dillies]

Have you tried by positivity?

[Yaël Dillies]

Oh wait #16632 still hasn't been merged, @Anne Baanen

[Yaël Dillies]

(but that would only give you 0 < (2 : ℝ)^(1 - a) anyway)

[Moritz Doll]

docs#real.one_lt_rpow together with docs#ne_of_gt should help (I hope I got the inequality sign the right way round)

[Anne Baanen]

Yaël Dillies said:

Oh wait #16632 still hasn't been merged, Anne Baanen

I'm not opposed to merging this but it's more important to come to a consensus with the other reviewers. I'll try and ask them to come to a conclusion.

[Dave Jones]

Thank you for the quick responses!

@Moritz Doll - These two theorems did the trick!
This would have taken me way longer to come up with on my own - thank you so much!

@Yaël Dillies My system was actually able to recognize the keyword positivity, but I got the following errors:

not a positivity/nonnegativity/nonzeroness goal

failed to prove positivity/nonnegativity/nonzeroness

Just in case this might be useful feedback.

Thanks all

[Moritz Doll]

the reason why positivity does not work here is because you are proving something that is not 'by design' positive such as $0 \leq e^x + 3*|y|$. There is the addition that if positivity can prove such a goal it can also prove that the RHS is not equal to zero.

[Yaël Dillies]

I know I know. I just hadn't seen the - 1 on the LHS.

[Eric Wieser]

I had a proof of this floating around:

lemma real.rpow_eq_one_iff_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
  x ^ y = 1 ↔ x = 1 ∨ y = 0 :=
begin
  obtain rfl | hy := eq_or_ne y 0,
  { simp },
  split,
  { intro h,
    rw [← real.one_rpow y] at h,
    left,
    refine real.rpow_left_inj_on hy hx _ h,
    exact @zero_le_one ℝ _, },
  { rintros (rfl | rfl),
    { exact real.one_rpow _ },
    { exact real.rpow_zero _ } },
end

lemma nnreal.rpow_eq_one_iff {x : ℝ≥0} {y : ℝ} :
  x ^ y = 1 ↔ x = 1 ∨ y = 0 :=
by exact_mod_cast real.rpow_eq_one_iff_of_nonneg x.prop