Idiomatic proof of "denseness" of `finset.range`

Stream: Is there code for X?

[Yakov Pechersky]

What is the idiomatic way of proving the following? The approach will be useful for me to learn more about idiomatic proofs during building the infinite product API.

import analysis.p_series

noncomputable theory
open finset filter function classical
open_locale topology classical filter

example (f : finset ℕ → ℝ) (x : ℝ) (hf : monotone f)
  (h : tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x)) :
  tendsto (λ s : finset ℕ, f s) at_top (𝓝 x) :=
sorry

[Yakov Pechersky]

The underlying motivation is the following calculation image.png

[Kevin Buzzard]

Here's a probably non-idiomatic proof:

import analysis.p_series

noncomputable theory
open finset filter function classical
open_locale topology classical big_operators filter

lemma le_range (s : finset ℕ) : ∃ n : ℕ, s ≤ range n :=
  (finset.range_mono.tendsto_at_top_at_top_iff).1 filter.tendsto_finset_range _

example (f : finset ℕ → ℝ) (x : ℝ) (hf : monotone f)
  (h : tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x)) :
  tendsto (λ s : finset ℕ, f s) at_top (𝓝 x) :=
begin
  have hf' : monotone (λ n, f (range n)) := λ a b hab, hf (range_mono hab),
  have frange_bdd := hf'.ge_of_tendsto h,
  have f_bdd : ∀ (s : finset ℕ), f s ≤ x,
  { intro s,
    obtain ⟨n, hn⟩ := le_range s,
    exact le_trans (hf hn) (frange_bdd n), },
  rw metric.tendsto_nhds at h ⊢,
  intros ε hε,
  specialize h ε hε,
  obtain ⟨a, ha⟩ := mem_at_top_sets.1 h,
  specialize ha a (le_refl a),
  refine mem_at_top_sets.2 _,
  use range a,
  intros s hs,
  have h1 : f (range a) ≤ f s := hf hs,
  have h2 : f s ≤ x := f_bdd s,
  dsimp at ⊢ ha,
  rw [real.dist_eq, abs_lt] at ha ⊢,
  split; linarith,
end

[Kevin Buzzard]

I had to resort to epsilons but I don't really see any other way.

[Patrick Massot]

I would say that

example (f : finset ℕ → ℝ) (x : ℝ) (hf : monotone f)
  (h : tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x)) :
  tendsto f at_top (𝓝 x) :=
(tendsto_iff_tendsto_subseq_of_monotone hf tendsto_finset_range).mpr h

is more idiomatic.

[Patrick Massot]

It's even more idiomatic to change the statement to the iff version:

example (f : finset ℕ → ℝ) (x : ℝ) (hf : monotone f) :
  tendsto f at_top (𝓝 x) ↔ tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x) :=
tendsto_iff_tendsto_subseq_of_monotone hf tendsto_finset_range

[Yakov Pechersky]

Wonderful, thank you! Now, the same seems to be true for antitone f. Is there a more general catch-all that deals with both cases?

[Patrick Massot]

I don't know.

[David Loeffler]

There isn't even a definition in mathlib for "either monotone increasing or monotone decreasing" (i.e. what most mathematicians mean by "monotone"), is there?

[Yaël Dillies]

Yes there is, if you are willing to constrain the base type: docs#quasilinear_on

[Yakov Pechersky]

For reference, here are the companion statements for antitone functions:

import topology.algebra.order.monotone_convergence

open filter set function finset
open_locale filter topology classical
variables {ι α β : Type*}

lemma at_top_dual_eq_at_bot [preorder α] :
  (at_top : filter αᵒᵈ).map order_dual.of_dual = (at_bot : filter α) := rfl
lemma at_bot_dual_eq_at_top [preorder α] :
  (at_bot : filter αᵒᵈ).map order_dual.of_dual = (at_top : filter α) := rfl

lemma tendsto_at_top_at_bot_of_antitone [preorder α] [preorder β] {f : α → β} (hf : antitone f)
  (h : ∀ b, ∃ a, f a ≤ b) :
  tendsto f at_top at_bot :=
begin
  rw [←at_bot_dual_eq_at_top, tendsto_map'_iff],
  exact tendsto_at_bot_at_bot_of_monotone hf.dual_left h,
end

lemma tendsto_at_bot_at_top_of_antitone [preorder α] [preorder β] {f : α → β} (hf : antitone f)
  (h : ∀ b, ∃ a, b ≤ f a) :
  tendsto f at_bot at_top :=
begin
  rw [←at_top_dual_eq_at_bot, tendsto_map'_iff],
  exact tendsto_at_top_at_top_of_monotone hf.dual_left h,
end

lemma tendsto_at_top_at_bot_iff_of_antitone [nonempty α] [semilattice_sup α] [preorder β]
  {f : α → β} (hf : antitone f) :
  tendsto f at_top at_bot ↔ ∀ b : β, ∃ a : α, f a ≤ b :=
tendsto_at_top_at_bot.trans $ forall_congr $ λ b, exists_congr $ λ a,
  ⟨λ h, h a (le_refl a), λ h a' ha', le_trans (hf ha') h⟩

lemma tendsto_at_bot_at_top_iff_of_antitone [nonempty α] [semilattice_inf α] [preorder β]
  {f : α → β} (hf : antitone f) :
  tendsto f at_bot at_top ↔ ∀ b : β, ∃ a : α, b ≤ f a :=
tendsto_at_bot_at_top.trans $ forall_congr $ λ b, exists_congr $ λ a,
  ⟨λ h, h a (le_refl a), λ h a' ha', le_trans h (hf ha')⟩

alias tendsto_at_top_at_bot_of_antitone ← _root_.antitone.tendsto_at_top_at_bot
alias tendsto_at_bot_at_top_of_antitone ← _root_.antitone.tendsto_at_bot_at_top
alias tendsto_at_top_at_bot_iff_of_antitone ← _root_.antitone.tendsto_at_top_at_bot_iff
alias tendsto_at_bot_at_top_iff_of_antitone ← _root_.antitone.tendsto_at_bot_at_top_iff

/-- If `u` is an antitone function with linear ordered codomain and the range of `u` is not bounded
below, then `tendsto u at_top at_bot`. -/
lemma tendsto_at_top_at_bot_of_antitone' [preorder ι] [linear_order α]
  {u : ι → α} (h : antitone u) (H : ¬bdd_below (range u)) :
  tendsto u at_top at_bot :=
begin
  apply h.tendsto_at_top_at_bot,
  intro b,
  rcases not_bdd_below_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩,
  exact ⟨N, le_of_lt hN⟩
end

lemma tendsto_of_antitone {ι α : Type*} [preorder ι] [topological_space α]
  [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : antitone f) :
  tendsto f at_top at_bot ∨ (∃ l, tendsto f at_top (𝓝 l)) :=
if H : bdd_below (range f) then or.inr ⟨_, tendsto_at_top_cinfi h_mono H⟩
else or.inl $ tendsto_at_top_at_bot_of_antitone' h_mono H

lemma tendsto_at_top_iff_tendsto_range_at_top
  [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  [no_max_order α] {f : finset ℕ → α} {x : α} (hf : monotone f) :
  tendsto f at_top (𝓝 x) ↔ tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x) :=
tendsto_iff_tendsto_subseq_of_monotone hf tendsto_finset_range

lemma tendsto_iff_tendsto_subseq_of_antitone {ι₁ ι₂ α : Type*} [semilattice_sup ι₁] [preorder ι₂]
  [nonempty ι₁] [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  [no_min_order α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : antitone f)
  (hg : tendsto φ at_top at_top) :
  tendsto f at_top (𝓝 l) ↔ tendsto (f ∘ φ) at_top (𝓝 l) :=
begin
  split; intro h,
  { exact h.comp hg },
  { rcases tendsto_of_antitone hf with h' | ⟨l', hl'⟩,
    { exact (not_tendsto_at_bot_of_tendsto_nhds h (h'.comp hg)).elim },
    { rwa tendsto_nhds_unique h (hl'.comp hg) } }
end

lemma tendsto_at_top_iff_tendsto_range_at_top'
  [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  [no_min_order α] {f : finset ℕ → α} {x : α} (hf : antitone f) :
  tendsto f at_top (𝓝 x) ↔ tendsto (λ n : ℕ, f (range n)) at_top (𝓝 x) :=
tendsto_iff_tendsto_subseq_of_antitone hf tendsto_finset_range