Multiple indices in iSup

Stream: new members

[Gareth Ma]

How should I prove the following, or deal with iSup with multiple arguments in general?

example {f : ℝ → ℝ → ℝ} {s t : Set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ t)
      (hf : BddAbove (Set.range f.uncurry)) :
    f a b ≤ ⨆ (x ∈ s) (y ∈ t), f x y := by
  sorry

[Gareth Ma]

If it's a single index f a <= sup (x in s), f x, then I can use le_iSup and prove a is in s

[Gareth Ma]

But it seems the multiple indexing iSup above is just a shorthand for ⨆ x ∈ s, ⨆ y ∈ t, f x y

[Kevin Buzzard]

Not at lean right now but why doesn't the le_iSup approach still work?

[Gareth Ma]

Because le_iSup is $x \in s \implies f(x) \leq \bigsqcup_{x \in s} f(x)$, but here $f(a, b) \neq \bigsqcup_{y \in t} f(x, y)$ for any $x$

[Gareth Ma]

Oh but replacing $\neq$ by $\le$ holds, so I can use le_iSup for the inner iSup, then for the outer one, and trans them/calc them together

[Gareth Ma]

oops, let me try

[Kevin Buzzard]

Oh I see, so you need some lemma relating the sup of the sup to the sup over the set prod probably

[Gareth Ma]

Yeah exactly

[Gareth Ma]

There is

[Gareth Ma]

!docs4 le_iSup₂

[Gareth Ma]

#docs4 le_iSup₂

[Gareth Ma]

ok i give up but

[Gareth Ma]

le_iSup₂

[Gareth Ma]

But that is indexing over a type, and apparently we don't have

example {f : ℝ → ℝ} (s : Set ℝ) : (⨆ (x ∈ s), f x) = (⨆ (x : s), f (x : ℝ)) := by
  exact?

I can work on that I guess

[Gareth Ma]

Nevermind, there is iSup_subtype'. What I stated is incorrect because \R doesn't have a \top

[Gareth Ma]

No it's incorrect because of this

[Gareth Ma]

def f' : ℝ → ℝ := -1
def s' : Set ℝ := {1}

example : ⨆ (x ∈ s'), f' x = 0 := by
  have : Set.range (fun x ↦ ⨆ (_ : x ∈ s'), f' x) = {0, -1} := by
    apply subset_antisymm
    · intro x
      simp [s', f']
      rintro y rfl
      by_cases hy : y = 1 <;> [right; left] <;> simp [hy]
    · intro x h
      simp_all [s', f']
      cases' h with h h <;> subst h <;> [use 0; use 1] <;> simp
  rw [iSup, this]
  simp

example : ⨆ (x : s'), f' x = -1 := by
  have : Set.range (fun x : s' ↦ f' x) = {-1} := by ext x; simp [s', f']
  rw [iSup, this, csSup_singleton]

[Gareth Ma]

I feel like this might be confusing to other new members..

[Yakov Pechersky]

I have a PR currently improving our ciSup API

[Yakov Pechersky]

And a branch I'm working on that further treats it like a big operator

[Yakov Pechersky]

Gareth Ma said:

Nevermind, there is iSup_subtype'. What I stated is incorrect because \R doesn't have a \top

Actually, because it doesn't have a bot if we're talking ciSup

[Yakov Pechersky]

Gareth, you need a hypothesis either that your f is nonnegative along s x t, or that s and t are univ

[Gareth Ma]

Great to hear about your PR, looking forward to it :D

Gareth, you need a hypothesis either that your f is nonnegative along s x t, or that s and t are univ

Yes I realised. I think if s and t are univ then I can change it to iSup (not ciSup), and I saw a lemma that rewrites iSup (fun x => iSup (fun y => f x y)) to iSup over the product type. Anyways it's not what I want, what I really want is the \Sup (x : s) one, so I will just use that :)

[Yakov Pechersky]

#15271, #15284