Trying to do real analysis with filters

Stream: new members

[rtertr (Sonia)]

Hello everyone,
I am trying to prove different limits on \R using filters. I unfortunately haven't been able to prove anything other than these simple limits.
Right now, my first goal is just to show lim x->0 x^2 = 0, but as soon as my function is no longer just x, I can't move forward.
I have seen work material where limits are proved using new definitions such as
def tendsto (a : ℕ → ℝ) (t : ℝ) : Prop :=∀ ε > 0, ∃ B : ℕ, ∀ n, B ≤ n → |a n - t| < ε in ImperialCollegeLondon/formalising-mathematics-2022.
So I guess my question is, how do I transform tendsto (λ (x : ℝ), f(x) ) (nhds (a:ℝ) ) (nhds (b:ℝ)) into something like
∀ ε > 0, ∃ δ > 0, ∀ (x:ℝ), 0<|x - p| < δ → |f(x) - L| < ε without making my own definition and simply working with the theorems for filters, maps, etc.
Last, but not least, thank you for letting me join this community! Excited to improve my math skills using Lean.

import tactic
import topology.basic
import analysis.special_functions.exp_deriv

open set
open real
open filter

namespace my_work

noncomputable theory

lemma my_limit1 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), (x)) (nhds (0:ℝ) ) (nhds (0:ℝ)) :=
begin
unfold tendsto,
rw filter.map_id',
exact nhds_le_nhds_iff.mpr rfl,
end

lemma my_limit2 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), x) (nhds (0:ℝ) ) (nhds (0:ℝ)) :=
begin
rw tendsto_def,
intro y,
intro h,
simp only [preimage_id'],
exact h,
end

lemma my_limit3 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), (8:ℝ)) (nhds (0:ℝ) ) (nhds (8:ℝ)) :=
begin
unfold tendsto,
rw filter.map_const,
exact pure_le_nhds 8,
end

lemma my_limit4 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), x+ (0:ℝ )) (nhds (0:ℝ) ) (nhds (0:ℝ)) :=
begin
unfold tendsto,
rw ←filter.add_pure,
simp,
sorry,
end

lemma my_limit5 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), x+ (0:ℝ )) (nhds (0:ℝ) ) (nhds (0:ℝ)) :=
begin
unfold tendsto,
rw ←filter.add_pure,
simp,
sorry,
end

lemma my_limit6 (x:ℝ ) (y:ℝ ) (f : ℝ → ℝ ) (F : filter ℝ ) (G : filter ℝ ): tendsto (λ (x : ℝ), x*x) (nhds (0:ℝ) ) (nhds (0:ℝ)) :=
begin
rw tendsto_def,
intro y,
intro h,
sorry
end

end my_work

[Eric Wieser]

(#backticks might help you with formatting)

[Kevin Buzzard]

I'm unclear about whether you want to use filters in the proof you're writing that x^2->0 or whether you want to avoid them

[Kevin Buzzard]

To add to the confusion, you seem to be using tendsto to mean two different things in your post

[Alistair Tucker]

rtertr said:

So I guess my question is, how do I transform tendsto (λ (x : ℝ), f(x) ) (nhds (a:ℝ) ) (nhds (b:ℝ)) into something like
∀ ε > 0, ∃ δ > 0, ∀ (x:ℝ), 0<|x - p| < δ → |f(x) - L| < ε without making my own definition and simply working with the theorems for filters, maps, etc.

Would rw [tendsto_nhds_nhds] be what you're looking for?

[Patrick Massot]

@rtertr, I strongly advise you use your real name here since otherwise many people will think you are simply a student trying to cheat with some exercises. I'll answer this first question anyway. First you need to understand that your statement quoted by Alistair is simply false, because your tendsto uses docs#nhds and you $\epsilon$ and $\delta$ version uses punctured neighborhoods. You can translate using:

import topology.instances.real

open_locale topology
open filter set metric

example (f : ℝ → ℝ) (a b : ℝ) :
  tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - b| < ε :=
tendsto_nhds_nhds

example (f : ℝ → ℝ) (a b : ℝ) :
  tendsto f (𝓝[≠] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, 0 < |x - a| → |x - a| < δ → |f x - b| < ε :=
by simp [tendsto_nhds_within_nhds, real.dist_eq, mem_compl_singleton_iff, ← dist_pos]

Note those are really lemmas about metric spaces that are specialized to real numbers using the definition of the distance there.

[Patrick Massot]

The second example uses punctured neighborhoods, denoted by 𝓝[≠].

[Patrick Massot]

If you want to see results about limits of polynomials you can go to https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/polynomials.html. I can't be more specific unless you tell us what you actually want to do.

[Patrick Massot]

Last remark: your 0 < |x - a| < δ → will not work in Lean. If you are confused by this or by why I replaced it with 0 < |x - a| → |x - a| < δ → then you need to read basic explanations, for instance in #mil.

[rtertr (Sonia)]

Hello again everyone,
Thank you for all your help! My name is Sonia, and I am just trying some different elementary things in Lean to help me eventually formalize some more complicated math for my thesis.
To answer @Kevin Buzzard, I guess I wanted the starting point to be filters to keep it general. But then I wanted to either transform the proof into an epsilon-delta proof, or (ideally) prove my proofs without using the epsilon-delta definition. I know I referred to your sequence definition from your work sheet, but it was just a reference for where I had seen something defined like real analysis. I want to work with the function limit, not the sequence.
To @Alistair Tucker and @Patrick Massot , I think this is exactly what I was looking for. Thank you! I will take a look at the limits of polynomials!
Again, thank you all. I guess my next goal is to show that a function is bounded, but first I wanted to understand how the limits worked in Lean.

[Patrick Massot]

Did you read #mil?

[Patrick Massot]

Hopefully reading that book (and doing the exercises) should make your Lean learning a lot easier.

[Kevin Buzzard]

By the way, in my 2023 course I changed the epsilon delta definition to tends_to to fix the unfortunate nameclash

[rtertr (Sonia)]

Yes! Not all of it, but some of it. I think you, @Patrick Massot, wrote the section on Topology Filters cause I also found it through your website. It really helped, but since I haven't done a course on topology, thus I wanted to go back to real analysis!
@Kevin Buzzard , thank you, great, I will take a look!