rpow log exp inequalities

Stream: Is there code for X?

[Yaël Dillies]

Is there anything like that somewhere?

import analysis.special_functions.exp_log
import analysis.special_functions.pow

lemma le_pow_of_log_le {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
  (h : (real.log a)/(real.log b) ≤ c) :
  a ≤ b^c := sorry

lemma le_exp_of_log_le {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h : real.log a ≤ b) :
  a ≤ real.exp b := sorry

I need le_pow_of_log_le

[Eric Wieser]

Does monotonicity of exp get you the second one?

[Eric Wieser]

have := real.exp_monotone h followed by rw real.exp_log ha at this or something

[Yaël Dillies]

Yeah, I think that works. Do you think such lemmas are worth having?

[Eric Wieser]

Is the second one true as an iff?

[Kevin Buzzard]

So they are a Galois connection I guess

[Eric Wieser]

Except conditional on a being positive

[Eric Wieser]

I think this lemma is worth having:

lemma log_le_iff_le_exp {a b : ℝ} (ha : 0 < a) :
  real.log a ≤ b ↔ a ≤ real.exp b :=
⟨λ h, real.exp_log ha ▸ real.exp_monotone h, λ h, real.exp_le_exp.mp $ (real.exp_log ha).symm ▸ h⟩

[Kevin Buzzard]

right, they're a galois connection between pos_real and real

[Kevin Buzzard]

In fact they're simply an order isomorphism between pos_real and real, this is what should be proved

[Eric Wieser]

I suspect we have that

[Kevin Buzzard]

well then this is a consequence

[Eric Wieser]

docs#real.exp_order_iso

[Eric Wieser]

Yes, but it's a consequence that probably has awkard coe debris to clean up

[Eric Wieser]

Maybe there's still an easier proof using that lemma though

[Yakov Pechersky]

I mean, real.log is defined using the order iso

[Eric Wieser]

I think your first lemma is false?

[Eric Wieser]

lemma le_pow_of_log_le {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
  (h : (real.log a)/(real.log b) ≤ c) :
  a ≤ b^c := begin
    rw [←real.log_le_log ha (real.rpow_pos_of_pos hb _), real.log_rpow hb,
      mul_comm, ←mul_inv_le_iff _, ←div_eq_mul_inv],
    exact h,
    sorry,  -- 0 < real.log b
  end

[Kevin Buzzard]

If a=b=1/2 and c=2 then h is true and the conclusion isn't.

[Eric Rodriguez]

Eric Wieser said:

docs#real.exp_order_iso

I tried using this a while back and it was hellish

[Yaël Dillies]

Ah yes, we need 1 < b to divide out the logs properly.