Even more positivity extensions

LeanAPAP.lean

@@ -15,17 +15,18 @@ import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
 import LeanAPAP.Mathlib.Algebra.GroupPower.Order
 import LeanAPAP.Mathlib.Algebra.Group.TypeTags
+import LeanAPAP.Mathlib.Algebra.ModEq
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
-import LeanAPAP.Mathlib.Algebra.Order.SMul
 import LeanAPAP.Mathlib.Algebra.Star.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Algebra.Star.Pi
 import LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
 import LeanAPAP.Mathlib.Algebra.Support
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
+import LeanAPAP.Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
@@ -35,6 +36,9 @@ import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
 import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Exponential
 import LeanAPAP.Mathlib.Data.Finset.Basic
@@ -77,6 +81,7 @@ import LeanAPAP.Mathlib.Order.Disjoint
 import LeanAPAP.Mathlib.Order.Heyting.Basic
 import LeanAPAP.Mathlib.Order.Partition.Finpartition
 import LeanAPAP.Mathlib.Tactic.Positivity
+import LeanAPAP.Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing

LeanAPAP/FiniteField/Basic.lean

@@ -33,20 +33,20 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
       (abs_l2inner_le_lpNorm_mul_lpNorm ⟨by exact_mod_cast hp, ?_⟩ _ _)
     _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) :=
         mul_le_mul (lpNorm_conv_le_lpNorm_dconv' (by positivity) (even_two_mul _) _) ?_
-          (by sorry) (by sorry) -- positivity
+          (by positivity) (by positivity)
     _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] *
           γ ^ (-(p : ℝ)⁻¹) := ?_
     _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity
   · rw [←balance_conv, balance, l2inner_sub_left, l2inner_const_left, expect_conv, sum_mu ℝ hA,
       expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ←mul_inv_cancel, ←mul_sub,
-      abs_mul, abs_of_nonneg, mul_div_cancel_left] <;> sorry -- positivity
+      abs_mul, abs_of_nonneg, mul_div_cancel_left] <;> positivity
   · rw [NNReal.coe_inv, NNReal.coe_sub hp'.le]
     simp
-  · rw [lpNorm_mu (one_le_inv (tsub_pos_of_lt hp') tsub_le_self) hC, NNReal.coe_inv, NNReal.coe_inv,
+  · rw [lpNorm_mu (one_le_inv (tsub_pos_of_lt hp') tsub_le_self) hC, NNReal.coe_inv,
       NNReal.coe_sub hp'.le, NNReal.coe_one, inv_inv, sub_sub_cancel_left, ←mul_rpow]
     rw [le_div_iff, mul_comm] at hγC
     refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _)
-    all_goals sorry -- positivity
+    all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two]
     rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
     push_cast
@@ -87,7 +87,7 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card
       Finset.card_empty, zero_div] at hαA ⊢
     exact ⟨by positivity, mul_nonpos_of_nonneg_of_nonpos (by positivity) hαA⟩
   have hγ₁ : γ ≤ 1 := hγC.trans (div_le_one_of_le (Nat.cast_le.2 C.card_le_univ) $ by positivity)
-  have hG : (card G : ℝ) ≠ 0 := by sorry -- positivity
+  have hG : (card G : ℝ) ≠ 0 := by positivity
   have := unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ hγ₁).ne') (ε / 2)
     (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num)
     (const _ (card G)⁻¹) (card G • (balance (μ A) ○ balance (μ A)))

LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean

@@ -308,39 +308,34 @@ open Finset
 namespace Mathlib.Meta.Positivity
 open Qq Lean Meta
 
--- TODO: This doesn't handle universe-polymorphic input
 @[positivity Finset.expect _ _]
-def evalExpect : PositivityExt where eval {u β2} zβ pβ e := do
-  let .app (.app (.app (.app (.app (.const _ [_, v]) (α : Q(Type v))) (β : Q(Type u)))
-    (_a : Q(Semifield $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e)
-      | throwError "not `Finset.expect`"
-  haveI' : $β =Q $β2 := ⟨⟩
-  haveI' : $e =Q Finset.expect $s $b := ⟨⟩
-  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
-  let rb ← core zβ pβ rhs
-
-  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
-    try {
-      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
-      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-      match s with
-      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
-      | _ => pure none }
-    catch _e => do
-      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-      pure (some (.fvar fv))
-  match rb, so with
-  | .nonnegative pb, _ => do
-    let pα' ← synthInstanceQ (q(LinearOrderedSemifield $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
-    pure (.nonnegative q(@expect_nonneg.{u, v} $α $β $pα' $s $b (fun i _h => $pr i)))
-  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-    let pα' ← synthInstanceQ (q(LinearOrderedSemifield $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
-    pure (.positive q(@expect_pos.{u, v} $α $β $pα' $s $b (fun i _h => $pr i) $fi))
-  | _, _ => pure .none
+def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.expect $ι _ $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try {
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      } catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let instα' ← synthInstanceQ q(LinearOrderedSemifield $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      pure (.nonnegative q(@expect_nonneg $ι $α $instα' $s $f fun i _ ↦ $pr i))
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let instα' ← synthInstanceQ q(LinearOrderedSemifield $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      pure (.positive q(@expect_pos $ι $α $instα' $s $f (fun i _ ↦ $pr i) $fi))
+    | _, _ => pure .none
+  | _ => throwError "not Finset.expect"
 
 example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
 example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity

LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean

@@ -23,43 +23,38 @@ lemma sum_mul_sq_le_sq_mul_sq (s : Finset α) (f g : α → 𝕜) :
 
 end Finset
 
-open Finset
-open scoped BigOperators
-open Qq Lean Meta
 
--- TODO: This doesn't handle universe-polymorphic input
-@[positivity Finset.sum _ _]
-def Mathlib.Meta.Positivity.evalFinsetSum : PositivityExt where eval {u β2} zβ pβ e := do
-  let .app (.app (.app (.app (.app (.const _ [_, v]) (β : Q(Type u))) (α : Q(Type v)))
-    (_a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e)
-      | throwError "not `Finset.sum`"
-  haveI' : $β =Q $β2 := ⟨⟩
-  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
-  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
-  let rb ← core zβ pβ rhs
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
 
-  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
-    try {
-      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
-      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-      match s with
-      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
-      | _ => pure none }
-    catch _e => do
-      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-      pure (some (.fvar fv))
-  match rb, so with
-  | .nonnegative pb, _ => do
-    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
-    pure (.nonnegative q(@sum_nonneg.{u, v} $α $β $pα' $b $s (fun i _h => $pr i)))
-  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-    let pα' ← synthInstanceQ (q(OrderedCancelAddCommMonoid $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
-    pure (.positive q(@sum_pos.{u, v} $α $β $pα' $b $s (fun i _h => $pr i) $fi))
-  | _, _ => pure .none
+@[positivity Finset.sum _ _]
+def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.sum _ $ι $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try {
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      } catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      pure (.nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i))
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      pure (.positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi))
+    | _, _ => pure .none
+  | _ => throwError "not Finset.sum"
 
 example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∑ j in range n, a j^2 := by positivity
 example (a : ULift.{2} ℕ → ℤ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ ∑ j in s, a j^2 := by positivity

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -19,21 +19,20 @@ private alias ⟨_, sinh_ne_zero_of_ne_zero⟩ := Real.sinh_ne_zero
 /-- Extension for the `positivity` tactic: `Real.sinh` is positive/nonnegative/nonzero if its input
 is. -/
 @[positivity Real.sinh _]
-def evalSinh : PositivityExt where eval zα pα e := do
-  let (.app f (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.sinh"
-  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.sinh)
-  let ra ← core zα pα a
-  match ra with
-  | .positive pa =>
-      have pa' : Q(0 < $a) := pa
-      return .positive (q(sinh_pos_of_pos $pa') : Expr)
-  | .nonnegative pa =>
-      have pa' : Q(0 ≤ $a) := pa
-      return .nonnegative (q(sinh_nonneg_of_nonneg $pa') : Expr)
-  | .nonzero pa =>
-      have pa' : Q($a ≠ 0) := pa
-      return .nonzero (q(sinh_ne_zero_of_ne_zero $pa') : Expr)
-  | _ => return .none
+def evalSinh : PositivityExt where eval {u α} _ _ e := do
+  let zα : Q(Zero ℝ) := q(inferInstance)
+  let pα : Q(PartialOrder ℝ) := q(inferInstance)
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(Real.sinh $a) =>
+      assumeInstancesCommute
+      match ← core zα pα a with
+      | .positive pa => return .positive q(sinh_pos_of_pos $pa)
+      | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa)
+      | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
+      | _ => return .none
+    | _, _ => throwError "not Real.sinh"
+  else throwError "not Real.sinh"
 
 example (x : ℝ) (hx : 0 < x) : 0 < x.sinh := by positivity
 example (x : ℝ) (hx : 0 ≤ x) : 0 ≤ x.sinh := by positivity

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean

@@ -0,0 +1,48 @@
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
+import LeanAPAP.Mathlib.Data.Nat.Factorial.Basic
+
+open NormedSpace
+open scoped Nat
+
+namespace Complex
+
+/-- The power series expansion of `Complex.cosh`. -/
+lemma hasSum_cosh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n) / ↑(2 * n)!) (cosh z) := by
+  simpa [mul_assoc, cos_mul_I] using hasSum_cos' (z * I)
+
+/-- The power series expansion of `Complex.sinh`. -/
+lemma hasSum_sinh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z) := by
+  simpa [mul_assoc, sin_mul_I, neg_pow z, pow_add, pow_mul, neg_mul, neg_div]
+    using (hasSum_sin' (z * I)).mul_right (-I)
+
+lemma cosh_eq_tsum (z : ℂ) : cosh z = ∑' n, z ^ (2 * n) / ↑(2 * n)! := z.hasSum_cosh.tsum_eq.symm
+
+lemma sinh_eq_tsum (z : ℂ) : sinh z = ∑' n, z ^ (2 * n + 1) / ↑(2 * n + 1)! :=
+  z.hasSum_sinh.tsum_eq.symm
+
+end Complex
+
+namespace Real
+
+/-- The power series expansion of `Real.cosh`. -/
+lemma hasSum_cosh (r : ℝ) : HasSum (fun n  ↦ r ^ (2 * n) / ↑(2 * n)!) (cosh r) :=
+  mod_cast Complex.hasSum_cosh r
+
+/-- The power series expansion of `Real.sinh`. -/
+lemma hasSum_sinh (r : ℝ) : HasSum (fun n ↦ r ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh r) :=
+  mod_cast Complex.hasSum_sinh r
+
+lemma cosh_eq_tsum (r : ℝ) : cosh r = ∑' n, r ^ (2 * n) / ↑(2 * n)! := r.hasSum_cosh.tsum_eq.symm
+
+lemma sinh_eq_tsum (r : ℝ) : sinh r = ∑' n, r ^ (2 * n + 1) / ↑(2 * n + 1)! :=
+  r.hasSum_sinh.tsum_eq.symm
+
+lemma cosh_le_exp_half_sq (x : ℝ) : cosh x ≤ exp (x ^ 2 / 2) := by
+  rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum]
+  refine tsum_le_tsum (fun i ↦ ?_) x.hasSum_cosh.summable $ expSeries_summable' (x ^ 2 / 2)
+  simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]
+  gcongr
+  norm_cast
+  exact Nat.two_pow_mul_factorial_le_factorial_two_mul
+
+end Real

LeanAPAP/Mathlib/Data/Complex/Exponential.lean

@@ -22,6 +22,11 @@ lemma one_sub_le_exp_neg (x : ℝ) : 1 - x ≤ exp (-x) :=
 lemma one_sub_lt_exp_neg (hx : x ≠ 0) : 1 - x < exp (-x) :=
   (sub_eq_neg_add _ _).trans_lt $ add_one_lt_exp $ neg_ne_zero.2 hx
 
+lemma exp_nonneg (x : ℝ) : 0 ≤ exp x := x.exp_pos.le
+
+lemma exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x) := by
+  cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]
+
 lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=
   calc
     x ^ n / n ! ≤ ∑ k in range (n + 1), x ^ k / k !
@@ -31,12 +36,19 @@ lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x
 end Real
 
 namespace Mathlib.Meta.Positivity
-open Lean.Meta Qq
+open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: `Real.cosh` is always positive. -/
 @[positivity Real.cosh _]
-def evalCosh : PositivityExt where eval _ _ e := do
-  let (.app _ (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.cosh"
-  pure (.positive (q(Real.cosh_pos $a) : Lean.Expr))
+def evalCosh : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(Real.cosh $a) =>
+      assumeInstancesCommute
+      return .positive q(Real.cosh_pos $a)
+    | _, _ => throwError "not Real.cosh"
+  else throwError "not Real.cosh"
+
+example (x : ℝ) : 0 < x.cosh := by positivity
 
 end Mathlib.Meta.Positivity

LeanAPAP/Mathlib/Data/Nat/Factorial/Basic.lean

@@ -9,4 +9,12 @@ lemma factorial_two_mul_le : (2 * n)! ≤ (2 * n) ^ n * n ! := by
   rw [two_mul, ←factorial_mul_ascFactorial, mul_comm]
   exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _
 
+lemma two_pow_mul_factorial_le_factorial_two_mul : 2 ^ n * n ! ≤ (2 * n) ! := by
+  obtain _ | n := n
+  · simp
+  rw [mul_comm, two_mul]
+  calc
+    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) := mul_le_mul_left' (pow_le_pow_of_le_left le_add_self _) _
+    _ ≤ _ := Nat.factorial_mul_pow_le_factorial
+
 end Nat