Splitting a sum / series convergence

Stream: new members

[Nathan]

I'm having trouble with these sorrys.

• I have a sum over Finset 1 k and I just need to break out the k'th term.
• Is there a theorem in mathlib I can use to show that b_k is eventually constant since it's bounded below and nonincreasing?

import Mathlib

theorem USAMO_2007_1 (n : ℤ) (hn : n > 0) (a : ℤ → ℤ) (ha₁ : a 1 = n)
    (ha₂ : ∀ k, k > 1 → 0 ≤ a k ∧ a k ≤ k - 1 ∧ k ∣ ∑ i : Finset.Icc 1 k, a i) :
    ∃ N l, ∀ k, k > N → a k = l := by
  have ha₃ : ∀ k : ℤ, k > 0 → 0 ≤ a k ∧ k ∣ ∑ i : Finset.Icc 1 k, a i := by
    intro k kh
    by_cases ko : k = 1
    · simp[ko, ha₁]; grind
    replace ko : k > 1 := by grind
    let t := ha₂ k ko; exact ⟨t.left, t.right.right⟩
  replace ha₂ : ∀ k, k > 1 → a k ≤ k - 1 := by
    intro k kh; exact (ha₂ k kh).right.left
  let b := fun k : ℤ => (∑ i : Finset.Icc 1 k, a i) / k
  have hb : ∀ k, k > 0 → k * b k = ∑ i : Finset.Icc 1 k, a i := by
    intro k kh; unfold b
    let ⟨_, ⟨j, jh⟩⟩ := ha₃ k kh
    rw[jh]; simp; by_cases c : k = 0
    · right; assumption
    · left; simp[c]

  have b_bound : ∀ k, k > 0 → 0 < b k := by
    intro k kh; unfold b
    suffices suff : 0 < (∑ i : Finset.Icc 1 k, a i) from by
      let ⟨_, ⟨j, jh⟩⟩ := ha₃ k kh
      rw[jh] at suff
      exact calc
        0 < j := by
          rcases (pos_and_pos_or_neg_and_neg_of_mul_pos suff) with c1 | c2
          · exact c1.right
          · exfalso; grind
        _ = (∑ i : Finset.Icc 1 k, a i) / k := by
          rw[jh]
          refine Int.eq_ediv_of_mul_eq_right ?_ rfl
          exact Ne.symm (Int.ne_of_lt kh)
    refine Finset.sum_pos' ?_ ?_
    · intro i ih
      have := (Finset.mem_Icc.mp i.prop).left
      exact (ha₃ i this).left
    · have : 1 ∈ Finset.Icc 1 k := by simp; grind
      exists ⟨1, this⟩
      simp[ha₁, hn]
  have b_noninc : ∀ k, k > 1 → b k ≤ b (k - 1) := by
    intro k kh
    have kh₂ : k > 0 := by grind
    have := calc (k-1) * b k
      _ < k * b k := by
        suffices suff : k - 1 < k from by
          refine Int.mul_lt_mul_of_pos_right suff ?_
          refine b_bound k ?_
          grind
        simp
      _ = ∑ i : Finset.Icc 1 k, a i := hb k kh₂
      _ = (∑ i : Finset.Icc 1 (k-1), a i) + a k := sorry
      _ = (k-1) * b (k-1) + a k := by
        have : k-1 > 0 := by grind
        rw[hb (k-1) this]
      _ ≤ (k-1) * b (k-1) + (k - 1) := by simp[Int.add_le_add_left (ha₂ k kh)]
      _ = (k-1) * (b (k-1) + 1) := by linarith
    replace : b k < b (k-1) + 1 := by
      refine (Int.mul_lt_mul_left ?_).mp this
      simp[kh]
    exact (Int.add_le_add_iff_right 1).mp this
  have b_const : ∃ N l, ∀ k, k ≥ N → b k = l := sorry
  let ⟨N, l, ch⟩ := b_const
  exists (if N ≥ 1 then N else 1), l; intro k kh
  exact calc a k
    _ = (∑ i : Finset.Icc 1 k, a i) - (∑ i : Finset.Icc 1 (k-1), a i) := sorry
    _ = k * b k - (k-1) * b (k-1) := by
      have : k > 1 := by
        by_cases c : N ≥ 1 <;> simp[c] at kh <;> grind
      have kh₁ : k > 0 := by grind
      have kh₂ : k - 1 > 0 := by grind
      rw[hb k kh₁, hb (k-1) kh₂]
    _ = k * l - (k-1) * l := by
      have kh₁ : k ≥ N := by
        by_cases c : N ≥ 1 <;> simp[c] at kh <;> grind
      have kh₂ : k - 1 ≥ N := by
        by_cases c : N ≥ 1 <;> simp[c] at kh <;> grind
      rw[ch k kh₁, ch (k-1) kh₂]
    _ = l := by linarith

[David Ledvinka]

Being non-increasing and bounded below implies the sequence converges by monotone convergence (see tendsto_atTop_ciInf) it does not imply the sequence is eventually constant. Consider a_n = 1/n.

[Aaron Liu]

well if it's a sequence of integers then it's eventually constant

[Aaron Liu]

since the integers are discrete so all convergent sequences are eventually constant

[David Ledvinka]

oh my bad I was not paying close enough attention to see that b was a sequence of integers.

[David Ledvinka]

That gives you one proof strategy though. As far as I could tell the fact Aaron mentions is missing from mathlib (but should be in it).

[Aaron Liu]

here we go

  have b_const : ∃ N l, ∀ k, k ≥ N → b k = l := by
    -- sequence indexed by nat so we can be globally antitone and bounded below
    let f' (n : Nat) : Int := b (n + 1)
    have anti : Antitone f' := antitone_nat_of_succ_le fun n => by
      refine (congrArg₂ (fun u v => b u ≤ b v) ?_ ?_).mpr (b_noninc (n + 2) (by omega))
      · lia
      · lia
    have bdd : BddBelow (Set.range f') := by
      use 0
      intro z hz
      obtain ⟨n, rfl⟩ := hz
      exact (b_bound (n + 1) (by lia)).le
    -- monotone convergence
    have tendsto := tendsto_atTop_ciInf anti bdd
    rw [nhds_discrete] at tendsto
    have const := Filter.EventuallyConst.of_tendsto tendsto
    rw [Filter.eventuallyConst_atTop] at const
    obtain ⟨n, hn⟩ := const
    use n + 1, f' n
    intro k hk
    lift k to ℕ using by lia
    obtain ⟨k, rfl⟩ : ∃ k', k = k' + 1 := Nat.exists_eq_add_one.2 (by lia)
    exact mod_cast hn k (by lia)

[Nathan]

thanks, what is lia?

[Aaron Liu]

docs#Lean.Parser.Tactic.lia

`lia` solves linear integer arithmetic goals.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
Please use `grind` instead if you need additional capabilities.

[Nathan]

what about the sums? I can't seem to figure out how to do it

[Nathan]

ah nevermind, i figured it out