gcongr, forall, and positivity

Stream: mathlib4

[Sébastien Gouëzel]

Sometimes, when using gcongr for sums or products, I end up with side goals of the form ∀ i, 0 ≤ ‖f i‖ or ∀ i ∈ s, 0 ≤ ‖f i‖. They are shown to me because positivity can not solve them (it's not really in its scope), but still I find it a little bit sad. Should this be special-cased in gcongr or positivity?

[Yaël Dillies]

I would personally be very much in favour of that

[Geoffrey Irving]

bound should work for some of them already, but +1 to extending gcongr.

[Geoffrey Irving]

(aesop by default does intros, if I’m remembering correctly)

[Heather Macbeth]

@Alex J. Best wrote positivity extensions for sums and products for Terry Tao's symmetric polynomials project:
https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/positivity_ext.lean
I don't know if they ever made it to Mathlib, but they should!

[Jireh Loreaux]

This works:

import Mathlib

example {E ι : Type} [NormedAddCommGroup E] [Fintype ι] (f : ι → E) : 0 ≤ ∑ i, ‖f i‖ := by positivity

[Heather Macbeth]

Ah indeed: docs#Mathlib.Meta.Positivity.evalFinsetSum, from #10538.

[Heather Macbeth]

Given that that's there, I wonder why Sébastien is encountering side goals like

∀ i, 0 ≤ ‖f i‖ or ∀ i ∈ s, 0 ≤ ‖f i‖.

?

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

He could be working over finsums and Finite as opposed to finset sum. Or the TODO in the docstring of the extension

[Sébastien Gouëzel]

MWE:

import Mathlib
lemma foo (n : ℕ) (f g : Fin n → ℝ) (h : ∀ i, ‖f i‖ ≤ ‖g i‖) :
    ∏ i, ‖f i‖ ≤ ∏ i, ‖g i‖ := by
  gcongr with i hi
  · exact fun j hj ↦ by positivity
  exact h i

Here the side goal is not discharged automatically.

[Heather Macbeth]

It looks like gcongr is doing too much here, so positivity doesn't fire: rather than producing the side goal 0 ≤ ∏ i : Fin n, ‖f i‖ (as I would expect) it is producing the side goal ∀ i ∈ Finset.univ, 0 ≤ ‖f i‖.

[Heather Macbeth]

I'm a little surprised by this! I'll dig into the code.

[Yaël Dillies]

Heather, I think you are forgetting that some boundedness/nonemptiness condition is needed for ⨅ i, f i to be monotone in f.

[Yaël Dillies]

... or are you saying it should use the fact that Fin n is finite in a more fundamental way?

[Heather Macbeth]

In fact I was overthinking this: in my head the side condition for the @[gcongr] lemma was 0 ≤ ∏ i, ‖f i‖ (which indeed would have required the positivity extension for products), whereas it actually is ∀ i, 0 ≤ ‖f i‖ (which is solved by intros plus OG positivity.)

I also remembered that this feature had been requested before. I tried it out on mathlib and it seems harmless and mildly useful, so I have PR'd it! #16747

[Yaël Dillies]

Can't wait for the proofs in APAP to lose many lines :tada:

[Sébastien Gouëzel]

Thanks!