filter coprod lemma

Stream: mathlib4

[Jireh Loreaux]

Can I nerdsnipe someone (maybe @Anatole Dedecker ?) into golfing this into oblivion for me? It seems like it should be far easier than this. I'm open to slight changes in the statement if it makes it easier. E.g., h₁ could become the equivalent statements: ∀ s ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc or ∃ᶠ s in la.smallSets, Tendsto f (𝓟 sᶜ ×ˢ lb) lc.

It seems like it should be easier than I'm making it out to be, most likely because I'm missing something obvious.

import Mathlib.Order.Filter.Prod

open Set Filter

lemma Filter.Tendsto.coprod_of_prod_top_right {α β γ : Type*}
    {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (h₁ : ∀ s : Set α, sᶜ ∈ la → Tendsto f (𝓟 s ×ˢ lb) lc)
    (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
    Tendsto f (la.coprod lb) lc := by
  rw [coprod_eq_prod_top_sup_top_prod]
  refine .sup h₂ ?_
  intro tc htc
  obtain ⟨ta, hta, h⟩ := by simpa [mem_prod_iff] using h₂ htc
  obtain ⟨ta', hta', tb, htb, h'⟩ := by simpa [mem_prod_iff] using h₁ taᶜ (by simpa) htc
  rw [mem_map, mem_prod_iff] at ⊢
  refine ⟨univ, univ_mem, tb, htb, Subset.trans ?_ (union_subset h h')⟩
  trans ta ×ˢ tb ∪ taᶜ ×ˢ tb
  · simp [← union_prod]
  · gcongr
    simp

[Jireh Loreaux]

(the context is that to show some function tendsto l along cobounded (α × β), it suffices to show that f tendsto to l along cobounded α ×ˢ ⊤ and along s × cobounded β for every bounded set s.)

[Aaron Liu]

Jireh Loreaux said:

E.g., h₁ could become the equivalent statements: ∀ s ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc or ∃ᶠ s in la.sets, Tendsto f (𝓟 sᶜ ×ˢ lb) lc.

Is ∃ᶠ s in la.sets, Tendsto f (𝓟 sᶜ ×ˢ lb) lc type correct?

[Jireh Loreaux]

sorry, I meant smallSets, corrected now.

[Aaron Liu]

I think you can probably do some coheyting magic here but the coframe structure on filters isn't really developed in mathlib

[Aaron Liu]

there's just docs#Filter.instCoframe

[Aaron Liu]

not really much else

[Bhavik Mehta]

Does grind count as oblivion? I switched to the first alternate version of h1 that you suggested

import Mathlib.Order.Filter.Prod

open Set Filter

lemma Filter.Tendsto.coprod_of_prod_top_right {α β γ : Type*}
    {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (h₁ : ∀ s : Set α, s ∈ la → Tendsto f (𝓟 sᶜ ×ˢ lb) lc)
    (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
    Tendsto f (la.coprod lb) lc := by
  simp only [coprod_eq_prod_top_sup_top_prod, tendsto_sup, mem_top, tendsto_prod_iff]
  grind [mem_top, mem_principal, tendsto_prod_iff]

[Anatole Dedecker]

Here's my proposal for a proof staying in filter land. I'm not satisfied, because it is still quite long and it relies on ultrafilters, but I don't have much more time to actively think about this for now.

import Mathlib.Order.Filter.Prod
import Mathlib.Order.Filter.Ultrafilter.Basic

open Set Filter

lemma Filter.Tendsto.coprod_of_prod_top_right {α β γ : Type*}
    {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (h₁ : ∀ s : Set α, s ∈ la → Tendsto f (𝓟 sᶜ ×ˢ lb) lc)
    (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
    Tendsto f (la.coprod lb) lc := by
  rw [tendsto_iff_ultrafilter]
  intro u hu
  rw [coprod_eq_prod_top_sup_top_prod, Ultrafilter.le_sup_iff] at hu
  by_cases hu' : (u : Filter (α × β)) ≤ la ×ˢ ⊤
  · exact h₂.mono_left hu'
  · replace hu := hu.resolve_left hu'
    simp_rw [prod_top, ← tendsto_iff_comap, not_tendsto_iff_exists_frequently_notMem,
      Ultrafilter.frequently_iff_eventually] at hu'
    rcases hu' with ⟨s, hs, hsu⟩
    exact h₁ s hs |>.mono_left <|
      le_prod.mpr ⟨by simpa, by simpa [top_prod, tendsto_iff_comap] using hu⟩

[Anatole Dedecker]

Aaron Liu said:

I think you can probably do some coheyting magic here but the coframe structure on filters isn't really developed in mathlib

If I'm understanding correctly your suggestion, my proof is essentially doing this but using ultrafilters as points to make my life easier (I don't think this is true actually)

[Anatole Dedecker]

Here is another version of the same argument:

import Mathlib.Order.Filter.Prod
import Mathlib.Order.Filter.Ultrafilter.Basic

open Set Filter

lemma Filter.foo {α β : Type*}
    {la : Filter α} {lb : Filter β} :
    la.coprod lb = (la ×ˢ ⊤) ⊔ ⨆ s ∈ la, 𝓟 sᶜ ×ˢ lb := by
  rw [coprod_eq_prod_top_sup_top_prod, sup_eq_sup_iff_left]
  constructor
  · rw [prod_top, top_prod, le_iff_ultrafilter]
    simp_rw [Ultrafilter.le_sup_iff, ← tendsto_iff_comap, or_iff_not_imp_left,
      not_tendsto_iff_exists_frequently_notMem, Ultrafilter.frequently_iff_eventually]
    intro u hu ⟨s, hs, hsu⟩
    exact le_iSup₂_of_le s hs (by simp [le_prod, hsu, hu])
  · exact iSup₂_le fun s hs ↦ le_sup_of_le_right (prod_mono le_top le_rfl)

lemma Filter.Tendsto.coprod_of_prod_top_right {α β γ : Type*}
    {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (h₁ : ∀ s : Set α, s ∈ la → Tendsto f (𝓟 sᶜ ×ˢ lb) lc)
    (h₂ : Tendsto f (la ×ˢ ⊤) lc) :
    Tendsto f (la.coprod lb) lc := by
  simpa [foo, tendsto_sup, tendsto_iSup, h₂]