Continuity

Stream: new members

[Parivash]

Hi,
I'm going to prove the left continuity of this function:
$f(x)-f(x_c)$ in which $f(x)= (\frac{1}{x})^2$
I want to prove that the lim of ($f(x)-f(x_c)$) when x approach $x_c$ from left is equal to the value of the function ($f(x)-f(x_c)$) at $x_c$ which is equal to zero

I define it like this:

import data.real.basic
import topology.instances.real
import analysis.normed_space.basic
import tactic.linarith


open filter
open_locale topological_space
noncomputable theory

open filter set

def f (x : ℝ) : ℝ := (1/x)^2

def f_shift (x x_c : ℝ) : ℝ := f x - f x_c

lemma limit_V_shift (x x_c : ℝ) (hx : x ≠ 0)(hx_c : x_c ≠ 0) :
  tendsto (λ x, f_shift x x_c) (𝓝[Iio x_c] x_c) (𝓝 0) :=
begin
  sorry,
end

is it correct?

[Kevin Buzzard]

This code does not compile for me on recent master: I get locale topological_space does not exist. Are you using a very old mathlib? I think this changed several months ago. I changed it to open_locale topology and got it compiling. As for the mathematics, I'm not sure what 𝓝[Iio x_c] x_c means but this is my problem, not yours :-)

[Parivash]

Oh, thanks for point it out.
Yeah, I used the notation 𝓝[Iio x_c] x_c to represent the behavior of a function as it approaches a particular value from one side (in this case, from values less than x_c).
In particular, I used it to express the idea that x tending to x_c from the left
But don't have idea how to prove it!

[Jireh Loreaux]

@Kevin Buzzard 𝓝[s] c is notation for nhds_within c s := 𝓝 c ⊓ filter.principal s

[Eric Wieser]

Is 𝓝[Iio x_c] x_c the same as 𝓝[≤] x_c?

[Jireh Loreaux]

Well, 𝓝[<] x_c, but yes.

[Eric Wieser]

I always screw up when reading the io/ic interval variants

[Kevin Buzzard]

Mathematically it looks like the statement is true then

[Jireh Loreaux]

There's an extraneous x in the statement though.

[Jireh Loreaux]

@Parivash is there a reason you want to prove this statement from scratch? It should follow easily from things we have in the library.

[Parivash]

Excuse me!
No, I just want to prove this:
$lim(f x - f x_c) (x \to x_c^-) = f x_c -f x_c = 0$
No matter how!

[Jireh Loreaux]

For instance, we have a has_continuous_inv₀ ℝ instance.

[Jireh Loreaux]

I have to feed my kids now, but if no one has given you hints in an hour or so I'll write something up.

[Jireh Loreaux]

import topology.instances.real

-- note that `continuous_within_at` exactly captures what you want
-- this is a step-by-step proof so you can see the pieces.
example {c : ℝ} (hc : c ≠ 0) :
  continuous_within_at (λ x : ℝ, (1 / x) ^ 2) (set.Iio c) c :=
begin
  refine continuous_at.continuous_within_at _,
  simp_rw [←inv_eq_one_div],
  change continuous_at ((λ x : ℝ, x ^ 2) ∘ (λ x : ℝ, x⁻¹)) c,
  refine continuous_at.comp _ (continuous_at_inv₀ hc),
  refine continuous.continuous_at _,
  exact continuous_pow 2,
end

-- the above can be golfed to this
lemma foo {c : ℝ} (hc : c ≠ 0) :
  continuous_within_at (λ x : ℝ, (1 / x) ^ 2) (set.Iio c) c :=
by simpa only [←inv_eq_one_div] using
  ((continuous_pow 2).continuous_at.comp (continuous_at_inv₀ hc)).continuous_within_at

-- Of course, this fact is stronger, and we used it to prove the above:
example {c : ℝ} (hc : c ≠ 0) :
  continuous_at (λ x : ℝ, (1 / x) ^ 2) c :=
by simpa only [←inv_eq_one_div] using
  (continuous_pow 2).continuous_at.comp (continuous_at_inv₀ hc)

-- this was technically the statement you had, but it follows from `foo` easily.
example {c : ℝ} (hc : c ≠ 0) :
  filter.tendsto (λ x : ℝ, (1 / x) ^ 2 - (1 / c) ^ 2) (𝓝[<] c) (𝓝 0) :=
begin
  have : continuous_within_at (λ x : ℝ, (1 / x) ^ 2 - (1 / c) ^ 2) (set.Iio c) c,
    from (foo hc).sub tendsto_const_nhds,
  simpa only [continuous_within_at, sub_self],
end

[Parivash]

Excellent!
Thank you @Jireh Loreaux

[David⚛️]

Jireh Loreaux said:

import topology.instances.real

-- note that `continuous_within_at` exactly captures what you want
-- this is a step-by-step proof so you can see the pieces.
example {c : ℝ} (hc : c ≠ 0) :
  continuous_within_at (λ x : ℝ, (1 / x) ^ 2) (set.Iio c) c :=
begin
  refine continuous_at.continuous_within_at _,
  simp_rw [←inv_eq_one_div],
  change continuous_at ((λ x : ℝ, x ^ 2) ∘ (λ x : ℝ, x⁻¹)) c,
  refine continuous_at.comp _ (continuous_at_inv₀ hc),
  refine continuous.continuous_at _,
  exact continuous_pow 2,
end

-- the above can be golfed to this
lemma foo {c : ℝ} (hc : c ≠ 0) :
  continuous_within_at (λ x : ℝ, (1 / x) ^ 2) (set.Iio c) c :=
by simpa only [←inv_eq_one_div] using
  ((continuous_pow 2).continuous_at.comp (continuous_at_inv₀ hc)).continuous_within_at

-- Of course, this fact is stronger, and we used it to prove the above:
example {c : ℝ} (hc : c ≠ 0) :
  continuous_at (λ x : ℝ, (1 / x) ^ 2) c :=
by simpa only [←inv_eq_one_div] using
  (continuous_pow 2).continuous_at.comp (continuous_at_inv₀ hc)

-- this was technically the statement you had, but it follows from `foo` easily.
example {c : ℝ} (hc : c ≠ 0) :
  filter.tendsto (λ x : ℝ, (1 / x) ^ 2 - (1 / c) ^ 2) (𝓝[<] c) (𝓝 0) :=
begin
  have : continuous_within_at (λ x : ℝ, (1 / x) ^ 2 - (1 / c) ^ 2) (set.Iio c) c,
    from (foo hc).sub tendsto_const_nhds,
  simpa only [continuous_within_at, sub_self],
end

Please can you show these lines of code of continuity in Lean 4?

[Kevin Buzzard]

Are you asking how to translate this code into lean 4? Did you try yourself? Where do you get stuck?

[Jireh Loreaux]

Mathport oneshot can also do that for you.

[David⚛️]

Kevin Buzzard said:

Are you asking how to translate this code into lean 4? Did you try yourself? Where do you get stuck?

Yea ,
I was asking how to translate the code into lean 4 as I want to try something similar but the syntax remains unclear to me.

[David⚛️]

Jireh Loreaux said:

Mathport oneshot can also do that for you.

Not familiar with Mathport oneshot.

[Jireh Loreaux]

@David⚛️ : https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md

[David⚛️]

@Jireh Loreaux @Kevin Buzzard
At this point, my challenge is having a full grasp of how to use Mathlib.
This question might sound so dumb but I need to speak up.
The def and theorems in the doc of Mathlib, how do I apply /use them to whatever I wanna prove?
Is a struggle for me.

[Jireh Loreaux]

Can you give an example of what you want to prove? Something simple to start is a good idea. Separately, have you had a look at some of our learning resources, like #mil ?

[David⚛️]

I've had time to go through some of the learning resources (Mechanics of Proof).
For example, if I want to show a function is continuous, I know Mathlib can help me but I don't know how to use it even when I open the Mathlib doc