How to index over two elements in suprenum definition.

Stream: lean4

[Robert]

Hey, i am a bit stuck on how to write this formally in Lean.
image.png

I tried it as follows but can't get it to work

def trial(G :ℝ → ℝ) : ℝ :=
  ⨆ x y:ℝ,  x ≠ y, (G(x - y)) / (x - y)

but it doesnt compile and says unexpected identifier; expected ','

can anyone help me? I don't know how to index over two elements in the suprenum definition, https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html#supr

this doesn't help either: (

[Ruben Van de Velde]

Does ⨆ x y:ℝ, ⨆ (h : x ≠ y), (G(x - y)) / (x - y) work?

[Kevin Buzzard]

I don't think Lean would like G( either. This should work:

⨆ x : ℝ, ⨆ y : ℝ, ⨆ (h : x ≠ y), (G (x - y)) / (x - y)

but I always get confused about how to make this shorter.

[Robert]

Thank you @Kevin Buzzard it works! and @Ruben Van de Velde that unfortunately didn't work: (

[Sébastien Gouëzel]

The right way is

import Mathlib

noncomputable def trial (G :ℝ → ℝ) : ℝ :=
  sSup {a | ∃ x y, x ≠ y ∧ a = G (x - y) / (x - y)}

The strategy using ⨆ will not give what you expect because of issues with the supremum of the empty set in ℝ.

[Ruben Van de Velde]

Thanks for thinking :)

[Kevin Buzzard]

Aah yes I remember this gotcha and now I've fallen into the trap

[Robert]

Oh thanks @Sébastien Gouëzel ! That is a great solution!