start proof

Stream: new members

[Yujie Wang]

Hi guys, I'm trying to do this proof, I just define the k here, but I'm not sure how to express the rest part, maybe could you give me some advice or examples please? Thank you sooooo much!!!

For any 1 ≤ k < n, we have |x1 + x2 + · · · + xk| + |xk+1 + · · · + xn| ≤ X.
When n is odd:

When n is even:

image.png

  theorem test_1 (n : ℕ) (hn : 3 ≤ n) (x y : ℕ → ℝ)
  (hx : ∀ i, x i ≠ 0)
  (h : ∀ k : ℕ, 1 ≤ k ∧ k < n →
    |∑ i in Finset.Icc 1 k, x i| + |∑ i in Finset.Icc (k+1) n, x i| =
    |∑ i in Finset.Icc 1 k, y i| + |∑ i in Finset.Icc (k+1) n, y i|) :
  IsGreatest {M : ℝ | M = (∑ i in Finset.Icc 1 n, |y i|) / (∑ i in Finset.Icc 1 n, |x i|)} M ∧
  (Odd n → M = n) ∧
  (Even n → M = n - 1) := by{

    have h1 : ∀ k ∈ Finset.Ico 1 n, 1 ≤ k ∧ k < n := by{
      intro k hk
      rw [Finset.mem_Ico] at hk
      cases hk with
      | intro hk_left hk_right =>
      --cases hk with h_left h_right,
      constructor;
      { exact hk_left };  -- prove 1 ≤ k
      { exact hk_right } -- prove k < n
    }

    let x:


    sorry
  }

[Ruben Van de Velde]

If you want to use a different proof for n even or odd, you can write cases n.even_or_odd

[Ruben Van de Velde]

But note that you haven't proved the statement in line 2, and I'm not convinced M means what you intend to

[Yujie Wang]

Hi thank you Ruben! hereM = (|y_1| + |y_2| + ... + |y_n|) / (|x_1| + |x_2| + ... + |x_n|)

[Yujie Wang]

Actually the question for this is```
/- Problem: For integers n ≥ 3, given two sequences {x_n}, {y_n} satisfying:

1. x_i ≠ 0 for 1 ≤ i ≤ n,
2. For any 1 ≤ k < n, |x_1 + ... + x_k| + |x_{k+1} + ... + x_n|
   = |y_1 + ... + y_k| + |y_{k+1} + ... + y_n|,
   Find the maximum value of:
   M = (|y_1| + |y_2| + ... + |y_n|) / (|x_1| + |x_2| + ... + |x_n|)
   Prove:

• M = n when n is odd,
• M = n - 1 when n is even. -/