Maximum Term Method Help

Stream: Is there code for X?

[Max Bobbin]

I'm working on proving the maximum term method, but I keep getting to a point where I get stuck. I'm starting to think there may be a flaw in how I wrote the theorem and wanted to get feedback. My idea for the proof was by induction on n, but I get to an unsolvable goal. I've also experimented with either using just n or n.succ but neither variation seems to make much difference for the proof.

import algebra.big_operators.order
import tactic.ring

open finset
open_locale big_operators

theorem finset.mem_le_pos_sum {β : Type*} [linear_ordered_add_comm_group β] (n : ℕ) (f : ℕ → β) (h1 : ∀ x, x ∈ (finset.range n) → 0 < f x)

:  ∀ y ∈ (finset.range n), f y ≤ ∑ x in (finset.range n), f x :=

[Yaël Dillies]

You should generalise to any finset, not just finset.range n, and do induction on the finset itself rather than its cardinality.

[Max Bobbin]

I think the generalized form would look like this.

theorem finset.mem_le_pos_sum {α : Type*} {β : Type*} [linear_ordered_add_comm_group β] (f : α → β) (s : finset α) (h1 : ∀ x, x ∈ s → 0 < f x)
:  ∀ y (H : y ∈ s), f y ≤ ∑ x in s, f x :=

And then you mean do induction s as the first step?

[Junyan Xu]

Just use docs#finset.sum_eq_add_sum_diff_singleton and docs#finset.sum_nonneg

[Kevin Buzzard]

If you go via Yael's route, use the bespoke induction principle docs#finset.induction_on .

[Junyan Xu]

Actually you can directly apply docs#finset.single_le_sum

[Max Bobbin]

Thank you for the help! I imagined the code already existed in some form, but it was just a matter of finding the exact wording