limsup_antitone_continuous_eq_antitone_continuous_liminf

Stream: Is there code for X?

[Kalle Kytölä]

Do we have reasonable statements of the following kind? (Specializing to the at_top filter is probably not optimal generality, but the question is if I'm missing existing results from the library.)

lemma limsup_antitone_continuous_eq_antitone_continuous_liminf
  {ι R : Type*} [semilattice_sup ι] [nonempty ι]
  [complete_linear_order R] [topological_space R] [order_topology R]
  (a : ι → R) {f : R → R} (f_decr : antitone f) (f_cont : continuous f) :
  at_top.limsup (f ∘ a) = f (at_top.liminf a) :=
sorry

[Kalle Kytölä]

I also did not find related lemmas about Sup and Inf under decreasing (continuous) functions. Or increasing (continuous) functions for that matter. Below are clumsy proofs. I'd greatly appreciate an answer to Is there code for X? about any of them. Thanks!

import topology.order.lattice
import topology.instances.ennreal

open set filter order

lemma Sup_antitone_le_antitone_Inf {R S : Type*} [complete_semilattice_Inf R]
  [complete_linear_order S]
  -- It should be enough to assume `[complete_semilattice_Sup S] [linear_order S]`
  -- but how to make the `≤` of these two match?
  {f : R → S} (f_decr : antitone f) (A : set R) :
  Sup (f '' A) ≤ f (Inf A) :=
begin
  refine Sup_le _,
  intros x x_in_fA,
  rcases (mem_image f A x).mp x_in_fA with ⟨z, ⟨z_in_A, fz_eq_x⟩⟩,
  by_contra b_gt,
  have key := (f_decr (Inf_le z_in_A)),
  rw fz_eq_x at key,
  exact (lt_self_iff_false x).mp (lt_of_le_of_lt key (not_le.mp b_gt)),
end

lemma continuous_Inf_le_Sup_continuous {R S : Type*}
  [complete_linear_order R] [topological_space R] [order_topology R]
  [complete_linear_order S] [topological_space S] [order_closed_topology S]
  {f : R → S} (f_cont : continuous f)
  (A : set R) (hA : A.nonempty):
  f (Inf A) ≤ Sup (f '' A) :=
begin
  refine le_Sup_iff.mpr _,
  intros b hb,
  have InfA_mem_clA : Inf A ∈ closure A, from Inf_mem_closure hA,
  have aux := @continuous.continuous_on _ _ _ _ f (closure A) f_cont,
  have key := (continuous_on.image_closure aux).trans (closure_mono (show f '' A ⊆ Iic b, from hb)),
  simpa [closure_Iic] using key (mem_image_of_mem f InfA_mem_clA),
end

lemma Sup_antitone_eq_antitone_Inf {R S : Type*}
  [complete_linear_order R] [topological_space R] [order_topology R]
  [complete_linear_order S] [topological_space S] [order_closed_topology S]
  {f : R → S} (f_decr : antitone f) (f_cont : continuous f)
  (A : set R) (hA : A.nonempty):
  Sup (f '' A) = f (Inf A) :=
begin
  refine le_antisymm _ _,
  { apply Sup_antitone_le_antitone_Inf f_decr, },
  { exact continuous_Inf_le_Sup_continuous f_cont A hA, },
end

lemma Inf_antitone_eq_antitone_Sup {R S : Type*}
  [complete_linear_order R] [topological_space R] [order_topology R]
  [complete_linear_order S] [topological_space S] [order_closed_topology S]
  {f : R → S} (f_decr : antitone f) (f_cont : continuous f)
  (A : set R) (hA : A.nonempty):
  Inf (f '' A) = f (Sup A) :=
begin
  apply @Sup_antitone_eq_antitone_Inf (order_dual R) (order_dual S) _ _ _ _ _ _ f _ f_cont A hA,
  exact λ r₁ r₂ h, @f_decr r₂ r₁ h,
end

lemma limsup_eq_Inf_Sup {ι R : Type*}
  [semilattice_sup ι] [nonempty ι]
  [complete_linear_order R] [topological_space R] [order_topology R]
  (a : ι → R) :
  at_top.limsup a = Inf ((λ i, Sup (a '' (Ici i))) '' univ) :=
begin
  refine le_antisymm _ _,
  { rw limsup_eq,
    apply Inf_le_Inf,
    intros x hx,
    simp only [image_univ, mem_range] at hx,
    rcases hx with ⟨j, hj⟩,
    filter_upwards [Ici_mem_at_top j],
    intros i hij,
    rw ← hj,
    exact le_Sup (mem_image_of_mem _ hij), },
  { rw limsup_eq,
    apply le_Inf_iff.mpr,
    intros b hb,
    simp only [mem_set_of_eq, eventually_at_top] at hb,
    rcases hb with ⟨j, hj⟩,
    apply Inf_le_of_le (mem_image_of_mem _ (mem_univ j)),
    apply Sup_le,
    intros x hx,
    simp at hx,
    rcases hx with ⟨k, j_le_k, ak_eq_x⟩,
    rw ← ak_eq_x,
    exact hj k j_le_k, },
end

lemma liminf_eq_Sup_Inf {ι R : Type*}
  [semilattice_sup ι] [nonempty ι]
  [complete_linear_order R] [topological_space R] [order_topology R]
  (a : ι → R) :
  at_top.liminf a = Sup ((λ i, Inf (a '' (Ici i))) '' univ) :=
@limsup_eq_Inf_Sup ι (order_dual R) _ _ _ _ _ a

lemma liminf_antitone_continuous_eq_antitone_continuous_limsup
  {ι R : Type*} [semilattice_sup ι] [nonempty ι]
  [complete_linear_order R] [topological_space R] [order_topology R]
  (a : ι → R) {f : R → R} (f_decr : antitone f) (f_cont : continuous f) :
  at_top.liminf (f ∘ a) = f (at_top.limsup a) :=
begin
  rw [limsup_eq_Inf_Sup, liminf_eq_Sup_Inf,
      ←Sup_antitone_eq_antitone_Inf f_decr f_cont _ (nonempty_image_iff.mpr (@univ_nonempty ι _))],
  apply congr_arg,
  simp_rw [image_image, function.comp_app, image_univ],
  apply congr_arg,
  funext n,
  rw ← Inf_antitone_eq_antitone_Sup f_decr f_cont _ (nonempty_image_iff.mpr nonempty_Ici),
  simp_rw image_image,
end

lemma limsup_antitone_continuous_eq_antitone_continuous_liminf
  {ι R : Type*} [semilattice_sup ι] [nonempty ι]
  [complete_linear_order R] [topological_space R] [order_topology R]
  (a : ι → R) {f : R → R} (f_decr : antitone f) (f_cont : continuous f) :
  at_top.limsup (f ∘ a) = f (at_top.liminf a) :=
begin
  apply @liminf_antitone_continuous_eq_antitone_continuous_limsup ι (order_dual R) _ _ _ _ _ a f _ f_cont,
  exact λ r₁ r₂ h, @f_decr r₂ r₁ h,
end

[Floris van Doorn]

There is docs#antitone.le_map_Inf

[Floris van Doorn]

(with type-class assumptions that are neither stronger nor weaker than yours, but which can probably be weakened)

[Floris van Doorn]

and docs#filter.limsup_eq_infi_supr might be as convenient as your version?

[Kalle Kytölä]

Thanks!

Meanwhile I had created a PR, #15218.

[Kalle Kytölä]

I indeed did not succeed in reducing to docs#antitone.le_map_Inf and friends. :oh_no:

[Kalle Kytölä]

And I just had noticed docs#filter.limsup_eq_infi_supr, which (with its liminf-counterpart), as you say, should get rid of two lemmas above.

[Kalle Kytölä]

But is it really true that the result limsup_antitone_continuous_eq_antitone_continuous_liminf does not currently exist in this or similar enough form?

[Jireh Loreaux]

I think we don't because a while ago I had a PR for ennreal.inv_limsup and friends, which I needed for the Gelfand formula.

[Kalle Kytölä]

I still had difficulties using those existing lemmas, which seem like they should help. :worried:

I marked the PR as "help wanted", because it seems likely I am not doing things the ideal way. But since I would nevertheless like the limsup_antitone_continuous_eq_antitone_continuous_liminf result merged into mathlib, I simultaneously marked it as "awaiting review". I hope thus leaving the judgement to reviewers is not terribly rude here.