Proving symmetry

Stream: new members

[David⚛️]

import Mathlib

noncomputable def pbc (position cell_length : ℝ) : ℝ :=  position - cell_length * round (position / cell_length)

noncomputable def minImageDistance (cell_length posA posB : Fin n → ℝ) : ℝ :=
  let dist := fun i => pbc (posB i - posA i) (cell_length i)
  (Finset.univ.sum (fun i => (dist i) ^ 2)).sqrt

theorem minImageDistance_symm (cell_length posA posB : Fin n → ℝ) :
  minImageDistance cell_length posA posB = minImageDistance cell_length posB posA := by
  unfold minImageDistance
  suffices h : ∑ i, (pbc (posB i - posA i) (cell_length i))^2 = ∑ i, (pbc (posA i - posB i) (cell_length i))^2
  · simp only [h]

  -- Prove symmetry term-by-term
  have h_term : ∀ i, (pbc (posB i - posA i) (cell_length i))^2 = (pbc (posA i - posB i) (cell_length i))^2 := by
    intro i
    unfold pbc
    -- Break the goal into sub-terms for clarity
    let a := posB i - posA i
    let b := posA i - posB i

    -- We need to show the equality directly rather than using rewrite
    calc
      (a - cell_length i * round (a / cell_length i))^2 = (-(b) - cell_length i * round (-(b) / cell_length i))^2 := by
       congr
       · ring
       · ring
    _  = (b - cell_length i * round (b / cell_length i))^2 := by  sorry

I need help to close up the goal

[Ruben Van de Velde]

Seems like you're missing imports

[Kevin Buzzard]

(just edit your original post, so that the "view in Lean 4 playground" link works)

[David⚛️]

Kevin Buzzard said:

(just edit your original post, so that the "view in Lean 4 playground" link works)

I just edited it. Thanks

[Kevin Buzzard]

Now I get

application type mismatch
  Finset.sum_congr rfl h_term
argument
  h_term
has type
  ∀ (i : Fin n), pbc (posB i - posA i) (cell_length i) ^ 2 = pbc (posA i - posB i) (cell_length i) ^ 2 : Prop
but is expected to have type
  ∀ x ∈ Finset.univ, pbc (posB x - posA x) (cell_length x) ^ 2 = pbc (posA x - posB x) (cell_length x) ^ 2 : Prop

[Kevin Buzzard]

It would be good if the code contained no errors and could just be run by other people with one click. That way you are likely to get more help.

[Kevin Buzzard]

Or perhaps you should clarify your question

[David⚛️]

Kevin Buzzard said:

Or perhaps you should clarify your question

No errors now.

[Ruben Van de Velde]

Is it true? I got as far as

import Mathlib

noncomputable def pbc (position cell_length : ℝ) : ℝ :=  position - cell_length * round (position / cell_length)

noncomputable def minImageDistance (cell_length posA posB : Fin n → ℝ) : ℝ :=
  let dist := fun i => pbc (posB i - posA i) (cell_length i)
  (Finset.univ.sum (fun i => (dist i) ^ 2)).sqrt

theorem minImageDistance_symm (cell_length posA posB : Fin n → ℝ) :
  minImageDistance cell_length posA posB = minImageDistance cell_length posB posA := by
  unfold minImageDistance
  suffices h : ∑ i, (pbc (posB i - posA i) (cell_length i))^2 = ∑ i, (pbc (posA i - posB i) (cell_length i))^2
  · simp only [h]

  -- Prove symmetry term-by-term
  have h_term : ∀ i, (pbc (posB i - posA i) (cell_length i))^2 = (pbc (posA i - posB i) (cell_length i))^2 := by
    intro i
    unfold pbc
    -- Break the goal into sub-terms for clarity
    let a := posB i - posA i
    let b := posA i - posB i

    -- We need to show the equality directly rather than using rewrite
    calc
      (a - cell_length i * round (a / cell_length i))^2 = (-(b) - cell_length i * round (-(b) / cell_length i))^2 := by
       congr
       · ring
       · ring
    _  = (b - cell_length i * round (b / cell_length i))^2 := by
      rw [← neg_sq, neg_sub', neg_neg, ← mul_neg, ← Int.cast_neg]
      congr
      rw [round_eq, round_eq, ← Int.ceil_neg, neg_add, neg_div, neg_neg, ← sub_eq_add_neg]
      sorry

[Tyler Josephson ⚛️]

Thanks for your help! By the way, we figured out why this isn't a true theorem. At the edge case where (posA i - posB i) / cell_length is exactly equal to 0.5 or another number exactly halfway between numbers, then the reverse, (posB i - posA i) / cell_lengthis equal to -0.5. The former rounds up to 1, but the latter also rounds up to 0, making the theorem not true.