broken positivity extensions for sums?

Stream: mathlib4

[Jireh Loreaux]

It seems that the positivity extensions for Finset.sum and tsum are broken, but I recall that I have used them at some point where they did work.

import Mathlib.Tactic.Positivity.Finset
import Mathlib.Topology.Algebra.InfiniteSum.Order

set_option trace.Tactic.positivity true

/--
trace: [Tactic.positivity] trying to prove positivity of ∑ i ∈ s, f i
[Tactic.positivity] trying to prove positivity of f ?m.18
[Tactic.positivity] f ?m.18 => none
[Tactic.positivity] ∑ i ∈ s, f i => none
-/
#guard_msgs in
example {ι α : Type*} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (f : ι → α)
    (h : ∀ i, 0 ≤ f i) (s : Finset ι) : 0 ≤ ∑ i ∈ s, f i := by
  try positivity
  exact s.sum_nonneg fun i _ ↦ h i

/--
trace: [Tactic.positivity] trying to prove positivity of ∑' (i : ι), f i
[Tactic.positivity] trying to prove positivity of f i
[Tactic.positivity] f i => none
[Tactic.positivity] ∑' (i : ι), f i => none
-/
#guard_msgs in
example {ι α : Type*} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α]
    [OrderClosedTopology α] (f : ι → α) (h : ∀ i, 0 ≤ f i) : 0 ≤ ∑' i, f i := by
  try positivity
  exact tsum_nonneg h

[Jireh Loreaux]

@Yaël Dillies because you wrote the extension for Finset.sum. I assume I'm somehow being an idiot here, because there's no way this can actually be broken without breaking a bunch of uses in Mathlib, right?

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Ah, I understand, the issue is that it can't use the hypothesis because it's under a binder. It would work if the quantity we were summing over were obviously nonnegative for some other reason (e.g., each term was of the form‖_‖).

[Yaël Dillies]

Yep, exactly. Would be nice if we could support this obvious use case, but it would be getting closer to scope-creep on positivity's behalf