filters.lean

import tactic
import data.real.basic
import topology.metric_space.basic

notation `|` x `|` := abs x

namespace epsilon_delta

/-!
## Epsilon-Delta - Motivation for Filters

To understand filters, and why we need them, first we must look at the ε-δ definition of the
limit, that is f(x) → L as x → p if

∀ ε > 0, ∃ δ > 0, ∀ x, 0 < |x - p| < δ → |f(x) - L| < ε
-/

def limit_of_function (f : ℝ → ℝ) (p L : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - p| < δ → |f x - L| < ε

/-!
On the other hand, we also have limits of sequences
-/

def limit_of_sequence (x : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |x n - c| < ε

/-!
and a variety of other limits too, such as one sided limits, limits to infinity, ...

With this, we end up with `k` different limits. 

Doesn't seem too bad so far? But we can have different source/targets for ±∞, rationals, ...

Now we have `k * k` different definitions.

Worse still, limits compose. Now we're up to `k * k * k` different definitions.

Patrick Massot determined that `k = 13`, and defining all of those lemmas does not scale. Therefore
we introduce the idea of filters to tie everything together, and different types of limits can be
defined by defining new filters, and the composition lemmas will only need to be proven once.
-/

end epsilon_delta

open epsilon_delta

namespace filters_game

/-!
## Filters - Intuitively

This section isn't going to have much Lean code, rather it is an explanation for what Filters are 
(in a simplified example). We're not even going to define a filter properly right now.

Let X be the set (Type) we're working in, this could be ℕ, ℝ, ℝ^2, ...

Then let ℱ be a collection of subsets of X satisfying a certain property. For now, let's just say 
that the property is that the set is "big".

### Neighbourhood

For a point l in X (which we will take to be some metric space for now), we can say that a subset U 
is "big" if and only if there exists δ > 0 such that N_δ(l) ⊆ U, that is, for all x ∈ U, d(x, l) < δ.

The neighbourhoods of l when δ gets smaller and smaller is similar to "zooming in" when we let 
δ → 0 in the definition of the limit of a real function. In fact, for the real line, this is the 
same definition. Intuitively, we use the neighbourhood filter to represent getting closer and closer
to a point.

### Principal Filter

Let s ⊆ X be a set, then we can define the principal filter on s, 𝓟(s), as all of the supersets of 
X. For example, 𝓟(∅) includes all subsets of X, and 𝓟(univ) = {univ}.

### At Top

Next, we can look at X = ℕ, and we say a set U is big if it has some minimum value a, and for all 
b ≥ a, b ∈ U. For example, {1,2,3,...} would be big, so would {795, 796, ...}, but {1,3,4,7, ...} 
would not be.

With the ε-N definition of a limit of a sequence, we said that for some fixed N, all n ≥ N satisfies
some property. This is the same as the at top filter, since we just choose an element of the filter,
and then say that the property holds for all elements of the set.

Equally, we can also set X = ℝ, and then we can define the at top filter similarly. With this, we
can use the at top filter to represent the values in the filter getting bigger and bigger. That is,
x → ∞.

Equivalently, we also have the at bot filter, which we use to represent x → -∞.

## Filters - Formal Mathematical Definition

A filter ℱ on a set (Type) X is a collection of subsets of X such that

- X ∈ ℱ (the whole space/set/type is in the filter)
- If U ∈ ℱ and U ⊆ V, then V ∈ ℱ (anything bigger than something in the filter must also be in the 
    filter)
- If U, V ∈ ℱ, then U ∩ V ∈ ℱ (the intersection of two big sets is big)

## Filters - In Lean
-/

-- A filter F on some type X
structure filter (X : Type*) :=
-- Is a collection of subsets of X
(sets : set (set X))
-- such that X is in the sets
(univ_mem : set.univ ∈ sets)
-- anything bigger is also in the filter
(superset_mem : ∀ {U V}, U ∈ sets → U ⊆ V → V ∈ sets)
-- and the intersection of two things in the filter is also in the filter
(inter_mem : ∀ {U V}, U ∈ sets → V ∈ sets → U ∩ V ∈ sets)

variables {X : Type*}

-- We can say that a set s is in a filter F if s ∈ F.sets
instance : has_mem (set X) (filter X) := ⟨λ s F, s ∈ F.sets⟩

lemma mem_iff_mem_sets {s : set X} {F : filter X} : s ∈ F ↔ s ∈ F.sets := iff.rfl

lemma filter_eq : ∀{F G : filter X}, F.sets = G.sets → F = G
| ⟨a, _, _, _⟩ ⟨_, _, _, _⟩ rfl := rfl

@[ext]
protected lemma ext {F G : filter X} : (∀ s, s ∈ F ↔ s ∈ G) → F = G :=
begin
  intro h,
  apply filter_eq,
  ext1 s,
  exact h s,
end

/-
### Join

Given a F, a filter of filters on X, we can define a filter on X, G, by saying
s ∈ G if and only if there exists a set of filters T ∈ F such that ∀ t ∈ T, s ∈ T.
-/
def join (f : filter (filter X)) : filter X :=
{ sets := {s | {t : filter X | s ∈ t.sets} ∈ f.sets},
  univ_mem := begin
    simp only [set.mem_set_of_eq],
    convert f.univ_mem,
    ext1,
    rw eq_true,
    exact x.univ_mem,
  end,
  superset_mem := begin
    intros s t hs hst,
    apply f.superset_mem hs,
    intros u hu,
    apply u.superset_mem _ hst,
    exact hu,
  end,
  inter_mem := begin
    intros u h hu hv,
    apply f.superset_mem (f.inter_mem hu hv),
    rintros t ⟨h1, h2⟩,
    exact t.inter_mem h1 h2,
  end }

/-!
### Principal Filter

We can define the principal filter on a set, as described above.
-/
def principal (s : set X) : filter X :=
{ sets := {t | s ⊆ t},
  univ_mem :=
  begin
    exact set.subset_univ _,
  end,
  superset_mem := begin
    rintros U V (hU : s ⊆ U) (hUV),
    exact set.subset.trans hU hUV,
  end,
  inter_mem := begin
    rintros U V (hU : s ⊆ U) (hV : s ⊆ V),
    apply set.subset_inter,
    exact hU,
    exact hV,
  end }

notation `𝓟` := principal

lemma mem_principal (s t : set X) : t ∈ 𝓟 s ↔ s ⊆ t := iff.rfl

/-!
## Order Structure on Filters

Much as sets can be ordered, by defining A ≤ B ↔ A ⊆ B, we can also order filters. We can say that
a F ≤ G if G.sets ⊆ F.sets. Note that the order is reversed from the set inclusion order. This can be
thought of as being similar to the refinement of a partition of an interval (a, b) as used in the
definition of the Riemann Integral. That is, if F ≤ G then we can think of F as a refinement of G.

Similar to how ⊆ on sets is transitive, ≤ on filters is also transitive. This means that with the
refinement analogy, if F ≤ G ≤ H, then clearly F ≤ H as F is also a refinement of H.

First, we shall define the partial order on filters.
-/

instance : partial_order (filter X) :=
{ -- Let F, G be filters, we say F ≤ G if G.sets ⊆ F.sets, or equivalently s ∈ G ⇒ s ∈ F.
  le := λ F G, ∀ ⦃s⦄, s ∈ G → s ∈ F,
  le_refl := begin
    intro F, exact set.subset.refl _,
  end,
  le_trans := begin
    intros F G H h1 h2,
    exact set.subset.trans h2 h1,
  end,
  le_antisymm := begin
    intros F G h1 h2,
    ext1,
    split,
    { apply h2 },
    { apply h1 }
  end }

lemma le_def {F G : filter X} : F ≤ G ↔ ∀ ⦃s⦄, s ∈ G → s ∈ F := iff.rfl

/-
Clearly if F is a refinement of G, and s is in G, then s must be in F.
-/
lemma mem_of_mem_of_le {s : set X} {F G : filter X} (h : F ≤ G) (hs : s ∈ G) : s ∈ F :=
begin
  apply h,
  exact hs,
end

-- This is a lemma which is helpful to prove a different lemma, but is not very useful in general.
lemma mp_sets {F : filter X} {s t : set X} (hs : s ∈ F.sets) (h : {x | x ∈ s → x ∈ t} ∈ F.sets) : t ∈ F.sets :=
F.superset_mem (F.inter_mem hs h) 
begin
  rintros x ⟨h₁, h₂⟩,
  apply h₂,
  exact h₁,
end

/-
### Infimum and Supremum

After defining the partial order structure, we now need to define the infimum and supremum of two 
filters.

First, we will define the infimum. If F, G are filters, we define F ⊓ G to be the set of all s, such 
that there exists t ∈ F and u ∈ G where t ∩ u ⊆ s. If we're using the analogy of refinements from
before, then F ⊓ G is the most refined filter which is a refinement of F and a refinement of G. That
is, F ⊓ G is the greatest common refinement of F and G.

This means that F ⊓ G ≤ F and F ⊓ G ≤ G. The final property we need is that if A ≤ B and A ≤ C, then
A ≤ B ⊓ C. That is, if A is a refinement of B, and a refinement of C, then A is a refinement of 
B ⊓ C.

-/
instance : has_inf (filter X) := ⟨λ F G, 
{ sets := {s | ∃ t ∈ F, ∃ u ∈ G, t ∩ u ⊆ s},
  univ_mem := begin
    use [set.univ, F.univ_mem, set.univ, G.univ_mem],
    simp,
  end,
  superset_mem := begin
    rintros U V ⟨t₁, ht₁, u₁, hu₁, h⟩ hUV,
    use [t₁, ht₁, u₁, hu₁],
    apply set.subset.trans h hUV,
  end,
  inter_mem := begin
    rintros U V ⟨t₁, ht₁, u₁, hu₁, h₁⟩ ⟨t₂, ht₂, u₂, hu₂, h₂⟩,
    use [t₁ ∩ t₂, F.inter_mem ht₁ ht₂, u₁ ∩ u₂, G.inter_mem hu₁ hu₂],
    rw [←set.inter_assoc, set.inter_assoc _ t₂, set.inter_comm t₂, ←set.inter_assoc, 
      set.inter_assoc (t₁ ∩ u₁)],
    apply set.inter_subset_inter,
    exact h₁,
    exact h₂,
  end }⟩

/--
Next, we shall define the supremum of two filters. If F and G are filters, then F ⊔ G is the filter
that is the least refined such that F and G are both refinements of it. We define F ⊔ G = F ∩ G, and
we can check that the properties we expect hold, that is

F ≤ F ⊔ G
G ≤ F ⊔ G

and that if A ≤ C, B ≤ C then A ⊔ B ≤ C. This means that if A and B are both refinements of C, then
C must be a refinement of A ⊔ B, which comes from our requirement that it is the least refined.
-/
instance : has_sup (filter X) := ⟨λ F G,
{ sets := {s | s ∈ F ∧ s ∈ G},
  univ_mem := begin
    split,
    exact F.univ_mem,
    exact G.univ_mem,
  end,
  superset_mem := begin
    intros U V hU hUV,
    split,
    { apply F.superset_mem hU.1 hUV },
    { apply G.superset_mem hU.2 hUV }
  end,
  inter_mem := begin
    intros U V hU hV,
    split,
    { apply F.inter_mem hU.1 hV.1 },
    { apply G.inter_mem hU.2 hV.2 }
  end }⟩

/-
With this, we can now define the two semilattice structures on filters on X, one for the sup and one
for the inf.
-/
instance : semilattice_sup (filter X) := 
{ le_sup_left := begin
    intros a b s hs,
    exact hs.1
  end,
  le_sup_right := begin
    intros a b s hs,
    exact hs.2
  end,
  sup_le := begin
    intros a b c h1 h2 s hs,
    split,
    { apply mem_of_mem_of_le h1 hs },
    { apply mem_of_mem_of_le h2 hs }
  end,
  ..filter.has_sup,
  ..filter.partial_order }

instance : semilattice_inf (filter X) :=
{ inf_le_left := begin
    intros a b s hs,
    use [s, hs, set.univ, b.univ_mem],
    simp,
  end,
  inf_le_right := begin
    intros a b s hs,
    use [set.univ, a.univ_mem, s, hs],
    simp,
  end,
  le_inf := begin
    rintros a b c h1 h2 s ⟨t, ht, u, hu, h⟩,
    apply mp_sets (h2 hu),
    apply mp_sets (h1 ht),
    convert a.univ_mem, ext1,
    dsimp,
    rw eq_true,
    intros hxt hxu,
    apply h,
    split,
    { exact hxt },
    { exact hxu }
  end,
  ..filter.has_inf,
  ..filter.partial_order }

/-
### Top and Bottom Elements

With the lattice structure on filter X, there are top and bottom elements. That is, there is a filter
⊤ such that ∀ f, f ≤ ⊤. This means that all filters are refinements of ⊤. On the other hand, we
also have a filter ⊥, such that ∀ f, ⊥ ≤ f. This means that ⊥ is a refinement of all filters.

We can check that ⊤ = 𝓟(univ) and ⊥ = 𝓟(∅) satisfies those requirements. Once we have shown that,
we have proven that filters form a bounded lattice.
-/

instance : has_top (filter X) := ⟨principal set.univ⟩

/-
Clearly the only element in the ⊤ filter must be univ. Note that the ⊤ filter cannot be empty, as
we require that univ ∈ ⊤.
-/
lemma mem_top_iff {s : set X} : s ∈ (⊤ : filter X) ↔ s = set.univ :=
begin
  exact set.univ_subset_iff,
end

instance : has_bot (filter X) := ⟨principal ∅⟩

/-
Similarly, we can show that if ⊥ is a refinement of all filters, then in fact all subsets of X must
be in ⊥.
-/
lemma mem_bot {s : set X} : s ∈ (⊥ : filter X) :=
begin
  exact set.empty_subset s,
end

instance : bounded_lattice (filter X) :=
{ le_top := begin
    intros a s hs,
    rw mem_top_iff at hs,
    rw hs,
    exact a.univ_mem,
  end,
  bot_le := begin
    intros a s hs,
    exact mem_bot,
  end,
  ..filter.semilattice_sup,
  ..filter.semilattice_inf,
  ..filter.has_top,
  ..filter.has_bot }

/-
### Sup and Inf

We can now define the supremum and infimum on a set of filters. That is, Sup(s) is the filter which
is least refined, such that all elements of s are a refinement of Sup(s). Similarly, Inf(s) is the
filter which is the greatest common refinement of the elements of s.

Let S be a set of filters. Then we can take the principal filter of S, and then join them. We can
show that the result of this operation is Sup(s).

We can define the Infimum of a set S to be the Supremum of the set of common refinements of the set
S.
-/

instance : has_Sup (filter X) := ⟨join ∘ principal⟩

protected lemma Sup_le {s : set (filter X)} {a : filter X} (h : ∀ (b : filter X), b ∈ s → b ≤ a) :
  Sup s ≤ a :=
begin
  intros t ht g hg,
  exact h _ hg ht,
end

protected lemma le_Sup {s : set (filter X)} {a : filter X} (has : a ∈ s) :
  a ≤ Sup s :=
begin
  intros t ht,
  apply ht,
  exact has,
end

instance : has_Inf (filter X) := ⟨λ s, Sup {x | ∀ y ∈ s, x ≤ y}⟩

/-
Once we have defined Sup and Inf, we now have everything we need to show that filters form a
complete lattice.
-/

instance : complete_lattice (filter X) := 
{ le_Sup := begin
    intros s a has,
    apply filters_game.le_Sup has,
  end,
  Sup_le := begin
    intros s a h,
    apply filters_game.Sup_le h,
  end,
  Inf_le := begin
    intros s a h,
    apply filters_game.Sup_le,
    intros b hb,
    apply hb,
    exact h,
  end,
  le_Inf := begin
    intros s a h,
    apply filters_game.le_Sup,
    intros g hg,
    apply h,
    exact hg,
  end,
  ..filter.bounded_lattice,
  ..filter.has_Sup,
  ..filter.has_Inf }

/-
### Basis

We can define a basis B on a filter F, which is a family of set X indexed by ι, s, with some 
property p i which satisfies

t ∈ F if and only if there exists some i, which satifies p, and t includes s i
-/

protected structure filter.has_basis {ι : Type*} (l : filter X) (p : ι → Prop) (s : ι → set X) : Prop :=
(mem_iff' : ∀ (t : set X), t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t)

lemma filter.has_basis.mem_iff {ι : Type*} {l : filter X} {p : ι → Prop} {s : ι → set X} 
  (hl : l.has_basis p s) (t : set X) : t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
hl.mem_iff' t

/-!
## Maps

As filters are just sets of sets, we can define a map function on filters. If F is a filter on X,
and m : X → Y, then we can define a new filter F.map f on Y.

(For anyone who knows what a monad/functor is, the `map` function means filters are functors, and
 with the `join` operation, this makes them a monad).

Also note that I did not define the comap in this file. I didn't feel like developing the API for
comap as well was required in this file, as all proofs can be done without. However if you're
interested, feel free to take a look at mathlib and see how comap is defined, and also try and find
out where it can be used.
-/

def filter.map {Y : Type*} (m : X → Y) (F : filter X) : filter Y :=
{ -- set.preimage m is a function : set Y → set X, then we take the preimage of F.sets under that
  -- function, which gives us set (set Y).
  -- This is the sets of all S, such that m⁻¹(S) (the preimage of S) is in F.
  sets := (set.preimage m) ⁻¹' F.sets,
  univ_mem := begin
    -- Note these rewrites aren't necessary, they are just here to illustrate the definitional equalities
    rw set.mem_preimage,
    rw set.preimage_univ,
    exact F.univ_mem
  end,
  superset_mem := begin
    intros s t hs hst,
    rw [set.mem_preimage] at hs ⊢,
    -- Note that if s ⊆ t, then we must have that m⁻¹(s) ⊆ m⁻¹(t)
    apply F.superset_mem hs,
    apply set.preimage_mono,
    exact hst,
  end,
  inter_mem := begin
    intros u v hu hv,
    rw set.mem_preimage at hu hv ⊢,
    -- Note that m⁻¹(u ∩ v) = m⁻¹(u) ∩ m⁻¹(v)
    rw set.preimage_inter,
    apply F.inter_mem,
    { exact hu },
    { exact hv }
  end }

@[simp] lemma mem_map {Y : Type*} (m : X → Y) (F : filter X) (t : set Y) : 
  t ∈ F.map m ↔ {x | m x ∈ t} ∈ F := iff.rfl

lemma map_mono {Y : Type*} {F G : filter X} (h : F ≤ G) {f : X → Y} : F.map f ≤ G.map f := 
begin
  intros s hs,
  rw mem_map at hs,
  apply mem_of_mem_of_le h hs,
end

lemma map_map {Y Z : Type*} (f : X → Y) (g : Y → Z) (F : filter X) : 
  (F.map f).map g = F.map (g ∘ f) :=
begin
  ext1,
  simp,
end

/-!

## Tendsto

Now that we defined the theory of filters, we can use these to generalise our idea of "limits" and 
"tendsto". Recall that in the definition of a limit for a real function, we say that for all 
intervals (L - ε, L + ε), there exists an interval (p - δ, p + δ) such that all points in 
(p - δ, p + δ) is mapped to somewhere within (L - ε, L + ε). Equivalently, we can say that if S is 
the preimage of (L - ε, L + ε) under f, then there exists an interval (p - δ, p + δ) ⊆ S.

We can recognise that (p - δ, p + δ) ⊆ S is precisely the requirement for S to be in the 
neighbourhood filter around p.

Thus, if f : X → Y, F is a filter on X and G is a filter on Y, then we can say that f converges to 
G along F if

∀ X ∈ G, f⁻¹(X) ∈ F

This is equivalent to saying F.map f ≤ G.
-/

def tendsto {α β : Type*} (f : α → β) (F : filter α) (G : filter β) := F.map f ≤ G

lemma tendsto_def {α β : Type*} (f : α → β) (F : filter α) (G : filter β) : 
  tendsto f F G ↔ F.map f ≤ G := iff.rfl

lemma tendsto_iff {α β : Type*} (f : α → β) (F : filter α) (G : filter β) :
  tendsto f F G ↔ ∀ (X : set β), X ∈ G → f ⁻¹' X ∈ F := iff.rfl

/-!
## Preliminaries

It's nice that we have defined what it means for a filter to tend to another one, but without any
concrete examples of filters, it may not be obvious how filters work. But before then, we will need
some lemmas.

This section needs to be tidied up.
-/

lemma le_principal_iff {s : set X} {f : filter X} : f ≤ 𝓟 s ↔ s ∈ f :=
begin
  change (∀ {t}, s ⊆ t → t ∈ f) ↔ _,
  split,
  { intro h,
    apply h,
    exact set.subset.refl _ },
  { intros h t hst,
    apply f.superset_mem h,
    exact hst }
end

lemma principal_mono {s t : set X} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t :=
begin
  rw [le_principal_iff, mem_principal],
end

lemma eq_Inf_of_mem_sets_iff_exists_mem {S : set (filter X)} {l : filter X}
  (h : ∀ {s}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) : l = Inf S :=
begin
  apply le_antisymm,
  { apply le_Inf _,
    intros b hb s hs,
    rw h,
    use [b, hb, hs] },
  { intros s hs,
    rcases h.1 hs with ⟨f, hf, hs'⟩,
    exact mem_of_mem_of_le (Inf_le hf) hs' }
end

lemma eq_infi_of_mem_sets_iff_exists_mem {ι : Type*} {f : ι → filter X} {l : filter X}
  (h : ∀ {s}, s ∈ l ↔ ∃ i, s ∈ f i) :
  l = infi f :=
eq_Inf_of_mem_sets_iff_exists_mem $ λ s, h.trans set.exists_range_iff.symm

lemma infi_sets_eq {ι : Type*} {f : ι → filter X} (h : directed (≥) f) [ne : nonempty ι] : 
  (⨅ i, f i).sets = ⋃ i, (f i).sets :=
let ⟨i⟩ := ne,
  u : filter X := 
    { sets := ⋃ i, (f i).sets,
      univ_mem := begin
        rw [set.mem_Union],
        use [i, (f i).univ_mem],
      end,
      superset_mem := begin
        rintros U V ⟨S, ⟨j, rfl⟩, hj⟩ hUV,
        rw set.mem_Union,
        use j,
        apply (f j).superset_mem _ hUV,
        exact hj,
      end,
      inter_mem := begin
        rintros U V ⟨S, ⟨j, rfl⟩, hj⟩ ⟨T, ⟨k, rfl⟩, hk⟩,
        rcases h j k with ⟨l, hl⟩,
        rw set.mem_Union,
        use l,
        apply (f l).inter_mem,
        { apply mem_of_mem_of_le hl.1,
          exact hj },
        { apply mem_of_mem_of_le hl.2,
          exact hk }
      end } in
begin
  change _ = u.sets,
  apply congr_arg filter.sets,
  symmetry,
  apply eq_infi_of_mem_sets_iff_exists_mem,
  intro s,
  exact set.mem_Union,
end

lemma mem_infi {ι : Type*} {f : ι → filter X} (h : directed (≥) f) [nonempty ι] (s) :
  s ∈ infi f ↔ ∃ i, s ∈ f i :=
by simp only [mem_iff_mem_sets, infi_sets_eq h, set.mem_Union]

lemma mem_binfi {ι : Type*} {f : ι → filter X} {s : set ι}
  (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) {t : set X} :
  t ∈ (⨅ i∈s, f i) ↔ ∃ i ∈ s, t ∈ f i :=
by haveI : nonempty {x // x  ∈ s} := ne.to_subtype;
  erw [infi_subtype', mem_infi h.directed_coe, subtype.exists]; refl

lemma has_basis_binfi_principal {ι : Type*} {s : ι → set X} {S : set ι} (h : directed_on (s ⁻¹'o (≥)) S)
  (ne : S.nonempty) :
  (⨅ i ∈ S, 𝓟 (s i)).has_basis (λ i, i ∈ S) s :=
⟨begin
  refine λ t, (mem_binfi _ ne).trans $ by simp only [mem_principal],
  rw [directed_on_iff_directed, ← directed_comp, (∘)] at h ⊢,
  apply h.mono_comp _ _,
  exact λ _ _, principal_mono.2
end⟩

lemma has_basis_infi_principal {ι : Type*} {s : ι → set X} (h : directed (≥) s) [nonempty ι] :
  (⨅ i, 𝓟 (s i)).has_basis (λ _, true) s :=
⟨begin
  refine λ t, (mem_infi (h.mono_comp _ _) t).trans $
    by simp only [exists_prop, true_and, mem_principal],
  exact λ _ _, principal_mono.2
end⟩

lemma mem_infi_sets {ι : Type*} {f : ι → filter X} (i : ι) : ∀{s}, s ∈ f i → s ∈ ⨅i, f i :=
show (⨅i, f i) ≤ f i, from infi_le _ _

/-!
## Neighbourhood Filter

One of the most basic examples of a filter is the neighbourhood filter. Let p ∈ X be a point, and let
S be any open subset of X such that x ∈ S. Then we can define the principal filter on S. Now if we
take the infimum over all S of the principle filters, we get the neighbourhood filter.

We denote the neighbourhood filter on a point p by 𝓝(p).
-/

def nhds {X : Type*} [topological_space X] (p : X) : filter X :=
(⨅ s ∈ {s : set X | p ∈ s ∧ is_open s}, 𝓟 s)

notation `𝓝` := nhds

/-
The open sets containing the point p form a basis for 𝓝 p.
-/
lemma nhds_basis_opens (a : X) [topological_space X] : 
  (𝓝 a).has_basis (λ s : set X, a ∈ s ∧ is_open s) (λ x, x) :=
begin
  apply has_basis_binfi_principal,
  { rintros s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩,
    use s ∩ t,
    refine ⟨_, _, _⟩,
    { split,
      { exact ⟨hs₁, ht₁⟩ },
      { apply is_open_inter,
        { exact hs₂ },
        { exact ht₂ } } },
    { simp },
    { simp } },
  { use set.univ,
    split,
    { exact set.mem_univ _ },
    { exact is_open_univ } }
end

/-
Within a topological space, a set s is in 𝓝 p if and only if there exists some open set t such that
t ⊆ s and p ∈ t.
-/
lemma mem_nhds_iff {p : X} [topological_space X] {s : set X} : 
  s ∈ 𝓝 p ↔ ∃ t ⊆ s, p ∈ t ∧ is_open t := 
begin
  rw (nhds_basis_opens p).mem_iff,
  simp only [exists_prop],
  simp_rw [and_comm],
end

/-
Next, to show that this definition agrees with the intuitive understanding, let's show that in a 
metric space X, the open ball around X with radius r is in the neighbourhood filter.
-/

lemma ball_mem_nhds {p : X} [metric_space X] {r : ℝ} (hr : 0 < r) : metric.ball p r ∈ 𝓝 p :=
begin
  rw mem_nhds_iff,
  use metric.ball p r,
  refine ⟨_, _, _⟩,
  { exact rfl.subset },
  { exact metric.mem_ball_self hr },
  { exact metric.is_open_ball }
end

lemma mem_nhds_iff_exists_ball {p : X} [metric_space X] {s : set X} : s ∈ 𝓝 p ↔ ∃ (r > 0), metric.ball p r ⊆ s :=
begin
  split,
  { intro h,
    rw mem_nhds_iff at h,
    rcases h with ⟨t, hst, ht₁, ht₂⟩,
    rw metric.is_open_iff at ht₂,
    rcases ht₂ p ht₁ with ⟨r, hr, hb⟩,
    use [r, hr],
    apply set.subset.trans hb hst },
  { rintro ⟨r, hr, hb⟩,
    apply filter.superset_mem _ _ hb,
    exact ball_mem_nhds hr }
end

lemma mem_of_mem_nhds {p : X} [topological_space X] {s : set X} (h : s ∈ 𝓝 p) : p ∈ s :=
begin
  rw mem_nhds_iff at h,
  rcases h with ⟨t, hts, hpt, ht⟩,
  apply hts,
  exact hpt,
end

/-!
### At Top Filter

Another filter that we will need is the at top filter, which is the filter of all subsets of the 
form {x | a ≤ x}. This can be used to state the convergence of functions, as well as the convergence
of sequences.
-/

def at_top {X : Type*} [preorder X] : filter X := ⨅ a, principal (set.Ici a)

lemma mem_at_top [preorder X] (a : X) : {b | a ≤ b} ∈ (at_top : filter X) :=
begin
  apply mem_infi_sets a,
  exact set.subset.refl _,
end

lemma at_top_basis [nonempty X] [semilattice_sup X] :
  (@at_top X _).has_basis (λ _, true) set.Ici :=
has_basis_infi_principal (directed_of_sup $ λ a b, set.Ici_subset_Ici.2)

lemma mem_at_top_sets [nonempty X] [semilattice_sup X] {s : set X} :
  s ∈ (at_top : filter X) ↔ ∃a:X, ∀b≥a, b ∈ s :=
-- at_top_basis.mem_iff.trans $ exists_congr $ λ _, exists_const _
begin
  rw at_top_basis.mem_iff,
  { apply exists_congr,
    intro a,
    simp only [ge_iff_le, exists_prop_of_true],
    refl },
  apply_instance
end

/-!
### At Bot Filter

Much like how at top represents the filter as x → ∞, we also have thet at bot filter for when
x → -∞.
-/

def at_bot {X : Type*} [preorder X] : filter X := ⨅ a, principal (set.Iic a)

lemma mem_at_bot [preorder X] (a : X) : {b | b ≤ a} ∈ (at_bot : filter X) :=
begin
  apply mem_infi_sets a,
  exact set.subset.refl _,
end

/-!
## Convergence

Let's start off with something simple. Let's prove that the constant function f(x) = c tendsto c as 
x → p in some metric space X.
-/

example [metric_space X] (c p : X) : tendsto (λ x, c) (𝓝 p) (𝓝 c) :=
begin
  intros s hs,
  rw mem_map,
  rw mem_nhds_iff,
  use metric.ball p 1,
  refine ⟨_, _, _⟩,
  { intros x hx,
    simp only [set.mem_set_of_eq],
    apply mem_of_mem_nhds,
    exact hs },
  { apply metric.mem_ball_self,
    exact zero_lt_one },
  { apply metric.is_open_ball }
end

/-
Now let's prove that the filter definition of convergence is the same as the epsilon-delta
version of convergence.

Note x ∈ metric.ball c δ is the same as dist(c, x) < δ
-/

lemma tendsto_nhds_nhds_iff [metric_space X] {Y : Type*} [metric_space Y] (c : X) (p : Y) (f : X → Y) :
  tendsto f (𝓝 c) (𝓝 p) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ metric.ball c δ, f x ∈ metric.ball p ε :=
begin
  split,
  { intros h ε hε,
    let B := metric.ball p ε,
    have hB : B ∈ 𝓝 p,
    { apply ball_mem_nhds,
      exact hε },
    specialize h hB,
    rw [mem_map, mem_nhds_iff_exists_ball] at h,
    rcases h with ⟨δ, hδ, hδ'⟩,
    use [δ, hδ],
    intros x hx,
    exact hδ' hx, },
  { intros h s hs,
    rw [mem_nhds_iff_exists_ball] at hs,
    rcases hs with ⟨ε, hε, hε'⟩,
    rcases h ε hε with ⟨δ, hδ, hδ'⟩,
    rw [mem_map, mem_nhds_iff_exists_ball],
    use [δ, hδ],
    intros x hx,
    apply hε',
    apply hδ',
    exact hx }
end

/-
Now let's prove that the filter definition of f(x) = c as x → ∞ is the same as the one we commonly
use.
-/

lemma tendsto_at_top_nhds_iff [semilattice_sup X] [nonempty X] {Y : Type*} [metric_space Y] 
  (f : X → Y) (c : Y) : tendsto f at_top (𝓝 c) ↔ ∀ ε > 0, ∃ y, ∀ x ≥ y, f x ∈ metric.ball c ε :=
begin
  split,
  { intros h ε hε,
    let B := metric.ball c ε,
    have hB : B ∈ 𝓝 c,
    { apply ball_mem_nhds,
      exact hε },
    specialize h hB,
    rw [mem_map, mem_at_top_sets] at h,
    rcases h with ⟨y, hy⟩,
    use y,
    intros x hx,
    apply hy,
    exact hx },
  { intros h s hs,
    rw [mem_nhds_iff_exists_ball] at hs,
    rcases hs with ⟨ε, hε, hε'⟩,
    rw [mem_map, mem_at_top_sets],
    cases h ε hε with y hy,
    use y,
    intros x hx,
    apply hε',
    apply hy,
    exact hx }
end

/-
Finally, let's prove the convergence of a sequence.
-/

example [metric_space X] (x : ℕ → X) (c : X) :
  tendsto x at_top (𝓝 c) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, x n ∈ metric.ball c ε :=
begin
  apply tendsto_at_top_nhds_iff,
end

/-
So the generality of the at_top filter means that the convergence of a function f(x) as x → ∞,
and the convergence of a sequence x₁, x₂, ... are in fact the same thing. Pretty cool?
-/

/-!
## Composition

So far, we've had to set up the different filters, so the merit of using filters versus epsilon-delta
limits isn't clear yet. However, once we want to compose limits, then filters make it a lot easier.

For example, if we want to show that if a sequence x_n → a, and f(x) → b as x → a, then f(x_n) → b.
-/

example (x : ℕ → ℝ) (a b : ℝ) (hx : limit_of_sequence x a) (f : ℝ → ℝ) (hf : limit_of_function f a b) :
  limit_of_sequence (λ n, f (x n)) b :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ, hδ'⟩,
  cases hx δ hδ with N hN,
  use N,
  intros n hn,
  apply hδ',
  apply hN,
  exact hn
end

/-!
Now for every type of limit we have, we will need to write a composition lemma. Instead, if we have
filters, we can write a more general `tendsto_comp`, and this single lemma can perform the task of
all of the composition lemmas for different types of limits.
-/

lemma tendsto_comp {α β γ : Type*} (F : filter α) (G : filter β) (H : filter γ) (f : α → β) 
  (g : β → γ) (hf : tendsto f F G) (hg : tendsto g G H) : tendsto (g ∘ f) F H :=
begin
  rw tendsto_iff at *,
  intros s hs,
  rw set.preimage_comp,
  apply hf,
  apply hg,
  exact hs,
end

/-!
Finally, as we have an order structure on filters, we can also use that to prove that limits compose.
With `calc` mode, this makes it easy to work out the composition of multiple tendstos/filters.
-/

example {α β γ : Type*} (F : filter α) (G : filter β) (H : filter γ) (f : α → β) 
  (g : β → γ) (hf : tendsto f F G) (hg : tendsto g G H) : tendsto (g ∘ f) F H :=
calc
-- Rewriting by definition
  F.map (g ∘ f) = (F.map f).map g : by rw map_map
-- We need to show (F.map f).map g ≤ G.map g, and as `map` is monotone, suffices to show that 
-- `F.map f ≤ G`, but that is precisely `tendsto f F G`
            ... ≤ G.map g : map_mono hf
-- Now we need to show that `G.map g ≤ H`, but that's just `tendsto g G H`.
            ... ≤ H : hg

end filters_game

/-
## The End

This is the end of this file, which should have been an introduction to filters, and some examples,
as well as showing the equivalence between filters and the epsilon-delta (and others) definitions of
limits that we are familiar with. With this, there isn't too much point in continuing on, as we will
simply be duplicating parts of mathlib.

To see filters further, feel free to check out the use of filters in mathlib (which in fact can be
used for more than just limits), and also the LFTCM2020 exercises, available at

https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/friday/topology.lean
-/