Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ↑(Fintype.card ι) * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i := by

Mathlib declaration: Antivary.card_mul_sum_le_sum_mul_sum
Held-out module: Mathlib.Algebra.Order.Chebyshev
Banned modules (itself + downstream): 7
Reference proof premises (reachable / held-out): 1 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00053

Attempts

sample 0 · round 0Lean 3 syntax22.0 s model time

Proof

intro hfg
let n := Fintype.card ι
let s_f := ∑ i, f i
let s_g := ∑ i, g i
let s_fg := ∑ i, f i * g i
have h1 : ∀ i j, f i * g j + f j * g i ≤ f i * g i + f j * g j :=
  by intro i j; rw [add_comm]; apply (hfg i j)
let h2 : ∀ i j, f i * g j + f j * g i ≤ f i * g i + f j * g j :=
  by intro i j; exact h1 i j
let h3 : (∑ i, ∑ j, f i * g j) + (∑ i, ∑ j, f j * g i) ≤
  (∑ i, ∑ j, f i * g i) + (∑ i, ∑ j, f j * g j) :=
  by { rw [sum_add_distrib, sum_add_distrib], apply sum_le_sum; intro i j; exact h2 i j }
let h4 : (∑ i, ∑ j, f i * g j) = (∑ i, ∑ j, f j * g i) :=
  by { rw [sum_swap], apply congr_arg _ (congr rfl); apply sum_cong; intro j; rw [sum_swap]; apply congr_arg _ (congr rfl); intro i; refl }
let h5 : ∑ i, ∑ j, f i * g j = n * s_fg :=
  by { rw [h4], apply congr_arg _ (congr rfl); apply sum_cong; intro i; rw [sum_swap]; apply congr_arg _ (congr rfl); intro j; rw [sum_swap]; apply congr_arg _ (congr rfl); intro k; refl }
let h6 : ∑ i, ∑ j, f j * g i = n * s_fg :=
  by { rw [h4], apply congr_arg _ (congr rfl); apply sum_cong; intro i; rw [sum_swap]; apply congr_arg _ (congr rfl); intro j; rw [sum_swap]; apply congr_arg _ (congr rfl); intro k; refl }
let h7 : (∑ i, ∑ j, f i * g j) + (∑ i, ∑ j, f j * g i) = 2 * n * s_fg :=
  by { rw [h5, h6], apply congr_arg _ (congr rfl); rw [add_assoc]; rw [add_comm]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul]; rw [add_assoc]; rw [add_left_cancel]; rw [mul_add]; rw [add_mul];......

What Lean printed (this is all the model sees on repair)

15:46: error: unexpected token ','; expected '}'

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. one is monotone, the
other is antitone), the product of their sum is less than the size of the set times their scalar
product. -/
theorem Antivary.card_mul_sum_le_sum_mul_sum (hfg : Antivary f g) :
    Fintype.card ι * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i :=
  (hfg.antivaryOn _).card_mul_sum_le_sum_mul_sum