Rewriting an inequality under a binder

Stream: general

[Konstantin Weitz]

I'm trying to prove this goal, but I'm struggeling to rewrite under the sum. How do I do this?

∀ x, metric x n ≤ c * metric x 0
⊢ metric x 0 / ∑ x, metric x 0 ≤ c * metric x 0 / ∑ x, metric x n

[Aaron Liu]

rw can't rewrite terms with bound variables, the solution is to use simp_rw or conv.

[Konstantin Weitz]

Sorry, I've tried using these tactics, but I can't get them to work. Maybe they don't work well with inequalities? Are there specific lemmas around Finset.sum that I could use?

[Konstantin Weitz]

This lemma looks promising: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/BigOperators/Group/Finset.html#Finset.sum_le_sum

[Robin Arnez]

can you give an #mwe?

[Konstantin Weitz]

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0BBdAcwFMsokcAhYQgeTGPJmgGccAFYAKFElkRQZsOACIoKAJWJJ0VJC2ABjLl3TEQIJHDUg4ACgAaALgAqATwYBKOAG0AYsAB2MC8TgGAuvoBmR93ABaAD44ADkUQJDAXEI4awAPLjg4RTg/PUAAIjg4gBo4byy4RzhAEyJkuAAqPIKABmtguESquLhquAB6OEBEIizc/ObW0pTKvpb2rp6mwtSAXi4sM0aWaCgFlSA

import Mathlib.Algebra.BigOperators.Pi
import Mathlib.Data.Real.Basic

lemma lem (X:Type) [Fintype X] (f: X -> Nat -> ℝ ) x
  c : (∀ x, f x n ≤ c * f x 0) ->
  f x 0 / ∑ x, f x 0 ≤ c * f x 0 / ∑ x, f x n :=
by
  sorry

[Robin Arnez]

Does a counterexample work as well? :-)

import Mathlib.Analysis.RCLike.Basic

lemma lem' : ∃ (X : Type) (_ : Fintype X) (f : X -> Nat -> ℝ) (x : X) (n : Nat)
    (c : ℝ) (_ : ∀ x, f x n ≤ c * f x 0), ¬f x 0 / ∑ x, f x 0 ≤ c * f x 0 / ∑ x, f x n := by
  use Unit, inferInstance, (fun a n => if n = 0 then -3 else -4), (), 1, -1, ?_
  · norm_num
  · norm_num

[Robin Arnez]

For something more useful, here is a proof of your statement with a few (hopefully reasonable?) side conditions:

import Mathlib

-- f x = metric x n
-- g x = metric x 0
example (f : Fin 10 → ℝ) (g : Fin 10 → ℝ) (c : ℝ) (h : ∀ x, f x ≤ c * g x) (h' : ∀ x, 0 < f x) (h'' : 0 < c) :
    g x / ∑ x, g x ≤ c * g x / ∑ x, f x := by
  simp only [div_eq_mul_inv]
  rw [mul_comm c, mul_assoc]
  apply mul_le_mul_of_nonneg_left
  · rw [← div_le_iff₀' h'']
    rw [div_eq_mul_inv, ← mul_inv]
    apply inv_anti₀
    · apply Fintype.sum_pos
      exact lt_of_strongLT h'
    · rw [Finset.sum_mul]
      apply Finset.sum_le_sum
      intro x _
      rw [mul_comm]
      exact h x
  · have := le_trans (le_of_lt (h' x)) (h x)
    rwa [← div_le_iff₀' h'', zero_div] at this

[Aaron Liu]

Why Fin 10?

[Robin Arnez]

just some arbitrary Fintype..?

[Robin Arnez]

don't ask

[Robin Arnez]

:)

[Aaron Liu]

What if I want to apply it to Fin 37?

[Konstantin Weitz]

@Robin Arnez Thank you!