Rewrite inside BigOperators

Stream: new members

[Bernardo Borges]

When manipulating proofs that involve BigOperators, such as ∑, many of the terms will involve the index i. For example, I would like to understand how you would point the rw to the terms ys i and xs i, when we won't have i in the context:

import Mathlib.Data.Fin.Tuple.Reflection

open BigOperators

example
  (A : ℕ)
  (xs ys : Fin n → ℕ)
  (h : A ≤ ∑i,(xs i + ys i))
  : A ≤ ∑i,(ys i + xs i) := by
  rw [add_comm (ys i) (xs i)]
  -- unknown identifier 'i'
  assumption
  done

Should you intro? Declare a fun i =>? This is a more general question, because I will be manipulating Sums a lot. Thanks in advance!

[Johan Commelin]

You can use simp_rw. And just use an _ instead of the i.

[Bernardo Borges]

Oh. In this case the _ leaves a hole for Lean to complete?

[Bernardo Borges]

Looks good, thanks!

[Notification Bot]

Bernardo Borges has marked this topic as resolved.

[Notification Bot]

Ralf Stephan has marked this topic as unresolved.

[Ralf Stephan]

This works for me only up to the point, where properties of the bound variable come into play.

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

example : (∏ p ∈ Icc (1 : ℕ) 5, (∑' k : ℕ, (p ^ k : ℝ)⁻¹)) =
    (∏ p ∈ Icc (1 : ℕ) 5, ((p : ℝ) / (p - 1))) := by
  have h (p' : ℕ) (hp : p' ∈ Icc 1 5) : p' ≠ 0 := by sorry
  simp_rw [(inv_div (_ - 1 : ℝ) (_ : ℝ)).symm, sub_div]
  simp_rw [div_self (h _)]
--  rw [one_div, ←tsum_geometric_of_lt_one]
  sorry

Here the first simp_rw is fine, but for the second, div_self needs a proof that _ is nonzero, which I tried to give with h. What mistake did I make? How can I refer to the fact that p was declared ∈ Icc 1 5 under the product?

[Yaël Dillies]

After #11563, you will be able to do ∏ hp : p ∈ Icc 1 5, .... Before that, you have to do ∑ p : Icc 1 5, ...

[Michael Stoll]

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

example : (∏ p ∈ Icc (1 : ℕ) 5, (∑' k : ℕ, (p ^ k : ℝ)⁻¹)) =
    (∏ p ∈ Icc (1 : ℕ) 5, ((p : ℝ) / (p - 1))) := by
  have h (p' : ℕ) (hp : p' ∈ Icc 1 5) : p' ≠ 0 := by sorry
  simp_rw [(inv_div (_ - 1 : ℝ) (_ : ℝ)).symm, sub_div]
  have : ∏ x ∈ Icc (1 : ℕ) 5, (x / x - 1 / x : ℝ)⁻¹ = ∏ y ∈ Icc (1 : ℕ) 5, (1 - 1 / y : ℝ)⁻¹ := by
    refine Finset.prod_congr rfl fun x hx ↦ ?_
    rw [div_self (by exact_mod_cast h x hx)]
  rw [this]
  sorry

is one possibility. The various ...congr lemmas allow you to use information like your variable is in the given (fin)set.

[Alex Brodbelt]

I'm struggling to rewrite within a sum and was wondering what other things can I try?

Before the sorry I want to convert
(1 / 2) ^ (x * 2) / (1 / 2) ^ (x + 1)
to
(1/2) ^(x - 1)

import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Data.Real.Basic

open Real BigOperators Finset Field

theorem part_b : ∃ x : ℕ → ℝ, (∀ i, x i > 0) ∧ (∀ i, x (i + 1) ≤ x i) ∧ (x 0 = 1) ∧ (∀ N, (∑ n ∈ range N, ((x n)^2 / (x (n + 1)))) < 4) := by
  let x : ℕ → ℝ := fun n => (1 / 2)^n
  use x
  constructor
  · intro i
    apply pow_pos (by norm_num) i
  constructor
  · intro i
    apply pow_le_pow_of_le_one
    · norm_num
    · rw [one_div_le (by norm_num) (by norm_num), div_one]; norm_num -- why does norm_num or linarith not work here?
    · apply Nat.le_succ
  constructor
  · rfl
  intro N
  dsimp [x]
  simp_rw [← pow_mul]
 -- simp_rw [div_eq_mul_inv ((1 / 2) ^ (x * 2)) _, ← pow_sub] --lean is not happy with these rewrites
  sorry

I was also trying to make a helper lemma

lemma helper {x : ℕ} (hx : 1 ≤ x): (1 / 2 : ℝ) ^ (2 * x) / (1 / 2 : ℝ) ^ (x + 1) = (1 / 2 : ℝ)^(2 * x - (x + 1)) := by
  calc (1 / 2 : ℝ) ^ (2 * x) / (1 / 2 :  ℝ ) ^ (x + 1) = (1 / 2 : ℝ) ^ (2 * x - (x + 1)) := by rw [div_eq_mul_inv, ← pow_sub (a := (1 / 2)) (m := 2 * x) (n := x + 1)]

I have tried moogle and leansearch, but have had no success so far, I feel like it should be easy to do this computation and that there should be some tactic which I don't know how to use which should make this easy to do...

[Kyle Miller]

Re "why does norm_num not work here", you can use linarith, which knows how to prove inequalities. I think 1 / 2 ≤ 1 should be in the purview of norm_num though.

[Kyle Miller]

Here's some progress:

theorem part_b : ∃ x : ℕ → ℝ, (∀ i, x i > 0) ∧ (∀ i, x (i + 1) ≤ x i) ∧ (x 0 = 1) ∧ (∀ N, (∑ n ∈ range N, ((x n)^2 / (x (n + 1)))) < 4) := by
  let x : ℕ → ℝ := fun n => (1 / 2)^n
  use x
  constructor
  · intro i
    apply pow_pos (by norm_num) i
  constructor
  · intro i
    apply pow_le_pow_of_le_one
    · norm_num
    · linarith
    · apply Nat.le_succ
  constructor
  · rfl
  intro N
  dsimp [x]
  simp_rw [← pow_mul]
  convert_to (∑ x ∈ range N, (1/2) ^(x - 1) : ℝ) < 4 using 2
  rw [div_eq_mul_inv]
  -- ⊢ (1 / 2) ^ (x✝ * 2) * ((1 / 2) ^ (x✝ + 1))⁻¹ = (1 / 2) ^ (x✝ - 1)
  sorry

[Kyle Miller]

The convert_to tactic is useful for saying "I want to make the expression look like this; give me the difference". The using clause is to control how far to strip away like terms.

[Kyle Miller]

pow_sub doesn't apply here because it's for multiplicative groups, but the reals aren't a multiplicative group.

[Kyle Miller]

pow_sub₀ works though

[Alex Brodbelt]

Kyle Miller said:

Re "why does norm_num not work here", you can use linarith, which knows how to prove inequalities. I think 1 / 2 ≤ 1 should be in the purview of norm_num though.

I tried linarith as well and it fails too, which I thought was strange - but there could be something wrong with my version of lean. It has been acting up lately whenever I try start a new project using mathlib

[Kyle Miller]

Oh, you know what, norm_num works for me here. I didn't test it because I trusted the comment.

[Kyle Miller]

I'm on a version of mathlib from august 15, in case that helps.

[Alex Brodbelt]

Kyle Miller said:

Oh, you know what, norm_num works for me here. I didn't test it because I trusted the comment.

How can I check the version?
Something is weird, neither linarith or norm_num work for me there...

[Kevin Buzzard]

Are you working in mathlib itself or a project which has mathlib as a dependency?

[Alex Brodbelt]

Kevin Buzzard said:

Are you working in mathlib itself or a project which has mathlib as a dependency?

I'm working with mathlib as a dependency

[Kevin Buzzard]

Then you can look in your manifest file to see which mathlib commit you're using. Alternatively fire up a terminal, change directory to .lake/packages/mathlib and then do git log to see the date of the last commit.

[Alex Brodbelt]

I was working on part b for a q3 of the 1982 IMO (working on part a at the minute) and was wondering if there is a more idiomatic way to use sums over ranges or even Icc? what do more experienced users use when trying to formalise this sort of problem?
Once I have finished part a how can I add this to the archive of formalised IMO problems?

import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.GeomSum

open Real BigOperators Finset Field Nat Preorder

theorem part_b : ∃ x : ℕ → ℝ,
                (∀ i, x i > 0) ∧
                (∀ i, x (i + 1) ≤ x i) ∧ (x 0 = 1) ∧
                (∀ N, (∑ n ∈ range (N + 1), ((x n)^2 / (x (n + 1)))) < 4)
                := by
  let xₙ : ℕ → ℝ := fun n => (1/2)^n
  use xₙ
  constructor
  · intro i
    apply pow_pos (by norm_num) i
  constructor
  · intro i
    apply pow_le_pow_of_le_one (by norm_num)
    · rw [one_div_le (by norm_num) (by norm_num), div_one]; norm_num
    · apply Nat.le_succ
  constructor
  · rfl
  intro N
  dsimp [xₙ]
  rw [
    Finset.sum_eq_sum_diff_singleton_add (s := range (N + 1)) (i := 0) (Finset.mem_range.mpr (by linarith)),
    pow_zero, zero_add, one_pow, pow_one, one_div_one_div, add_comm
    ]
  convert_to (2 + ∑ n ∈ range (N), (1/2) ^ n : ℝ) < 4 using 2
  induction' N with k hk
  case zero =>
    simp only [
      zero_add, range_one, sdiff_self, bot_eq_empty, one_div, inv_pow, div_inv_eq_mul,
      sum_empty, range_zero
      ]
  case succ =>
    rw [
      Finset.sum_range_succ, ← hk, Finset.range_add_one
      ]
    simp only [
      one_div, inv_pow, div_inv_eq_mul, singleton_subset_iff, mem_insert, self_eq_add_left,
      AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_range, lt_add_iff_pos_left,
      add_pos_iff, zero_lt_one, or_true, sum_sdiff_eq_sub, lt_self_iff_false, not_false_eq_true,
      sum_insert, sum_singleton, pow_zero, one_pow, inv_one, zero_add, pow_one, one_mul
      ]
    rw [
      ← pow_mul, mul_comm, ← inv_pow
      ]
    nth_rewrite 1 [← inv_inv 2]
    rw [
      mul_comm, inv_pow 2⁻¹, ← pow_sub₀ (a := 2⁻¹) (ha := by norm_num) (h := by linarith), add_mul,
      one_mul, add_assoc, one_add_one_eq_two, mul_comm k 2, two_mul, add_assoc,
      Nat.add_sub_assoc (by linarith), Nat.sub_self, add_zero, inv_pow, add_sub_assoc, add_comm
    ]
  rw [
    geom_sum_eq (by norm_num), half_sub, div_neg, div_eq_inv_mul, one_div, inv_inv,
    mul_comm, ← neg_mul, neg_sub
    ]
  have h₀ : (1 - (2 : ℝ)⁻¹ ^ N) < 1 := by apply sub_lt_self; apply pow_pos (by norm_num)
  linarith [h₀]
  done

[Kevin Buzzard]

Once I have finished part a how can I add this to the archive of formalised IMO problems?

Just make a PR like you would for any changes to mathlib.