## Stream: new members

### Topic: bounding limits

#### Alex Kontorovich (Oct 01 2020 at 19:56):

Hello! I see theorems like cau_seq.lim_le here https://leanprover-community.github.io/mathlib_docs/data/real/cau_seq_completion.html which say f(n)<x -> lim f < x. If I know that f(n) and g(n) are Cauchy sequences, and f(n)<= g(n), is there really not a theorem that says lim f <= lim g? (Or am I missing something stupid?) Thanks!

#### Kevin Buzzard (Oct 01 2020 at 20:12):

I think these lemmas you're looking at don't say what you think they say. <= and < are defined on Cauchy sequences such that f <= g iff lim(f)<=lim(g) (when the limits exist). The lemmas lt_lim and lim_lt are not used at all in mathlib. The theorem you want will probably be expressed in terms of filters and will probably be there.

#### Heather Macbeth (Oct 01 2020 at 22:10):

@Alex Kontorovich Here's the statement, for limits rather than Cauchy sequences:
docs#le_of_tendsto_of_tendsto'

lemma le_of_tendsto_of_tendsto' {f g : β → α} {b : filter β} {a₁ a₂ : α} [ne_bot b]
(hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) :
a₁ ≤ a₂ :=


#### Heather Macbeth (Oct 01 2020 at 22:11):

Did you specifically want it to be about Cauchy sequences (or will it be enough for you to have it for limits, together with having access to a theorem saying that a Cauchy sequence has a limit)?

#### Alex Kontorovich (Oct 01 2020 at 23:22):

Hmm interesting. I'm trying to mimic the mathlib proof of exp_bound:

https://github.com/leanprover-community/mathlib/blob/4851857/src/data/complex/exponential.lean#L1021

Line 1025 says:

refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),


This converts the goal which is a statement about limits into a statement about jth terms of the defining sequences (the right side of which is constant). Kevin, are you saying there's some way to do that more directly, since <= is already "defined" on Cauchy sequences?... Thanks!

#### Heather Macbeth (Oct 01 2020 at 23:25):

Can I ask what context you're working in? Is it a different bound involving the exponential function? The special_functions library is especially ad hoc, so tricks that are needed for the exponential function because of its particular definition might not translate to other contexts.

#### Heather Macbeth (Oct 01 2020 at 23:32):

For example, exp is defined literally via a Cauchy sequence, but there is also a full library on infinite sums
https://leanprover-community.github.io/mathlib_docs/topology/algebra/infinite_sum.html
which would provide an alternative framework (maybe it didn't exist when the exp file was written).

#### Alex Kontorovich (Oct 01 2020 at 23:32):

Yes, I'm playing around with exp... I managed to prove that, if |x|<1/2, then |exp(x)-(1+x)|<1 (again, very ugly code, sorry):

theorem expBnd : ∀ x:ℂ , complex.abs x < 1/2 → complex.abs (complex.exp x - (1+x))< 1:=
begin
intros,

have rwrw1: complex.abs (complex.exp x - 1 - x) ≤ complex.abs x ^ 2,
{
refine complex.abs_exp_sub_one_sub_id_le _,
linarith,
},
have rwrw2: complex.abs x ^ 2 < 1/2 * 1/2,
{
have rw3: complex.abs x ^ 2 = complex.abs x  * complex.abs x,
{
ring,
},
rw rw3,
refine mul_lt_mul'' _ _ _ _ ,
linarith,
have rw5: (2:ℝ )⁻¹ =1/2,
{
rw  division_def,
ring,
},
rw rw5,
exact a,
exact absnonneg x,
exact absnonneg x,
},
have rwrw3: (1:ℝ )/2*1/2 =1/4,
{
ring,
},
have rwrw4: complex.abs (complex.exp x - 1 - x) < 1/2 * 1/2,
{
exact gt_of_gt_of_ge rwrw2 rwrw1,
},
have rwrw5: complex.abs (complex.exp x - 1 - x) = complex.abs (complex.exp x - (1 + x)),
{
ring,
},
have rwrw6: (1:ℝ )/4<1, by linarith,
rw ←  rwrw5,
rw rwrw3 at rwrw4,
linarith,
end


but now I'm trying to see how to do it without calling complex.abs_exp_sub_one_sub_id_le, by directly accessing the series. Of course the human proof is trivial:

|exp(x)-(1+x)| \le |x|^2/2+|x|^3/3!+...\le |x|^2+|x|^3+... \le 1

since |x|<1/2...

#### Alex Kontorovich (Oct 01 2020 at 23:38):

And the proof of complex.abs_exp_sub_one_sub_id_le uses exp_bound...

But thanks for the tip Heather, I'll try to mess around with infinite_sum...

#### Heather Macbeth (Oct 01 2020 at 23:38):

(just to continue with a guide to the more general approaches -- here's a file I wrote setting up the function $x\mapsto x^{-1}$ (where defined) in a Banach algebra, using the infinite sum framework I pointed to above:
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/units.html
and, btw, since last week @Yury G. Kudryashov has started seriously working towards analytic functions "done right"!
https://github.com/leanprover-community/mathlib/pull/4291#issuecomment-699684052 )

#### Yury G. Kudryashov (Oct 01 2020 at 23:48):

I'd say @Sebastien Gouezel already did most of the work but we need some glue to use it for exp, sin, etc.

#### Heather Macbeth (Oct 01 2020 at 23:53):

Yury, what setting are you planning to work in?

#### Heather Macbeth (Oct 01 2020 at 23:54):

Will you do single-variable power series in Banach algebras?

#### Heather Macbeth (Oct 01 2020 at 23:54):

Or something more general that unites the above theory with the theory of several complex variables?

#### Yury G. Kudryashov (Oct 01 2020 at 23:56):

The first step will be to define a function from mv_power_series (fin n) to continuous_multilinear_maps on A^n and from power_series to A, where A is an algebra.

#### Heather Macbeth (Oct 02 2020 at 00:02):

You could conceivably work on modules over A rather than just A^n. But I'm not sure there's any point.

Last updated: May 11 2021 at 14:11 UTC