help with supr proof

Stream: general

[Bernd Losert]

import tactic
import order.filter.partial
import data.fin.tuple

example {α : Type*} (n₁ n₂ : ℕ) : ℕ :=
begin
  have g₁ : fin (n₁ + 1) → filter α, sorry,
  have g₂ : fin (n₂ + 1) → filter α, sorry,
  let n := n₁ + n₂,
  have hn : n + 2 = n₁ + 1 + (n₂ + 1), by ring_nf,
  let g : fin (n + 2) → filter α := fin.append hn g₁ g₂,
  have : supr g₁ ≤ supr g,
  begin
    refine supr_mono' _,
    intros i,
    use i,
    sorry,
  end,
  exact 0
end

The family g of filters is basically the family g₁ followed by the family g₂. And I want to show supr g₁ ≤ supr g and supr g₂ ≤ supr g. This is straighforward on paper, but I'm having trouble writing this formally in Lean. Any tips?

I wonder if it would be easier to just use sets of filters instead of fin-indexed families.

[Adam Topaz]

is there a supr_sum_eq_sup lemma somewhere?

[Adam Topaz]

docs#supr_sum

[Adam Topaz]

so if you can identify g with the supr over the sum type, that would let you reduce to le_sup_left and le_sup_right

[Adam Topaz]

or you could just use docs#supr_le

[Bernd Losert]

I had an attempt using supr_le, but I didn't get very far.

[Bernd Losert]

Using the sum seems interesting.

[Bernd Losert]

Hmm..., but I can't use a sum since I need to deal with fin indexed families only.

[Adam Topaz]

example {α : Type*} (n₁ n₂ : ℕ) : ℕ :=
begin
  have g₁ : fin (n₁ + 1) → filter α, sorry,
  have g₂ : fin (n₂ + 1) → filter α, sorry,
  let n := n₁ + n₂,
  have hn : n + 2 = n₁ + 1 + (n₂ + 1), by ring_nf,
  let g : fin (n + 2) → filter α := fin.append hn g₁ g₂,
  have : supr g₁ ≤ supr g,
  begin
    apply supr_le _, intros i,
    have : g₁ i = g i,
    { sorry },
    rw this,
    apply le_supr g,
  end,
  exact 0
end

[Adam Topaz]

I don't know how hard that sorry is with the current api for fin.append

[Yakov Pechersky]

docs#fin_sum_fin_equiv

[Bernd Losert]

Ah, fin_sum_fin_equiv is pretty handy here.

[Adam Topaz]

Maybe fin.append should be redefined using fin_sum_fin_equiv?

[Bernd Losert]

I'm thinking though... maybe I should just redefine g₁, g₂, g to be finite sets. I think it will be easier this way to prove the corresponding Sup inequalities.

[Adam Topaz]

working with indexed families is almost always better when you're using supr and infi

[Adam Topaz]

you could use arbitrary indexing types satisfying [fintype _] and use the sum type instead of the append

[Bernd Losert]

Yeah. However, indexed families feels too sophisticated to me, at least in Lean. I'm more comfortable dealing with sets.

[Adam Topaz]

It's much easier if you use types, e.g.

example {α : Type*} (a b : Type*) : ℕ :=
begin
  have g₁ : a → filter α, sorry,
  have g₂ : b → filter α, sorry,
  let g : a ⊕ b → filter α := λ t, sum.rec_on t g₁ g₂,
  have : supr g₁ ≤ supr g,
  begin
    rw [supr_le_iff], intros i,
    have : g₁ i = g (sum.inl i) := rfl,
    rw this, apply le_supr g (sum.inl i),
  end,
  exact 0
end

[Bernd Losert]

Nice. I'll try this out if I can't get a set-based proof going. Thanks a lot.

[Yakov Pechersky]

You'd have to prove this:

  have : ∀ (x), (fin.append hn g₁ g₂ x =
    (λ (i : fin (n₁ + 1) ⊕ fin (n₂ + 1)),
      sum.cases_on i g₁ g₂ : fin (n₁ + 1) ⊕ fin (n₂ + 1) → filter α)
      (fin_sum_fin_equiv.symm (fin.cast hn x))),

[Yakov Pechersky]

Which requires some lemmas about the application of fin.append which I don't see right now

[Yakov Pechersky]

And some of these:

lemma assist {α ι ι' : Type*} [complete_lattice α] (e : ι' ≃ ι) (f : ι → α) :
  supr f ≤ supr (f ∘ e) :=
begin
  rw le_supr_iff,
  intros a hg,
  refine supr_le (λ i, _),
  refine (hg (e.symm i)).trans' _,
  simp
end

lemma assist' {α ι ι' : Type*} [complete_lattice α] (e : ι' ≃ ι) (f : ι → α) :
  supr (f ∘ e) ≤ supr f :=
begin
  rw le_supr_iff,
  intros a hg,
  refine supr_le (λ i, _),
  refine (hg (e i)).trans' _,
  simp
end

[Yakov Pechersky]

or something of that natrue