extrema, R^n

Stream: new members

[Nathan]

image.png

How is this code looking so far? I wasn't sure of the best way to deal with extrema or R^n. For R^n I used Fin n → NNReal. I'm also not sure about using the variable.

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

variable (n : ℕ) [NeZero n]
noncomputable def f (x : Fin n → NNReal) (i : Fin n) := x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (x : Fin n → NNReal) := (Finset.image (f n x) Finset.univ).max
noncomputable def m : NNReal := 1 / (2*n/3 : ℕ)

theorem POTD_2490 (hn : n ≥ 3) : Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (m n) := sorry

[Kevin Buzzard]

What does $x_i+\sqrt{x_{i+1}x_{i+2}}$ even mean if $i=n-1$ or $i=n$?

[Nathan]

sorry, i forgot to mention the indices wrap around, so $x_{n+1} = x_1$

[Bbbbbbbbba]

Maybe you want n to be implicit? Feels like keeping writing it out could be annoying

[Bbbbbbbbba]

I think the API you have chosen are certainly usable, though maybe not the most convenient. As a proof of concept I proved this, though I spent quite some time dealing with coercion to WithBot NNReal.

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

variable (n : ℕ) [NeZero n]
noncomputable def f (x : Fin n → NNReal) (i : Fin n) := x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (x : Fin n → NNReal) := (Finset.image (f n x) Finset.univ).max
noncomputable def m : NNReal := 1 / (2*n/3 : ℕ)

open Finset

example (x : Fin n → NNReal) : ∑ i, (f n x i) ≤ maxf n x * n := by
  let max'f := (Finset.image (f n x) Finset.univ).max' (Finset.image_nonempty.mpr univ_nonempty)
  have hmax : ∀ i ∈ Finset.univ, f n x i ≤ max'f :=
    fun i hi ↦ le_max' _ _ (mem_image.mpr ⟨i, hi, rfl⟩)
  have hcoe : max'f = maxf n x := coe_max' _
  rw [← hcoe]
  apply WithBot.coe_le_coe.mpr
  convert sum_le_sum hmax
  rw [mul_comm, Eq.comm]
  convert Finset.sum_const _ using 1
  rw [card_fin n]
  exact Eq.symm (nsmul_eq_mul n max'f)

[Bbbbbbbbba]

Nathan said:

image.png

How is this code looking so far? I wasn't sure of the best way to deal with extrema or R^n. For R^n I used Fin n → NNReal. I'm also not sure about using the variable.

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

variable (n : ℕ) [NeZero n]
noncomputable def f (x : Fin n → NNReal) (i : Fin n) := x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (x : Fin n → NNReal) := (Finset.image (f n x) Finset.univ).max
noncomputable def m : NNReal := 1 / (2*n/3 : ℕ)

theorem POTD_2490 (hn : n ≥ 3) : Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (m n) := sorry

Wait, is this value of m correct for e.g. n = 4?

[Nathan]

for n=4 it should be 1/2

[Bbbbbbbbba]

Oh just noticed that the denominator is ℕ :joy:

[Nathan]

yeah it's simulating a "floor" function.

since you mentioned WithBot, i think i could have maxf return NNReal by using max' rather than max

[Bbbbbbbbba]

Yeah that would be nicer API.

Did the "trivial" part (achievability of the minimum) for the special case n % 3 = 0, and still have a bunch sorries to fill :upside_down: Wondering if this is the right way.

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

variable (n : ℕ) [NeZero n]
noncomputable def f (x : Fin n → NNReal) (i : Fin n) := x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (x : Fin n → NNReal) := (Finset.image (f n x) Finset.univ).max
noncomputable def m : NNReal := 1 / (2*n/3 : ℕ)

open Finset

noncomputable def max'f (x : Fin n → NNReal) := (image (f n x) univ).max' (image_nonempty.mpr univ_nonempty)

theorem POTD'_2490 (hn : n ≥ 3) (hn3 : n % 3 = 0) : Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (m n) := by
  constructor
  · let x : Fin n → NNReal := fun i ↦ if i % 3 = 0 then 0 else 1 / (2 * n / 3 : ℕ)
    use x
    constructor
    · change FinVec.sum x = 1
      simp only [x, FinVec.sum_eq]
      have h1 : ∑ i with i % 3 = 0, x i = 0 := by
        convert ← Finset.sum_eq_card_nsmul _
        · exact nsmul_zero #{i | i % 3 = 0}
        · intro a ha; simp at ha; simp [x, ha]
      have h2 : ∑ i with i % 3 ≠ 0, x i = #{(i : Fin n) | i % 3 ≠ 0} • (1 / (2 * n / 3 : ℕ)) := by
        apply Finset.sum_eq_card_nsmul
        intro a ha; simp at ha; simp [x, ha]
      have h3 : #{(i : Fin n) | i % 3 ≠ 0} = 2 * n / 3 := by
        sorry
      rw [← sum_filter_add_sum_filter_not _ fun i ↦ i % 3 = 0, h1, h2, h3]
      simp only [nsmul_eq_mul, zero_add]
      refine mul_one_div_cancel (Nat.cast_ne_zero.mpr ?_)
      omega
    · have hcoe : max'f n x = maxf n x := coe_max' _
      rw [← hcoe]
      apply WithBot.coe_eq_coe.mpr
      have h : max'f n x ∈ _ := max'_mem _ _
      have ⟨i, _, hi⟩ := mem_image.mp h
      rw [← hi]
      by_cases hi : i % 3 = 0
      · have hi1 : (i + 1) % 3 ≠ 0 := by sorry
        have hi2 : (i + 2) % 3 ≠ 0 := by sorry
        simp only [f, x, m, hi, hi1, hi2, reduceIte, NNReal.sqrt_mul_self, zero_add]
      · by_cases hi1 : (i + 1) % 3 = 0
        · have hi2 : (i + 2) % 3 ≠ 0 := by sorry
          simp only [f, x, m, hi, hi1, hi2, reduceIte, zero_mul, NNReal.sqrt_zero, add_zero]
        · have hi2 : (i + 2) % 3 = 0 := by sorry
          simp only [f, x, m, hi, hi1, hi2, reduceIte, mul_zero, NNReal.sqrt_zero, add_zero]
  · sorry

[Nathan]

oh wow! it must have been tricky dealing with the mods and indices and stuff. i've been working on a different problem but i'll tackle this one next. i have an outline for a proof already.

[Nathan]

i'm gonna save your code for reference later

[Nathan]

is use x the same as exists x?

[Aaron Liu]

use does the same thing as exists mostly

[Aaron Liu]

it's a bit more complicated and also runs a discharger afterwards

[Aaron Liu]

but they do basically the same thing

[Nathan]

How can I prove have : ∃ j, g j = maxg := sorry in the code below?

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

variable (n : ℕ) [NeZero n]
noncomputable def f (x : Fin n → NNReal) (i : Fin n) := x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (x : Fin n → NNReal) := (Finset.image (f n x) Finset.univ).max
noncomputable def m : NNReal := 1 / (2*n/3 : ℕ)

open Finset
theorem POTD_2490 (hn : n ≥ 3) : Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (m n) := by
  and_intros
  · let w (i : Fin n) := if i % 3 = 0 then 0 else (m n)
    exists w; and_intros
    · change FinVec.sum w = 1
      simp only [w, FinVec.sum_eq]
      have h1 : ∑ i with i % 3 = 0, w i = 0 := by
        convert ← Finset.sum_eq_card_nsmul _
        · exact nsmul_zero #{i | i % 3 = 0}
        · intro a ha; simp at ha; simp [w, ha]
      have h2 : ∑ i with i % 3 ≠ 0, w i = #{(i : Fin n) | i % 3 ≠ 0} • (1 / (2 * n / 3 : ℕ)) := by
        apply Finset.sum_eq_card_nsmul
        intro a ha; simp at ha; simp [w, ha]
        unfold m; simp
      have h3 : #{(i : Fin n) | i % 3 ≠ 0} = 2 * n / 3 := by
        sorry
      rw [← sum_filter_add_sum_filter_not _ fun i ↦ i % 3 = 0, h1, h2, h3]
      simp only [nsmul_eq_mul, zero_add]
      refine mul_one_div_cancel (Nat.cast_ne_zero.mpr ?_)
      omega
    · refine le_antisymm ?_ ?_
      · sorry
      · sorry
  · --let g (x : Fin n → NNReal) (i : Fin n) := x i + min (x (i+1)) (x (i+2))
    intro fx ⟨x, xha, xhb⟩ _
    let g (i : Fin n) := x i + min (x (i+1)) (x (i+2))
    let maxg := (Finset.image g Finset.univ).max
    have : ∃ j, g j = maxg := sorry
    let ⟨j, jh⟩ := this
    suffices m n ≤ maxg from by
      refine le_trans this ?_
      rw[←xhb]; unfold maxf
      have : f n x j ≤ (Finset.image (f n x) Finset.univ).max := le_max (by simp)
      refine le_trans ?_ this
      rw[←jh]; unfold g f;
      refine WithBot.coe_le_coe.mpr ?_; simp
      by_cases gt : x (j+1) ≤ x (j+2)
      · left;
        have := mul_le_mul_left' gt (x (j + 1))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
      · right; simp at gt; replace gt := Std.le_of_lt gt
        have := mul_le_mul_right' gt (x (j + 2))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
    sorry

[Aaron Liu]

cutout

    have : ∃ j, g j = maxg := by
      have hs : (Finset.image g univ).Nonempty := by simp
      obtain ⟨x, hx⟩ := Finset.max_of_nonempty hs
      have hxs := Finset.mem_of_max hx
      obtain ⟨j, -, rfl⟩ := mem_image.1 hxs
      exact ⟨j, hx.symm⟩

[Nathan]

thanks!

[Nathan]

- is just throwing away the unneeded hypothesis, right?

[Aaron Liu]

yeah

[Bbbbbbbbba]

Hmm, this - syntax is only valid for obtain, not have. What other reasons are there to use obtain instead of have?

[Nathan]

oh i've been using let for this

[Nathan]

how do i deal with the errors on line 69?

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

noncomputable def f {n : ℕ} [NeZero n] (x : Fin n → NNReal) (i : Fin n) :=
  x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (n : ℕ) [NeZero n] (x : Fin n → NNReal) :=
  (Finset.image (f x) Finset.univ).max' (by simp)

open Finset

theorem POTD_2490 {n : ℕ} [NeZero n] (hn : n ≥ 3) :
    Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (1 / (2*n/3 : ℕ)) := by
  let m : NNReal := 1 / (2*n/3 : ℕ)
  and_intros
  · let w (i : Fin n) := if i % 3 = 0 then 0 else m
    exists w; and_intros
    · change FinVec.sum w = 1
      simp only [w, FinVec.sum_eq]
      have h1 : ∑ i with i % 3 = 0, w i = 0 := by
        convert ← Finset.sum_eq_card_nsmul _
        · exact nsmul_zero #{i | i % 3 = 0}
        · intro a ha; simp at ha; simp [w, ha]
      have h2 : ∑ i with i % 3 ≠ 0, w i = #{(i : Fin n) | i % 3 ≠ 0} • m := by
        apply Finset.sum_eq_card_nsmul
        intro a ha; simp at ha; simp [w, ha]
      have h3 : #{(i : Fin n) | i % 3 ≠ 0} = 2 * n / 3 := by
        sorry
      rw [← sum_filter_add_sum_filter_not _ fun i ↦ i % 3 = 0, h1, h2, h3]
      simp only [nsmul_eq_mul, zero_add]
      refine mul_one_div_cancel (Nat.cast_ne_zero.mpr ?_)
      omega
    · refine le_antisymm ?_ ?_
      · sorry
      · sorry
  · intro fx ⟨x, xha, xhb⟩ xhc; clear xhc; change FinVec.sum x = 1 at xha
    let g (i : Fin n) := x i + min (x (i+1)) (x (i+2))
    let gmax := (Finset.image g univ).max' (by simp)
    suffices m ≤ gmax from by
      refine le_trans this ?_
      replace := Finset.max'_mem (Finset.image g univ) (by simp)
      obtain ⟨j, -, jhb⟩ := mem_image.mp this; clear this
      unfold gmax; rw[←jhb, ←xhb]; clear jhb xhb
      have := le_max' (Finset.image (f x) Finset.univ) (f x j) (by simp)
      refine le_trans ?_ this; unfold g f; simp
      by_cases gt : x (j+1) ≤ x (j+2)
      · left;
        have := mul_le_mul_left' gt (x (j + 1))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
      · right; simp at gt; replace gt := Std.le_of_lt gt
        have := mul_le_mul_right' gt (x (j + 2))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
    clear xhb fx
    obtain ⟨i₀, ih⟩ : ∃ i, ∀ j, x (i-1) ≤ x j := by
      have := Finset.min'_mem (Finset.image x univ) (by simp)
      obtain ⟨i, -, ih⟩ := mem_image.mp this; exists i+1; simp
      have := (Finset.min'_eq_iff (Finset.image x univ) (by simp) (x i)).mp (Eq.symm ih)
      intro j; refine this.right (x j) ?_
      exact mem_image_of_mem x (by simp)
    let h (i : Fin n) := if x (i+1) ≥ x (i+2) then i+1 else i+2
    have := calc (2*n/3 : ℕ) * gmax
      _ = ((n+1)/3 : ℕ) * gmax + (n/3 : ℕ) * gmax := by
        have : 2*n/3 = (n+1)/3 + n/3 := by grind
        simp[this, right_distrib]
      _ = (∑ k : Fin ((n+1)/3), gmax) + (∑ k : Fin (n/3), gmax) := by simp
      _ ≥ (∑ k : Fin ((n+1)/3), g (i₀+3*k)) + (∑ k : Fin (n/3), g (h (i₀+3*k))) := sorry
      _ = 1 := sorry
    exact NNReal.div_le_of_le_mul' this

[Nathan]

Seems like i need to cast one kind of Fin into another, but I couldn't get it to work.
(∑ k : Fin ((n+1)/3), g (i₀+3*k)) + (∑ k : Fin (n/3), g (h (i₀+3*k)))

[Nathan]

i just edited line 69, there was a mistake

[Nathan]

sorry i had to edit it again

[Nathan]

but yeah, I'm still having issues casting the Fins

[Ruben Van de Velde]

In what direction? There's a number of definitions starting with Fin.cast, but nothing implicit (by design)

[Nathan]

k needs to become a Fin n before being multiplied by 3 and added to i₀

[Nathan]

oh, i was able to do it with Fin.castLE, thanks

[metakuntyyy]

Bbbbbbbbba said:

Hmm, this - syntax is only valid for obtain, not have. What other reasons are there to use obtain instead of have?

Obtain is just have with rcases afterwards. It's also useful to clear variables. If I have a combined statement like an existential or a nested conjunction I use obtain to clear out the existential statement afterwards.

[Nathan]

How can I prove this lemma? I'm stuck.

import Mathlib.Data.Nat.Init

lemma l1 {n : ℕ} [NeZero n] (h : n % 3 = 1) : 3 * Fin.ofNat n (n / 3 - 1) = -4 := sorry

Here's the context
POTD2490.lean

[Nathan]

i can give context in the form of latex if needed, but if the lemma can be solved as-is, then it's probably unnecessary

[metakuntyyy]

Can you paste the file here please? You can quote with ```

[Nathan]

yeah sure

[Nathan]

import Mathlib.Data.Int.Init
import Mathlib.Data.NNReal.Defs
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Algebra.BigOperators.Fin

noncomputable def f {n : ℕ} [NeZero n] (x : Fin n → NNReal) (i : Fin n) :=
  x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (n : ℕ) [NeZero n] (x : Fin n → NNReal) :=
  (Finset.image (f x) Finset.univ).max' (by simp)

open Finset

lemma l1 {n : ℕ} [NeZero n] (h : n % 3 = 1) : 3 * Fin.ofNat n (n / 3 - 1) = -4 := sorry

theorem POTD_2490 {n : ℕ} [NeZero n] (hn : n ≥ 3) :
    Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (1 / (2*n/3 : ℕ)) := by
  let m : NNReal := 1 / (2*n/3 : ℕ)
  and_intros
  · let w (i : Fin n) := if i % 3 = 0 then 0 else m
    exists w; and_intros
    · change FinVec.sum w = 1
      simp only [w, FinVec.sum_eq]
      have h1 : ∑ i with i % 3 = 0, w i = 0 := by
        convert ← Finset.sum_eq_card_nsmul _
        · exact nsmul_zero #{i | i % 3 = 0}
        · intro a ha; simp at ha; simp [w, ha]
      have h2 : ∑ i with i % 3 ≠ 0, w i = #{(i : Fin n) | i % 3 ≠ 0} • m := by
        apply Finset.sum_eq_card_nsmul
        intro a ha; simp at ha; simp [w, ha]
      have h3 : #{(i : Fin n) | i % 3 ≠ 0} = 2 * n / 3 := by
        sorry
      rw [← sum_filter_add_sum_filter_not _ fun i ↦ i % 3 = 0, h1, h2, h3]
      simp only [nsmul_eq_mul, zero_add]
      refine mul_one_div_cancel (Nat.cast_ne_zero.mpr ?_)
      omega
    · refine le_antisymm ?_ ?_
      · sorry
      · sorry
  · intro fx ⟨x, xha, xhb⟩ xhc; clear xhc; change FinVec.sum x = 1 at xha
    let g (i : Fin n) := x i + min (x (i+1)) (x (i+2))
    let gmax := (Finset.image g univ).max' (by simp)
    suffices m ≤ gmax from by
      refine le_trans this ?_
      replace := Finset.max'_mem (Finset.image g univ) (by simp)
      obtain ⟨j, -, jhb⟩ := mem_image.mp this; clear this
      unfold gmax; rw[←jhb, ←xhb]; clear jhb xhb
      have := le_max' (Finset.image (f x) Finset.univ) (f x j) (by simp)
      refine le_trans ?_ this; unfold g f
      simp only [add_le_add_iff_left, inf_le_iff]
      by_cases gt : x (j+1) ≤ x (j+2)
      · left;
        have := mul_le_mul_right gt (x (j + 1))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
      · right; simp only [not_le] at gt; replace gt := Std.le_of_lt gt
        have := mul_le_mul_left gt (x (j + 2))
        replace := NNReal.sqrt_le_sqrt.mpr this
        simp at this; assumption
    clear xhb fx
    obtain ⟨i₀, ih⟩ : ∃ i, ∀ j, x (i-1) ≤ x j := by
      have := Finset.min'_mem (Finset.image x univ) (by simp)
      obtain ⟨i, -, ih⟩ := mem_image.mp this; exists i+1; simp only [add_sub_cancel_right]
      have := (Finset.min'_eq_iff (Finset.image x univ) (by simp) (x i)).mp (Eq.symm ih)
      intro j; refine this.right (x j) ?_
      exact mem_image_of_mem x (by simp)
    let h (i : Fin n) := if x (i+1) ≥ x (i+2) then i+1 else i+2


    let res := if n%3 = 1 then x (i₀-1) else (if n%3 = 2 then x (i₀-1) + x (i₀-2) else 0)
    let c₁ (k : Fin n) := k < (n+1)/3
    let c₂ (k : Fin n) := k < n/3
    have := calc (2*n/3 : ℕ) * gmax
      _ = ((n+1)/3 : ℕ) * gmax + (n/3 : ℕ) * gmax := by
        have : 2*n/3 = (n+1)/3 + n/3 := by grind
        simp[this, right_distrib]
      _ = (∑ k with c₁ k, gmax) + (∑ k with c₂ k, gmax) := by
        have (a : ℕ) (h : a ≤ n) : a * gmax = ∑ (k : Fin n) with k.val < a, gmax := by
          nth_rewrite 2 [show gmax = gmax*1 by simp]; rw[←mul_sum, mul_comm]
          refine congrArg (HMul.hMul gmax) ?_
          simp only [sum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]; symm
          refine card_eq_of_bijective (fun i ↦ (fun (h : i < a) ↦ ⟨i, by grind⟩)) ?_ ?_ ?_
          · intro a ah; simp only [mem_filter, mem_univ, true_and] at ah; exists a.val, ah
          · intros; grind
          · intros; grind
        rw[this ((n+1)/3), this (n/3)]
        <;> grind
      _ ≥ (∑ k with c₁ k, g (i₀+3*k)) + (∑ k with c₂ k, g (h (i₀+3*k))) := by
        refine add_le_add ?_ ?_ <;>
        · refine sum_le_sum ?_; intros
          have := (Finset.max'_eq_iff _ (by simp) gmax).mp rfl
          exact this.right _ (by simp)
      _ ≥ (∑ k with c₂ k, g (i₀+3*k)) +
          (∑ k with c₂ k, max (x (i₀+3*k+1)) (x (i₀+3*k+2))) + res := by
        have le1 (hmod : n%3 ≠ 2) : ∑ k with c₂ k, g (i₀+3*k) ≤ ∑ k with c₁ k, g (i₀+3*k) := by
          refine le_of_eq ?_
          refine sum_bijective id (by simp) ?_ ?_ <;> grind
        have le2 {S : Finset (Fin n)} : ∑ k ∈ S, max (x (i₀+3*k+1)) (x (i₀+3*k+2)) ≤
            (∑ k ∈ S, g (h (i₀+3*k))) := by
          refine sum_le_sum ?_; intros
          convert le_self_add
          · grind
          exact NNReal.instCanonicallyOrderedAdd

        have mod_disj : n%3 = 0 ∨ n%3 = 1 ∨ n%3 = 2 := by
          have : n%3 < 3 := Nat.mod_lt n (by simp); grind
        rcases mod_disj with d | d | d <;> unfold res
        · simp only [d, zero_ne_one, ↓reduceIte, OfNat.zero_ne_ofNat, add_zero, ge_iff_le]
          exact add_le_add (le1 (by grind)) le2
        · simp only [d, ↓reduceIte, ge_iff_le]
          rw[add_assoc]
          refine add_le_add (le1 (by grind)) ?_
          rw[add_comm]
          have : NeZero (n/3) := by
            refine neZero_iff.mpr ?_
            exact Nat.div_ne_zero_iff.mpr ⟨by simp, hn⟩
          let klast := Fin.ofNat n (n/3-1)
          rw[←sum_filter_add_sum_filter_not _ (fun k ↦ k = klast)]
          nth_rewrite 3 [←sum_filter_add_sum_filter_not _ (fun k ↦ k = klast)]
          rw[←add_assoc]; refine add_le_add ?_ le2
          refine le_of_eq ?_

          have (f : Fin n → NNReal): ∑ k ∈ {k1 | c₂ k1} with k = klast, f k = f klast := by
            rw[←sum_singleton f klast]
            refine sum_bijective id (by simp) ?_ (by simp)
            simp only [mem_filter, mem_univ, true_and, id_eq, mem_singleton,
              and_iff_right_iff_imp, forall_eq]
            unfold c₂
            rw[Fin.val_ofNat n (n/3-1)]
            have lt : n/3-1 < n/3 := by
              refine Nat.sub_one_lt_of_lt (m := 0) ?_
              exact Nat.pos_of_neZero (n / 3)
            have : (n/3-1) % n = n/3-1 := by
              refine Nat.mod_eq_of_lt ?_
              exact Nat.lt_of_lt_of_le lt (Nat.div_le_self n 3)
            rw[this]; exact lt
          simp only [this]

          unfold h
          by_cases cas : x (i₀+3*klast+1) ≥ x (i₀+3*klast+2)
          · simp only [cas, sup_of_le_left, ↓reduceIte]
            unfold g; rw[add_comm]; simp only [add_right_inj]
            suffices suff : i₀+3*klast+1+2 = i₀-1 from by
              rw[suff]; simp only [ih, inf_of_le_right]
            rw[l1 d]; grind
          · simp only [show x (i₀ + 3 * klast + 2) ≥ x (i₀ + 3 * klast + 1) by grind,
              sup_of_le_right, ge_iff_le, cas, ↓reduceIte]
            unfold g; rw[add_comm]
            suffices suff : i₀+3*klast+2+1 = i₀-1 from by
              rw[suff]; simp only [ih, inf_of_le_left]
            rw[l1 d]; grind
        · simp only [d, OfNat.ofNat_ne_one, ↓reduceIte, ge_iff_le]
          rw[add_assoc]; nth_rewrite 1 [add_comm]; rw[add_assoc]; nth_rewrite 4 [add_comm]
          refine add_le_add le2 ?_
          refine le_of_eq ?_
          let klast := Fin.ofNat n (n/3)
          nth_rewrite 2 [←sum_filter_add_sum_filter_not _ (fun k ↦ k = klast)]
          refine (show ∀ {a b c d : NNReal}, a = b → c = d → a+c = b+d by grind) ?_ ?_
          · sorry
          · sorry
      _ = (∑ k with c₂ k, (g (i₀+3*k) + max (x (i₀+3*k+1)) (x (i₀+3*k+2)))) + res := sorry
      _ = (∑ k with c₂ k, (x (i₀+3*k) + x (i₀+3*k+1) + x (i₀+3*k+2))) + res := sorry
      _ = ∑ k : Fin n, x k := sorry
      _ = 1 := by rw[←xha]; simp only [FinVec.sum_eq];
    exact NNReal.div_le_of_le_mul' this

[metakuntyyy]

Does this help you? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/ZMod/Defs.html#Fin.instCommRing

[metakuntyyy]

You have to open the CommRing instance explicitly.

[Nathan]

it might help, but i'm not sure how to use it

[metakuntyyy]

letI := Fin.instCommRing n

[Ruben Van de Velde]

Maybe you want to use ZMod instead

[Nathan]

would i have to change the theorem statement? because the theorem uses maxf which uses Fin n

[Nathan]

If I try to use ZMod n instead of Fin n then I run into some trouble here: let w (i : Fin n) := if i % 3 = 0 then 0 else m

[Nathan]

ok i went through and changed everything to ZMod n but it just has the effect of changing the necessary lemma to this:

import Mathlib.Data.ZMod.Basic

lemma l1 {n : ℕ} [NeZero n] (h : n % 3 = 1) : 3 * ((n/3-1 : ℕ) : ZMod n) = -4 := sorry

[Kevin Buzzard]

h implies $n=3t+1$ and you seem to want to prove that $3t$ is $-4$ modulo $3t+1$ which is false in general unless I made a slip.

Edit: indeed I made a slip, it's $3(t-1)$ so this is fine as long as $t\geq1$.

[Nathan]

sorry i think it does fail for n=1, i didn't realize

[Nathan]

i was able to prove it with the additional hypothesis n ≥ 3. so i think the ZMod approach is viable :pray:

import Mathlib.Data.ZMod.Basic

lemma l1 {n : ℕ} [NeZero n] (h1 : n % 3 = 1) (h2 : n ≥ 3) : 3 * ((n/3-1 : ℕ) : ZMod n) = -4 := by
  have : ((3 : ℕ) : ZMod n) = (3 : ZMod n) := by exact Nat.cast_three
  nth_rewrite 1 [←this]
  rw[←Nat.cast_mul 3 (n/3-1)]
  have : 3 * (n/3-1) = n-4 := by grind
  rw[this]
  have : ((n-4 : ℕ) : ZMod n) = (n : ZMod n) - (4 : ZMod n) := by
    refine Nat.cast_sub ?_
    grind
  simp[this]

[Nathan]

maybe this proof can be modified for Fin n

[Nathan]

wait it doesn't fail for n=1 :joy: because anything is equal mod 1

[Nathan]

this can't be the best way to prove it for Fin n

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Init

lemma l2 {n : ℕ} [NeZero n] (h1 : n % 3 = 1) (h2 : n ≥ 3) : 3 * Fin.ofNat n (n / 3 - 1) = -4 := by
  have cast_mul (a b n : ℕ) [NeZero n] :
      Fin.ofNat n (a*b) = (Fin.ofNat n a) * (Fin.ofNat n b) := by
    refine Fin.eq_of_val_eq ?_
    unfold HMul.hMul; unfold instHMul; unfold Mul.mul; unfold Fin.instMul; unfold Fin.mul
    simp only [Fin.ofNat_eq_cast, Fin.val_natCast, Nat.mul_mod_mod, Nat.mod_mul_mod]
    unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
  have : (3 : Fin n) = Fin.ofNat n 3 := Fin.eq_of_val_eq rfl
  rw[this]
  rw[←cast_mul 3 (n/3-1)]
  have : 3 * (n/3-1) = n-4 := by grind
  rw[this]
  refine Fin.eq_of_val_eq ?_
  simp only [Fin.ofNat_eq_cast, Fin.val_natCast, Nat.self_sub_mod]
  unfold Fin.val; unfold Neg.neg; unfold Fin.neg; simp only [Fin.coe_ofNat_eq_mod]
  by_cases nf : n = 4
  · simp[nf]
  have : 4%n = 4 := by refine Nat.mod_eq_of_lt ?_; grind
  rw[this]; symm; exact Nat.self_sub_mod n 4

[metakuntyyy]

Fin n and ZMod n are equal when n is non-zero, so the proof shouldn't be much longer.

[Nathan]

i had to unfold a bunch of definitions to get cast_mul to work. but it just hit me, that maybe i need to import all of Mathlib to get access to more stuff. or maybe i need that CommRing instance you mentioned

[metakuntyyy]

I always import full mathlib, it usually doesn't hurt.

[Nathan]

Kevin Buzzard said:

h implies $n=3t+1$ and you seem to want to prove that $3t$ is $-4$ modulo $3t+1$ which is false in general unless I made a slip.

maybe you forgot to distribute something, it should be 3t-3 = -4 (mod 3t+1)

[Nathan]

this can be solved by grind but can the CommRing instance help here?

import Mathlib.Data.Nat.Init
import Mathlib.Data.ZMod.Defs

example {n : ℕ} [NeZero n] : (3 : Fin n) + (2 : Fin n) = (5 : Fin n) := by
  letI := Fin.instCommRing n
  simp
  sorry

[metakuntyyy]

Nathan said:

example {n : ℕ} [NeZero n] : (3 : Fin n) + (2 : Fin n) = (5 : Fin n) := by

No idea, but accessing the commRing instance of Fin is typically an antipattern. I would consider using ZMod in any case.

[Nathan]

i just dumped like 350 lines of code into gemini, and it understood everything (like that w stands for witness, res for residual terms). it's actually insane.

the code it provided was buggy as hell, but it found some good mathlib functions that i was able to take advantage of

[Nathan]

Screenshot 2026-01-30 at 4.26.16 AM.png
Screenshot 2026-01-30 at 4.26.37 AM.png
Screenshot 2026-01-30 at 4.26.49 AM.png

this is all completely accurate

[Nathan]

it had a cool strategy for the first problem too

[Nathan]

How can I rewrite these lines to avoid the warning? I don't think simp only will work, since I'm operating on multiple goals at once.

        by_cases c1 : (i.val % 3 = 0) <;> by_cases c2 : ((i+1).val % 3 = 0)
        <;> by_cases c3 : ((i+2).val % 3 = 0) <;> unfold f w m
        <;> simp[c1, c2, c3]

Screenshot 2026-01-31 at 3.48.52 AM.png

Here's more context

import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Fin.Tuple.Reflection

open Finset

noncomputable def f {n : ℕ} [NeZero n] (x : Fin n → NNReal) (i : Fin n) :=
  x i + NNReal.sqrt (x (i+1) * x (i+2))
noncomputable def maxf (n : ℕ) [NeZero n] (x : Fin n → NNReal) :=
  (Finset.image (f x) Finset.univ).max' (by simp)
theorem POTD_2490 {n : ℕ} [NeZero n] (hn : n ≥ 3) :
    Minimal (maxf n '' (fun x ↦ FinVec.sum x = 1)) (1 / (2*n/3 : ℕ)) := by
  let m : NNReal := 1 / (2*n/3 : ℕ)
  have oln : 1%n = 1 := Nat.mod_eq_of_lt (by grind only)
  have tln : 2%n = 2 := Nat.mod_eq_of_lt (by grind only)
  and_intros
  · let w (i : Fin n) := if i.val % 3 = 0 then 0 else m
    exists w; and_intros
    · change FinVec.sum w = 1
      simp only [w, FinVec.sum_eq]
      let s : Finset (Fin n) := {i | i.val % 3 = 0}
      let t : Finset (Fin n) := {i | ¬i.val % 3 = 0}
      have h1 : ∑ i ∈ s, w i = 0 := by
        convert ← Finset.sum_eq_card_nsmul _
        · exact nsmul_zero #{i : Fin n | i.val % 3 = 0}
        · unfold s; intro a ha; simp at ha; simp [w, ha]
      have h2 : ∑ i ∈ t, w i = #t • m := by
        unfold t; apply Finset.sum_eq_card_nsmul
        intro a ha; simp at ha; simp [w, ha]
      have h3 : #t = 2 * n / 3 := by
        have comp : #(s ∪ t) = #s + #t := by
          refine card_union_of_disjoint ?_
          exact disjoint_filter_filter_not univ univ fun i : Fin n ↦ i.val % 3 = 0
        rw[filter_union_filter_not_eq (fun i : Fin n ↦ i.val % 3 = 0) univ, card_fin n] at comp
        suffices #s = (n+2)/3 by lia
        refine card_eq_of_bijective (fun i ↦ fun _ ↦ Fin.ofNat n (i * 3)) ?_ ?_ ?_
        · intro a ah; unfold s at ah; simp only [mem_filter, mem_univ, true_and] at ah
          let ⟨j, jh⟩ := Nat.dvd_of_mod_eq_zero ah
          exists j; exists by have := jh ▸ a.isLt; lia
          simp only [Fin.ofNat_eq_cast]
          refine Fin.eq_of_val_eq ?_
          simp only [Fin.val_natCast]; rw[jh, mul_comm]
          exact Nat.mod_eq_of_lt (jh ▸ a.isLt)
        · intro i ih; unfold s
          simp only [Fin.ofNat_eq_cast, mem_filter, mem_univ, Fin.val_natCast, true_and]
          rw[show i*3%n = i*3 by refine Nat.mod_eq_of_lt (by lia)]; lia
        · intro i j ih jh; simp only [Fin.ofNat_eq_cast]; intro ijh
          replace ijh := Fin.val_eq_of_eq ijh; simp only [Fin.val_natCast] at ijh
          rw[show i*3%n = i*3 by refine Nat.mod_eq_of_lt (by lia)] at ijh
          rw[show j*3%n = j*3 by refine Nat.mod_eq_of_lt (by lia)] at ijh
          lia
      rw [← sum_filter_add_sum_filter_not _ fun i : Fin n ↦ i.val % 3 = 0, h1, h2, h3]
      simp only [nsmul_eq_mul, zero_add]
      refine mul_one_div_cancel (Nat.cast_ne_zero.mpr ?_)
      omega
    · refine (Finset.max'_eq_iff _ _ _).mpr ⟨?_, fun b bh ↦ ?_⟩
      · simp only [mem_image, mem_univ, true_and]
        exists 0; unfold f w m
        simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte, zero_add, oln, Nat.one_mod,
          one_ne_zero, tln, Nat.mod_succ, OfNat.ofNat_ne_zero, NNReal.sqrt_mul_self]
      · simp only [mem_image, mem_univ, true_and] at bh
        rcases bh with ⟨i, rfl⟩
        by_cases c1 : (i.val % 3 = 0) <;> by_cases c2 : ((i+1).val % 3 = 0)
        <;> by_cases c3 : ((i+2).val % 3 = 0) <;> unfold f w m
        <;> simp[c1, c2, c3]
        exfalso; clear w m oln tln
        sorry
  · sorry

[Nathan]

It creates 8 goals, and simp can close 7 of them

[Aaron Liu]

how about try (simp [c1, c2, c3]; done)

[Nathan]

oh it worked, thanks :pray: