(∑ i ∈ s, f i) / (∑ i ∈ s, g i) ≤ max i ∈ s, (f i / g i)

Stream: Is there code for X?

[Snir Broshi]

A sum over a sum (with the same number of terms) is bounded between the minimum and maximum ratio.
The proof is to start with f j / g j ≤ max i ∈ s, (f i / g i), multiply by the g j, sum the inequality over all j, then take the max out of the sum and divide by the sum of gs. Similarly for min.

[Snir Broshi]

import Mathlib

theorem foo_le_max {ι : Type*} {s : Finset ι} (f : ι → ℝ) (g : ι → ℝ)
    (hs : s.Nonempty) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 < g i) :
    (s.sum f / s.sum g :) ≤ (s.image <| f / g).max' (hs.image _) := by
  classical
  have ⟨i, hi⟩ := hs
  apply div_le_of_le_mul₀ (Finset.sum_pos hg hs).le <|
    div_nonneg (hf i hi) (hg i hi |>.le) |>.trans <|
      Finset.le_max' _ _ <| Finset.mem_image_of_mem (f / g) hi
  rw [Finset.mul_sum]
  refine Finset.sum_le_sum fun i hi ↦ div_le_iff₀ (hg i hi) |>.mp ?_
  exact Finset.le_max' _ _ <| Finset.mem_image_of_mem (f / g) hi

[Snir Broshi]

What's the most generality possible here? I tried abstracting reals away and using [Field M] [LinearOrder M] but it didn't work so great. I wonder if a version for Rings is possible by somehow avoiding division.

[Snir Broshi]

Also, this is equivalent to a (more familiar?) weighted average version:
(∑ i ∈ s, w i * x i) / (∑ i ∈ s, w i) ≤ max i ∈ s, x i

[Aaron Liu]

but surely this isn't specific to division?

[Aaron Liu]

this feels like some sort of jensen's inequality

[Snir Broshi]

Jensen can prove the weighted version where the sum of the weights is 1

[Snir Broshi]

No actually it might be just normal inequalities, I don't see any convex function we can define here

[Aaron Liu]

the convex function is division

[Aaron Liu]

I think that's convex?

[Snir Broshi]

Division by a constant?

[Aaron Liu]

division as a function of two variables

[Aaron Liu]

I think it's convex on the first quadrant

[Snir Broshi]

Oh that makes sense

[Snir Broshi]

Though the proof above is easier probably

[Aaron Liu]

I don't see a theorem saying division is convex

[Aaron Liu]

I'll try proving it for the real numbers

[Aaron Liu]

ahh, division isn't convex

[Aaron Liu]

I guess I sort of expected it, since simpson's paradox is a thing

[Snir Broshi]

Simpsons paradox is that division isn't convex?

[Snir Broshi]

Something something Bayes?

[Aaron Liu]

maybe???

[Aaron Liu]

idk if they're actually related it just felt similar

[Snir Broshi]

hmm I agree

[Snir Broshi]

So since division isn't convex, Jensen's isn't a generalization of this lemma. What is?

[Aaron Liu]

well although division isn't convex as a function of two variables, it becomes convex if you fix either one of the arguments

[Aaron Liu]

so maybe we can still get something here?

[Artie Khovanov]

Snir Broshi said:

What's the most generality possible here? I tried abstracting reals away and using [Field M] [LinearOrder M] but it didn't work so great. I wonder if a version for Rings is possible by somehow avoiding division.

If you want an ordered field, you want [Field M] [LinearOrder M] [IsStrictOrderedRing M]

[Yaël Dillies]

Snir Broshi said:

So since division isn't convex, Jensen's isn't a generalization of this lemma. What is?

$\|fg\|_{L^1} \le \|f\|_{L^1}\|g\|_{L^\infty}$

[Snir Broshi]

Interesting, this might work for Finsupp, and maybe continuous functions on a compact domain. Is this a known inequality? It looks similar to Hölder

[Yaël Dillies]

This is as general as I wrote it: It works for any L^1 function f and L^infty function g. It is technically Hölder for L^1-L^infty, but at least in additive combinatorics it is usually referred to as "taking g out".

[Snir Broshi]

IIUC since it's for all functions, the norms would be EReal rather than reals?
Is it in Mathlib?

[Yaël Dillies]

The inequality I stated above is an informal one. There are many formal versions one could write

[J. J. Issai (project started by GRP)]

Snir Broshi said:

A sum over a sum (with the same number of terms) is bounded between the minimum and maximum ratio.
The proof is to start with f j / g j ≤ max i ∈ s, (f i / g i), multiply by the g j, sum the inequality over all j, then take the max out of the sum and divide by the sum of gs. Similarly for min.

Note that this is a mild generalization of 'mediant sum': for positive reals (elements of an ordered ring where one can construct a domain of fractions) a,b,c,d with ad <= bc ( so a/c <= b/d ) one has a(c+d) <= c(a+b) (so a/c <= (a+b)/(c+d) ) and analogously for b/d. For finite sums I think an inductive proof on the number of summands is easier to understand and program. Also, by rearranging the terms in the numerator, one can try crafting tighter bounds on the end result. I would be interested in knowing whether this approach is better in terms of performance than Snir's approach above.~~

(I suspect this may apply to lattice ordered rings, but I don't know if one can make a 'nicely ordered' field of fractions out of such a ring.)~~

[Ilmārs Cīrulis]

$\|fg\|_{L^1} \le \|f\|_{L^1}\|g\|_{L^\infty}$ - is there any chance for this to be true, if one replaces $\infty$ with bounded real number $1 \le p$?

Or, after getting rid of root, this:

import Mathlib

lemma T {ι : Type*} (s : Finset ι) {f g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) :
    s.sum (fun i => f i * g i) ^ p ≤ (s.sum f) ^ p * s.sum (fun i => g i ^ p) := by
  sorry

Apologies for the disturbance. If there's a counterexample to such statement, I would be very grateful. :pray:

[Aaron Liu]

holder inequality (says $\|fg\|_{L^1} \le \|f\|_{L^p} \|g\|_{L^q}$ whenever $1/p + 1/q = 1$) is tight when $|f|^p$ and $|g|^q$ are linearly dependent

[Ilmārs Cīrulis]

Ilmārs Cīrulis said:

import Mathlib

lemma T {ι : Type*} (s : Finset ι) {f g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) :
    s.sum (fun i => f i * g i) ^ p ≤ (s.sum f) ^ p * s.sum (fun i => g i ^ p) := by
  sorry

I managed to prove it. That's good too.

[Yaël Dillies]

Aaron Liu said:

holder inequality (says $\|fg\|_{L^1} \le \|f\|_{L^p} \|g\|_{L^q}$ whenever $1/p + 1/q = 1$) is tight when $|f|^p$ and $|g|^q$ are linearly dependent

Tightness only holds when $p, q < \infty$