Getting parameters that give the supremum of a set

Stream: new members

[Rida Hamadani]

I've defined the diameter of a SimpleGraph as:

noncomputable def diam (G : SimpleGraph α) : ℕ∞ :=
  sSup {d | ∃ u v : α, d = G.dist u v}

I would like to have a lemma stating that there exists u and v such that G.dist u v = G.diam, perhaps when α is finite.

import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Combinatorics.SimpleGraph.Girth
namespace SimpleGraph
variable {α : Type*} {G : SimpleGraph α}

noncomputable def diam (G : SimpleGraph α) : ℕ∞ :=
  sSup {d | ∃ u v : α, d = G.dist u v}

lemma diam_eq_dist (ht : G.diam ≠ ⊤) : -- is this condition correct?
    1 ≤ G.diam ↔ ∃ (u v : α), G.diam = G.dist u v ∧ G.Reachable u v ∧ u ≠ v := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  . sorry -- what to do
  . obtain ⟨u, v, h⟩ := h
    rw [h.1, Nat.one_le_cast]
    apply LT.lt.nat_succ_le (Reachable.pos_dist_of_ne h.2.1 h.2.2)

It seems that the perfect lemma to use here is docs#Nat.sSup_mem, but it needs a hypothesis stating that the set of distances is BddAbove. Or maybe we can use docs#Set.Nonempty.csSup_mem, but in that case, we need to show that the set is finite and non-empty.

In both cases, I don't know how to continue this, any help is highly appreciated!

[Rida Hamadani]

Actually I would be happy with a lemma of this form:

lemma diam_exists (ht : G.diam ≠ ⊤) : ∃ (u v : α),  G.dist u v = G.diam
  sorry

As proving the lemma above is easy after I've obtained such a lemma.

[Mitchell Lee]

You can apply this theorem to find the upper bound you need: ENat.iSup_coe_ne_top

[Mitchell Lee]

Sorry, maybe this doesn't work. I'll be back soon to find something.

[Mitchell Lee]

One way is to use WithTop.coe_untop to prove that G.diam is actually a natural number, and then use that as your upper bound.

[Matt Diamond]

You might need a Nonempty α assumption, unless I'm missing something

[Matt Diamond]

man, this is surprisingly annoying to prove... you'd think we'd have this lemma:

lemma ENat.sSup_mem_of_nonempty_ne_top
  {s : Set ℕ∞} (hs : s.Nonempty) (hs2 : sSup s ≠ ⊤) : sSup s ∈ s := sorry

[Rida Hamadani]

Thank you for the suggestions! I've read a bit in the file of WithTop.coe_untop and found another useful lemma WithTop.ne_top_iff_exists. Here is my code so far:

import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Combinatorics.SimpleGraph.Girth
namespace SimpleGraph
variable {α : Type*} {G : SimpleGraph α}

noncomputable def diam (G : SimpleGraph α) : ℕ∞ :=
  sSup {d | ∃ u v : α, d = G.dist u v}

lemma diam_exists (ht : G.diam ≠ ⊤) :
    ∃ (u v : α),  G.dist u v = G.diam := by
  obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp ht
  rw [← hn]
  simp only [ENat.some_eq_coe, Nat.cast_inj]
  /-
    α: Type u_1
    G: SimpleGraph α
    ht: diam G ≠ ⊤
    n: ℕ
    hn: ↑n = diam G
    ⊢ ∃ u v, dist G u v = n
  -/
  sorry

My problem is that I am unable to use a theorem such as Nat.sSup_def because of the coercion, so I am unable do something like this:

  have : ∀ d ∈ {d | ∃ u v : α, d = G.dist u v}, d ≤ n := by
    rw [hn] -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑n

[Matt Diamond]

docs#WithTop.sSup_eq might be relevant... if you could prove that WithTop.some ⁻¹' s is bounded above, then you could shift to the Nat context

[Rida Hamadani]

When I try something like:

  have hs' : BddAbove (WithTop.some ⁻¹' s) := by
    sorry

I get the following error:

/-
application type mismatch
  WithTop.some ⁻¹' s
argument
  s
has type
  Set ℕ : Type
but is expected to have type
  Set (WithTop ?m.3332) : Type
-/

Is there a way to get the statement accepted?

[Matt Diamond]

my guess is that when you defined s you didn't specify that the elements are ENats, so Lean assumed they were Nats

try something like this:

let s := {d : ℕ∞ | ∃ u v : α, d = G.dist u v}

[Rida Hamadani]

Maybe it is more useful to prove ENat.sSup_mem_of_nonempty_ne_top which you provided above first. I'll sleep on it today and reattempt proving it tomorrow. I'll use this topic to send any new questions I get. Thank you! :grinning_face_with_smiling_eyes:

[Matt Diamond]

sounds good... I've actually got a proof of diam_exists though it could probably use some golfing, I'll post shortly

[Matt Diamond]

lemma top_not_mem_of_sup_ne_top {s : Set ℕ∞} (hs : sSup s ≠ ⊤) : ⊤ ∉ s :=
by
  contrapose! hs
  rw [sSup_eq_top]
  intro b hb
  use ⊤, hs

lemma diam_exists [Nonempty α] (ht : G.diam ≠ ⊤) : ∃ (u v : α),  G.dist u v = G.diam :=
by
  unfold diam at *
  set s := {d : ℕ∞ | ∃ u v : α, d = G.dist u v}
  let s' := WithTop.some ⁻¹' s
  have nonempty_s' : s'.Nonempty := by
    have v := Classical.arbitrary α
    use 0, v, v
    exact congrArg _ SimpleGraph.dist_self.symm
  have bddAbove_s' : BddAbove s' := by
    simp_rw [sSup_eq_top.not] at ht
    push_neg at ht
    rcases ht with ⟨ub, ub_lt_top, hub⟩
    use WithTop.untop ub ub_lt_top.ne
    intro a ha
    rw [WithTop.le_untop_iff]
    rw [Set.mem_preimage] at ha
    exact hub a ha
  obtain ⟨u, v, huv⟩ := Nat.sSup_mem nonempty_s' bddAbove_s'
  have top_not_mem := top_not_mem_of_sup_ne_top ht
  rw [WithTop.sSup_eq top_not_mem bddAbove_s']
  use u, v, huv.symm