New to Lean and MATHLIB4

Stream: new members

[Jason Mahaffey]

There is much to absorb in the community. I am a hobby math enthusiast (M.S. Math) and would like to contribute to the effort. The new AI is making coding in Lean much more accessible for people like me. I have a fully compiled (no sorry, no axiom, just a definition for the recurring coefficient) version of the Waring formula for A^n+B^n=... but I don't want to contribute to the A.I. slop "crises". I used the Mathlib4 library search tool and did not see the theorem. Would this be a valuable contribution and if so, what group would be a good contact before submitting a PR?

[Jason Mahaffey]

Code snippet:**-- The Waring formula with division (in a Field) -/
theorem waring_formula {R : Type*} [Field R] [CharZero R] (A B : R) (p : ℕ) (hp : 0 < p) :
    A^p + B^p = (A + B)^p + ∑ j ∈ Finset.Icc 1 (p / 2),
      (-1 : R)^j * ((p : R) * (Nat.choose (p - j - 1) (j - 1) +
      Nat.choose (p - j - 1) j) / (p - j : R)) * (A + B)^(p - 2 * j) * (A * B)^j**

[Matt Diamond]

welcome! please use #backticks when posting code (and also read #mwe)

[Jason Mahaffey]

Sorry for that. here is the mwe and I have updated the format of the formula to make it more useable.

PastedText.txt

[Jason Mahaffey]

I did include extra Chebyshev lemmas in there by mistake.

[Julian Berman]

Can you have another look at that #backticks link, the point is if you do it, then it makes it a lot easier for us to read what you wrote because it immediately becomes accessible in the Live Playground. Watch:

example : 37 = 37 := by
  rfl

Click the link that appears when you hover over the top right of the text box just above. We want to see that for your code :).

[Jason Mahaffey]

Having trouble getting the code to fit within the limit.

[Jason Mahaffey]

import Mathlib
variable {R : Type*} [CommRing R]
def waringCoeff' (n j : ℕ) : ℕ :=
  if j = 0 then 1
  else if n < 2 * j then 0
  else Nat.choose (n - j) j + Nat.choose (n - 1 - j) (j - 1)
-- end of waringCoeff' definition
def waringSum' (n : ℕ) (S P : R) : R :=
  if n = 0 then 2 else
  ∑ j ∈ Finset.range (n / 2 + 1),
    (-1 : R)^j * (waringCoeff' n j : R) * S^(n - 2 * j) * P^j
-- end
lemma waringCoeff'_succ_add (n j : ℕ) (hn : 1 ≤ n) (hj : 1 ≤ j) :
    waringCoeff' (n + 2) j = waringCoeff' (n + 1) j + waringCoeff' n (j - 1) := by
  by_cases hj1 : j = 1
  · subst hj1
    have hw0 : waringCoeff' n (1 - 1) = 1 := rfl
    rw [hw0]
    unfold waringCoeff'
    have h_ne : 1 ≠ 0 := by decide
    have h1 : ¬(n + 2 < 2 * 1) := by omega
    have h2 : ¬(n + 1 < 2 * 1) := by omega
    simp only [h_ne, h1, h2, ↓reduceIte]
    have h_sub : 1 - 1 = 0 := rfl
    rw [h_sub]
    simp only [Nat.choose_one_right, Nat.choose_zero_right]
    omega
  · obtain ⟨k, rfl⟩ : ∃ k, j = k + 2 := ⟨j - 2, by omega⟩
    have hk1 : k + 2 - 1 = k + 1 := by omega
    rw [hk1]
    unfold waringCoeff'
    have hj0 : k + 2 ≠ 0 := by omega
    have hj1_ne : k + 1 ≠ 0 := by omega
    simp only [hj0, hj1_ne, ↓reduceIte]
    have eq_cond : n + 2 < 2 * (k + 2) ↔ n < 2 * (k + 1) := by omega
    by_cases c1 : n + 2 < 2 * (k + 2)
    · have c2 : n + 1 < 2 * (k + 2) := by omega
      have c3 : n < 2 * (k + 1) := eq_cond.mp c1
      simp only [c1, c2, c3, ↓reduceIte]
    · have c1_not : ¬(n + 2 < 2 * (k + 2)) := c1
      have c3_not : ¬(n < 2 * (k + 1)) := eq_cond.not.mp c1_not
      by_cases c2 : n + 1 < 2 * (k + 2)
      · simp only [c1_not, c2, c3_not, ↓reduceIte, zero_add]
        have eq : n = 2 * k + 2 := by omega
        rw [eq]
        have e1 : 2 * k + 2 + 2 - (k + 2) = k + 2 := by omega
        have e2 : 2 * k + 2 + 2 - 1 - (k + 2) = k + 1 := by omega
        have e3 : 2 * k + 2 - (k + 1) = k + 1 := by omega
        have e4 : 2 * k + 2 - 1 - (k + 1) = k := by omega
        have e5 : k + 2 - 1 = k + 1 := by omega
        have e6 : k + 1 - 1 = k := by omega
        rw [e1, e2, e3, e4, e5, e6]
        simp only [Nat.choose_self]
      · have c2_not : ¬(n + 1 < 2 * (k + 2)) := c2
        simp only [c1_not, c2_not, c3_not, ↓reduceIte]
        rw [show n + 2 - (k + 2) = n - k by omega]
        rw [show n + 2 - 1 - (k + 2) = n - k - 1 by omega]
        rw [show n + 1 - (k + 2) = n - k - 1 by omega]
        rw [show n + 1 - 1 - (k + 2) = n - k - 2 by omega]
        rw [show n - (k + 1) = n - k - 1 by omega]
        rw [show n - 1 - (k + 1) = n - k - 2 by omega]
        have e_right1 : k + 2 - 1 = k + 1 := by omega
        have e_right2 : k + 1 - 1 = k := by omega
        rw [e_right1, e_right2]
        have H1 : Nat.choose (n - k) (k + 2) = Nat.choose (n - k - 1)
         (k + 1) + Nat.choose (n - k - 1) (k + 2) := by
          have h := Nat.choose_succ_succ (n - k - 1) (k + 1)
          have e1 : (n - k - 1).succ = n - k := by omega
          have e2 : (k + 1).succ = k + 2 := by omega
          rw [e1, e2] at h
          exact h
        have H2 : Nat.choose (n - k - 1) (k + 1) = Nat.choose (n - k - 2)
         k + Nat.choose (n - k - 2) (k + 1) := by
          have h := Nat.choose_succ_succ (n - k - 2) k
          have e1 : (n - k - 2).succ = n - k - 1 := by omega
          have e2 : k.succ = k + 1 := by omega
          rw [e1, e2] at h
          exact h
        rw [H1, H2]
        omega
--end
lemma waringSum'_eq_sum_range (n : ℕ) (S P : R) :
    waringSum' n S P = if n = 0 then 2 else ∑ j ∈ Finset.range (n + 2), (-1 : R)^j *
    (waringCoeff' n j : R) * S^(n - 2 * j) * P^j := by
  unfold waringSum'
  split_ifs with h
  · rfl
  · apply Finset.sum_subset
    · intro j hj; rw [Finset.mem_range] at hj ⊢; omega
    · intro j hj hj'
      rw [Finset.mem_range] at hj hj'
      have hj0 : j ≠ 0 := by omega
      have hn2j : n < 2 * j := by omega
      simp [waringCoeff', hj0, hn2j]
-- end
lemma waringSum'_rec_eq (n : ℕ) (hn : 1 ≤ n) (S P : R) :
    waringSum' (n + 2) S P = S * waringSum' (n + 1) S P - P * waringSum' n S P := by
  have hn0 : (n = 0) ↔ False := iff_false_intro (by omega)
  have hn1 : (n + 1 = 0) ↔ False := iff_false_intro (by omega)
  have hn2 : (n + 2 = 0) ↔ False := iff_false_intro (by omega)
  rw [waringSum'_eq_sum_range (n + 2), waringSum'_eq_sum_range (n + 1), waringSum'_eq_sum_range n]
  simp only [hn0, hn1, hn2, ite_false]
  rw [Finset.mul_sum, Finset.mul_sum]
  have sum_P_shift : ∑ j ∈ Finset.range (n + 3), (if j = 0 then (0 : R) else -
   ((-1 : R) ^ j * (waringCoeff' n (j - 1) : R) * S ^ (n + 2 - 2 * j) * P ^ j)) =
      ∑ j ∈ Finset.range (n + 2), P * ((-1 : R) ^ j * (waringCoeff' n j : R) *
       S ^ (n - 2 * j) * P ^ j) := by
    have h_split := Finset.sum_range_succ' (fun j => if j = 0 then (0 : R)
     else - ((-1 : R) ^ j * (waringCoeff' n (j - 1) : R) * S ^ (n + 2 - 2 * j) * P ^ j)) (n + 2)
    rw [h_split]
    have eq0 : (0 = 0) ↔ True := iff_true_intro rfl
    simp only [ite_true, add_zero]
    apply Finset.sum_congr rfl
    intro j _
    have hj0 : j + 1 ≠ 0 := by omega
    have hj0_iff : (j + 1 = 0) ↔ False := iff_false_intro hj0
    simp only [hj0_iff, ite_false, Nat.add_sub_cancel_right]
    have hS : n + 2 - 2 * (j + 1) = n - 2 * j := by omega
    rw [hS]
    ring
  have lhs_eq : ∑ j ∈ Finset.range (n + 4), (-1 : R) ^ j *
   (waringCoeff' (n + 2) j : R) * S ^ (n + 2 - 2 * j) * P ^ j =
      ∑ j ∈ Finset.range (n + 3), (-1 : R) ^ j * (waringCoeff' (n + 2) j : R)
       * S ^ (n + 2 - 2 * j) * P ^ j := by
    have h_split := Finset.sum_range_succ (fun j => (-1 : R) ^ j * (waringCoeff' (n + 2) j : R)
     * S ^ (n + 2 - 2 * j) * P ^ j) (n + 3)
    rw [h_split]
    have hz : waringCoeff' (n + 2) (n + 3) = 0 := by
      unfold waringCoeff'
      have h1 : (n + 3 = 0) ↔ False := iff_false_intro (by omega)
      have h2 : (n + 2 < 2 * (n + 3)) ↔ True := iff_true_intro (by omega)
      simp only [h1, h2, ite_false, ite_true]
    rw [hz]
    simp only [Nat.cast_zero, mul_zero, zero_mul, add_zero]
  rw [← sum_P_shift, lhs_eq, ← Finset.sum_sub_distrib]
  apply Finset.sum_congr rfl
  intro j _
  rcases j with _ | j
  · have eq0 : (0 = 0) ↔ True := iff_true_intro rfl
    simp only [ ite_true, sub_zero, pow_zero, mul_one]
    have c1 : waringCoeff' (n + 2) 0 = 1 := rfl
    have c2 : waringCoeff' (n + 1) 0 = 1 := rfl
    simp only [c1, c2, Nat.cast_one, one_mul]
    have e1 : n + 2 - 2 * 0 = n + 2 := rfl
    have e2 : n + 1 - 2 * 0 = n + 1 := rfl
    rw [e1, e2]
    ring
  · have hsucc : (j + 1 = 0) ↔ False := iff_false_intro (by omega)
    simp only [hsucc, ite_false, sub_neg_eq_add]
    rw [waringCoeff'_succ_add n (j + 1) hn (by omega)]
    push_cast
    by_cases h_bounds : n + 1 < 2 * (j + 1)
    · have z1 : waringCoeff' (n + 1) (j + 1) = 0 := by
        unfold waringCoeff'
        have h_bounds_true : (n + 1 < 2 * (j + 1)) ↔ True := iff_true_intro h_bounds
        simp only [hsucc, h_bounds_true, ite_false, ite_true]
      rw [z1]
      ring
    · have h_pow : n + 2 - 2 * (j + 1) = n + 1 - 2 * (j + 1) + 1 := by omega
      have hS : S ^ (n + 2 - 2 * (j + 1)) = S ^ (n + 1 - 2 * (j + 1))
       * S := by rw [h_pow, pow_add, pow_one]
      rw [hS]
      ring
-- end
theorem waring_formula_div_free (A B : R) (n : ℕ) :
    A^n + B^n = waringSum' n (A + B) (A * B) := by
  induction n using Nat.strongRecOn with
  | ind n ih =>
    rcases n with _ | _ | _ | n
    · simp [waringSum']; norm_num        -- ← add norm_num here
    · simp [waringSum', waringCoeff']
    · rw [waringSum']
      simp [waringCoeff', Finset.sum_range_succ]
      ring
    · have hrec : A ^ (n + 3) + B ^ (n + 3) =
          (A + B) * (A ^ (n + 2) + B ^ (n + 2)) - A * B * (A ^ (n + 1) + B ^ (n + 1)) := by ring
      rw [hrec, ih (n + 2) (by omega), ih (n + 1) (by omega)]
      exact (waringSum'_rec_eq (n + 1) (by omega) (A + B) (A * B)).symm
-- end
lemma waringCoeff_single_eq (n j : ℕ) (hn : n ≠ 0) (hj : j ≤ n / 2) :
    (if j = 0 then 1 else Nat.choose (n - j) j + Nat.choose (n - 1 - j) (j - 1)) =
    n * Nat.choose (n - j) j / (n - j) := by
  split_ifs with h
  · simp only [h, Nat.sub_zero, Nat.choose_zero_right, mul_one]
    exact (Nat.div_self (by omega)).symm
  · have h_nj_pos : 0 < n - j := by omega
    symm
    apply Nat.div_eq_of_eq_mul_right h_nj_pos
    have h1 : n - 1 - j + 1 = n - j := by omega
    have h2 : j - 1 + 1 = j := by omega
    have H := Nat.add_one_mul_choose_eq (n - 1 - j) (j - 1)
    rw [h1, h2] at H
    have hn_eq : n = n - j + j := (Nat.sub_add_cancel (by omega)).symm
    have expand_lhs : n * Nat.choose (n - j) j =
        (n - j) * Nat.choose (n - j) j + j * Nat.choose (n - j) j := by
      conv_lhs => rw [hn_eq]
      simp only [Nat.add_sub_cancel]
      ring
    have expand_rhs : (Nat.choose (n - j) j + Nat.choose (n - 1 - j) (j - 1)) * (n - j) =
        (n - j) * Nat.choose (n - j) j + (n - j) * Nat.choose (n - 1 - j) (j - 1) := by
      ring
    linarith [H]
-- end
theorem waring_formula_div_free_sum_single (A B : R) {n : ℕ} (hn : n ≠ 0) :
    A^n + B^n = ∑ j ∈ Finset.range (n / 2 + 1),
      (-1 : R)^j * (((n * Nat.choose (n - j) j / (n - j)) : ℕ) : R)
       * (A + B)^(n - 2 * j) * (A * B)^j := by
  rw [waring_formula_div_free A B n, waringSum', if_neg hn]
  apply Finset.sum_congr rfl
  intro j hj
  rw [waringCoeff']
  have hj_bound : j ≤ n / 2 := by
    rw [Finset.mem_range] at hj; omega
  have h_not_lt : ¬(n < 2 * j) := by omega
  have h_simplify : (if j = 0 then 1 else if n < 2 * j then 0 else
   Nat.choose (n - j) j + Nat.choose (n - 1 - j) (j - 1)) =
                    (if j = 0 then 1 else Nat.choose (n - j) j
                     + Nat.choose (n - 1 - j) (j - 1)) := by
    split_ifs with hj0
    · rfl
    · simp
  rw [h_simplify, waringCoeff_single_eq n j hn hj_bound]
-- end

[Weiyi Wang]

I am not a mathlib maintainer, but given that there is a Mathworld entry for it, and the proof doesn't seem terribly long or niche, I think the theorem is something mathlib can have. As for the proof, if it was generated by AI, it usually needs to be massively polished before it meets mathlib code standard

[Weiyi Wang]

I also noticed there is a n-variable generalization https://planetmath.org/waringsformula. Mathlib usually wants the most general form (as long as it is reasonable)

[Filippo A. E. Nuccio]

Unfortunately I'm inclined to say that code in that style is really far from Mathlib. @Jason Mahaffey we've witnessed a lot of cases of this kind of efforts recently and almost none of them made it to the library. But don't get me wrong: I don't want to discourage you nor to question your good faith. Consider simply that getting something in Mathlib requires a lot of efforts from authors and if you've got limited Lean experience this will mean spending a significant amount of time learning the basics. If you're ready to embark in the adventure, great! Let's try to open a PR, first and foremost trying to reduce your imports (no file in Mathlib can import the whole of it!). Before doing so, though, I would suggest that you pick a theorem whose proof (on paper) you know and is in Mathlib : try to read Mathlib 's proof. Once you'll understand all details you might be ready to write your first one.