feat: positivity extension for Real.log of natural/integer casts …

…and numeric literals (#5839)

This PR adds a positivity extension for expressions of the form `Real.log n` where `n` is a cast from a natural number or an integer. (Since `positivity` can't handle conditions like `1 ≤ x`, this is pretty much the best we can do for the log.)

Also, the namespace of the positivity extension for `exp` is corrected.

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -184,6 +184,11 @@ theorem log_pos (hx : 1 < x) : 0 < log x :=
   (log_pos_iff (lt_trans zero_lt_one hx)).2 hx
 #align real.log_pos Real.log_pos
 
+theorem log_pos_of_lt_neg_one (hx : x < -1) : 0 < log x := by
+  rw [←neg_neg x, log_neg_eq_log]
+  have : 1 < -x := by linarith
+  exact log_pos this
+
 theorem log_neg_iff (h : 0 < x) : log x < 0 ↔ x < 1 := by
   rw [← log_one]
   exact log_lt_log_iff h zero_lt_one
@@ -193,6 +198,12 @@ theorem log_neg (h0 : 0 < x) (h1 : x < 1) : log x < 0 :=
   (log_neg_iff h0).2 h1
 #align real.log_neg Real.log_neg
 
+theorem log_neg_of_lt_zero (h0 : x < 0) (h1 : -1 < x) : log x < 0 := by
+  rw [←neg_neg x, log_neg_eq_log]
+  have h0' : 0 < -x := by linarith
+  have h1' : -x < 1 := by linarith
+  exact log_neg h0' h1'
+
 theorem log_nonneg_iff (hx : 0 < x) : 0 ≤ log x ↔ 1 ≤ x := by rw [← not_lt, log_neg_iff hx, not_lt]
 #align real.log_nonneg_iff Real.log_nonneg_iff
 
@@ -213,6 +224,30 @@ theorem log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 :=
   (log_nonpos_iff' hx).2 h'x
 #align real.log_nonpos Real.log_nonpos
 
+theorem log_nat_cast_nonneg (n : ℕ) : 0 ≤ log n := by
+  by_cases hn : n = 0
+  case pos => simp [hn]
+  case neg =>
+    have : (1 : ℝ) ≤ n := by exact_mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
+    exact log_nonneg this
+
+theorem log_neg_nat_cast_nonneg (n : ℕ) : 0 ≤ log (-n) := by
+  rw [←log_neg_eq_log, neg_neg]
+  exact log_nat_cast_nonneg _
+
+theorem log_int_cast_nonneg (n : ℤ) : 0 ≤ log n := by
+  cases lt_trichotomy 0 n with
+  | inl hn =>
+      have : (1 : ℝ) ≤ n := by exact_mod_cast hn
+      exact log_nonneg this
+  | inr hn =>
+      cases hn with
+      | inl hn => simp [hn.symm]
+      | inr hn =>
+          have : (1 : ℝ) ≤ -n := by rw [←neg_zero, ←lt_neg] at hn; exact_mod_cast hn
+          rw [←log_neg_eq_log]
+          exact log_nonneg this
+
 theorem strictMonoOn_log : StrictMonoOn log (Set.Ioi 0) := fun _ hx _ _ hxy => log_lt_log hx hxy
 #align real.strict_mono_on_log Real.strictMonoOn_log
 
@@ -440,3 +475,115 @@ theorem tendsto_log_nat_add_one_sub_log : Tendsto (fun k : ℕ => log (k + 1) -
 end Real
 
 end TendstoCompAddSub
+
+namespace Mathlib.Meta.Positivity
+open Lean.Meta Qq
+
+lemma log_nonneg_of_isNat (h : NormNum.IsNat e n) : 0 ≤ Real.log (e : ℝ) := by
+  rw [NormNum.IsNat.to_eq h rfl]
+  exact Real.log_nat_cast_nonneg _
+
+lemma log_pos_of_isNat (h : NormNum.IsNat e n) (w : Nat.blt 1 n = true) : 0 < Real.log (e : ℝ) := by
+  rw [NormNum.IsNat.to_eq h rfl]
+  apply Real.log_pos
+  simpa using w
+
+lemma log_nonneg_of_isNegNat (h : NormNum.IsInt e (.negOfNat n)) : 0 ≤ Real.log (e : ℝ) := by
+  rw [NormNum.IsInt.neg_to_eq h rfl]
+  exact Real.log_neg_nat_cast_nonneg _
+
+lemma log_pos_of_isNegNat (h : NormNum.IsInt e (.negOfNat n)) (w : Nat.blt 1 n = true) :
+    0 < Real.log (e : ℝ) := by
+  rw [NormNum.IsInt.neg_to_eq h rfl]
+  rw [Real.log_neg_eq_log]
+  apply Real.log_pos
+  simpa using w
+
+lemma log_pos_of_isRat :
+    (NormNum.IsRat e n d) → (decide ((1 : ℚ) < n / d)) → (0 < Real.log (e : ℝ))
+  | ⟨inv, eq⟩, h => by
+    rw [eq, invOf_eq_inv, ←div_eq_mul_inv]
+    have : 1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h
+    exact Real.log_pos this
+
+lemma log_pos_of_isRat_neg :
+    (NormNum.IsRat e n d) → (decide (n / d < (-1 : ℚ))) → (0 < Real.log (e : ℝ))
+  | ⟨inv, eq⟩, h => by
+    rw [eq, invOf_eq_inv, ←div_eq_mul_inv]
+    have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
+    exact Real.log_pos_of_lt_neg_one this
+
+lemma log_nz_of_isRat : (NormNum.IsRat e n d) → (decide ((0 : ℚ) < n / d))
+    → (decide (n / d < (1 : ℚ))) → (Real.log (e : ℝ) ≠ 0)
+  | ⟨inv, eq⟩, h₁, h₂ => by
+    rw [eq, invOf_eq_inv, ←div_eq_mul_inv]
+    have h₁' : 0 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₁
+    have h₂' : (n : ℝ) / d < 1 := by exact_mod_cast of_decide_eq_true h₂
+    exact ne_of_lt <| Real.log_neg h₁' h₂'
+
+lemma log_nz_of_isRat_neg : (NormNum.IsRat e n d) → (decide (n / d < (0 : ℚ)))
+      → (decide ((-1 : ℚ) < n / d)) → (Real.log (e : ℝ) ≠ 0)
+  | ⟨inv, eq⟩, h₁, h₂ => by
+    rw [eq, invOf_eq_inv, ←div_eq_mul_inv]
+    have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁
+    have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂
+    exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'
+
+/-- Extension for the `positivity` tactic: `Real.log` of a natural number is always nonnegative. -/
+@[positivity Real.log (Nat.cast _)]
+def evalLogNatCast : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app (f : Q(ℝ → ℝ)) (.app _ (a : Q(ℕ))) ← withReducible (whnf e) | throwError "not Real.log"
+  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.log)
+  pure (.nonnegative (q(Real.log_nat_cast_nonneg $a) : Lean.Expr))
+
+/-- Extension for the `positivity` tactic: `Real.log` of an integer is always nonnegative. -/
+@[positivity Real.log (Int.cast _)]
+def evalLogIntCast : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app (f : Q(ℝ → ℝ)) (.app _ (a : Q(ℤ))) ← withReducible (whnf e) | throwError "not Real.log"
+  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.log)
+  pure (.nonnegative (q(Real.log_int_cast_nonneg $a) : Lean.Expr))
+
+/-- Extension for the `positivity` tactic: `Real.log` of a numeric literal. -/
+@[positivity Real.log _]
+def evalLogNatLit : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app (f : Q(ℝ → ℝ)) (a : Q(ℝ)) ← withReducible (whnf e) | throwError "not Real.log"
+  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.log)
+  match ←NormNum.derive a with
+  | .isNat (_ : Q(AddMonoidWithOne ℝ)) lit p =>
+    assumeInstancesCommute
+    have p : Q(NormNum.IsNat $a $lit) := p
+    if 1 < lit.natLit! then
+      let p' : Q(Nat.blt 1 $lit = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.positive (q(log_pos_of_isNat $p $p') : Lean.Expr))
+    else
+      pure (.nonnegative (q(log_nonneg_of_isNat $p) : Lean.Expr))
+  | .isNegNat _ lit p =>
+    assumeInstancesCommute
+    have p : Q(NormNum.IsInt $a (Int.negOfNat $lit)) := p
+    if 1 < lit.natLit! then
+      let p' : Q(Nat.blt 1 $lit = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.positive (q(log_pos_of_isNegNat $p $p') : Lean.Expr))
+    else
+      pure (.nonnegative (q(log_nonneg_of_isNegNat $p) : Lean.Expr))
+  | .isRat (i : Q(DivisionRing ℝ)) q n d p =>
+    assumeInstancesCommute
+    have p : Q(by clear! «$i»; exact NormNum.IsRat $a $n $d) := p
+    if 0 < q ∧ q < 1 then
+      let w₁ : Q(decide ((0 : ℚ) < $n / $d) = true) := (q(Eq.refl true) : Lean.Expr)
+      let w₂ : Q(decide ($n / $d < (1 : ℚ)) = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.nonzero (q(log_nz_of_isRat $p $w₁ $w₂) : Lean.Expr))
+    else if 1 < q then
+      let w : Q(decide ((1 : ℚ) < $n / $d) = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.positive (q(log_pos_of_isRat $p $w) : Lean.Expr))
+    else if -1 < q ∧ q < 0 then
+      let w₁ : Q(decide ($n / $d < (0 : ℚ)) = true) := (q(Eq.refl true) : Lean.Expr)
+      let w₂ : Q(decide ((-1 : ℚ) < $n / $d) = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.nonzero (q(log_nz_of_isRat_neg $p $w₁ $w₂) : Lean.Expr))
+    else if q < -1 then
+      let w : Q(decide ($n / $d < (-1 : ℚ)) = true) := (q(Eq.refl true) : Lean.Expr)
+      pure (.positive (q(log_pos_of_isRat_neg $p $w) : Lean.Expr))
+    else
+      failure
+  | _ => failure
+
+end Mathlib.Meta.Positivity

Mathlib/Data/Complex/Exponential.lean

@@ -2012,16 +2012,16 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
 
 end Real
 
-namespace Tactic
+namespace Mathlib.Meta.Positivity
 open Lean.Meta Qq
 
 /-- Extension for the `positivity` tactic: `Real.exp` is always positive. -/
 @[positivity Real.exp _]
-def evalExp : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+def evalExp : PositivityExt where eval {_ _} _ _ e := do
   let (.app _ (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.exp"
   pure (.positive (q(Real.exp_pos $a) : Lean.Expr))
 
-end Tactic
+end Mathlib.Meta.Positivity
 
 namespace Complex
 

test/positivity.lean

@@ -2,6 +2,7 @@ import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
 
 /-! # Tests for the `positivity` tactic
 
@@ -253,6 +254,18 @@ example (n : ℕ) : 0 < n ! := by positivity
 
 example {r : ℝ} : 0 < Real.exp r := by positivity
 
+example {n : ℕ} : 0 ≤ Real.log n := by positivity
+example {n : ℤ} : 0 ≤ Real.log n := by positivity
+example : 0 < Real.log 2 := by positivity
+example : 0 < Real.log 1.01 := by positivity
+example : 0 ≠ Real.log 0.99 := by positivity
+example : 0 < Real.log (-2) := by positivity
+example : 0 < Real.log (-1.01) := by positivity
+example : 0 ≠ Real.log (-0.99) := by positivity
+example : 0 ≤ Real.log 1 := by positivity
+example : 0 ≤ Real.log 0 := by positivity
+example : 0 ≤ Real.log (-1) := by positivity
+
 example {V : Type _} [NormedCommGroup V] (x : V) : 0 ≤ ‖x‖ := by positivity
 example {V : Type _} [NormedAddCommGroup V] (x : V) : 0 ≤ ‖x‖ := by positivity