feat(analysis/special_functions/exp_log): log_nonzero_of_ne_one and l…

…og_inj_pos (#6734)

log_nonzero_of_ne_one and log_inj_pos

Proves : 
 * When `x > 0`, `log(x)` is `0` iff `x = 1`
 * The real logarithm is injective (when restraining the domain to the positive reals)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/analysis/special_functions/exp_log.lean

@@ -486,6 +486,15 @@ begin
   rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]
 end
 
+lemma log_inj_on_pos : set.inj_on log (set.Ioi 0) :=
+strict_mono_incr_on_log.inj_on
+
+lemma eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : log x = 0) : x = 1 :=
+log_inj_on_pos (set.mem_Ioi.2 h₁) (set.mem_Ioi.2 zero_lt_one) (h₂.trans real.log_one.symm)
+
+lemma log_ne_zero_of_pos_of_ne_one {x : ℝ} (hx_pos : 0 < x) (hx : x ≠ 1) : log x ≠ 0 :=
+mt (eq_one_of_pos_of_log_eq_zero hx_pos) hx
+
 /-- The real logarithm function tends to `+∞` at `+∞`. -/
 lemma tendsto_log_at_top : tendsto log at_top at_top :=
 tendsto_comp_exp_at_top.1 $ by simpa only [log_exp] using tendsto_id